10 Unification and anti-unification
Unification is presented as a practical way to solve equations with unknowns by filling in holes so two structures become equal. The chapter first builds intuition with stacks, then generalizes to immutable binary terms made of holes, constants, and symbols, using substitutions to represent bindings. It explains that the key idea is not limited to math: once the structure is formalized, the same mechanism can power reasoning over trees, terms, and other data representations.
The chapter then develops Robinson-style unification carefully, showing why naïve approaches fail. A simple recursive algorithm works on easy cases but breaks when a substitution creates cycles or when bound holes are not fully resolved before further checks. The corrected algorithm introduces an occurs check and forces bound holes to be looked up before proceeding, which prevents self-referential substitutions and makes the result sound. The author also discusses performance, noting that the straightforward implementation can be expensive, but that deduplicated immutable structures and memoization can improve it substantially.
After establishing unification, the chapter shows why it matters in practice. It maps type inference problems to unification, demonstrating how generic type parameters and inferred types can be solved as term equations. It also connects unification to logic programming, where rules and facts are matched through backtracking search, as in Prolog. Finally, the chapter introduces anti-unification as the reverse process: instead of filling holes to make things equal, it extracts the most specific common generalization of two terms. This is used to detect code clones and infer bug-fix patterns from examples, such as repeatedly discovering the same null-check transformation across different fixes.
I’ve replaced parts of two immutable stacks with square holes X and Y. What could go in the holes to make the two stacks identical?
Our immutable stack unification problem looks nearly identical when drawn as a binary term. Again, holes are squares, symbols are ovals, and constants are circles.
This version of the problem, with Y replaced by X, ought to be unsolvable because it gives contradictory requirements for the stuff to fill into hole X: both the number 2 and a one-item stack that itself contains a reference to X.
The left sides of the roots imply that X is an alias for Y. The right sides imply that Y is a one-item stack containing X. We need an algorithm that will detect this circularity and cause unification to fail instead of entering unbounded recursion later.
An even simpler unification problem that our current naïve algorithm doesn’t handle correctly. If Y is both 2 and the empty stack, we should fail cleanly instead of corrupting the substitution or throwing an exception.
This unification problem seems straightforward, but the result is a little surprising. Again, the holes and constants are the same objects on both sides of the equals sign, but I’ve drawn them as copies to make the figure easier to read. Clearly, we could make this problem as large as we want by adding more holes to make both sides taller.
The unification has 16 total nodes when there are four holes. What if there are five, six, or seven holes in the problem? We get 32, 64, or 128 nodes in the result, which grows exponentially.
By deduplicating terms the same way we deduplicated quads in chapter 4, we can transform the exponential-size graph in figure 10.7 into this linear-size graph.
Type inference problems can be represented as unification problems in which the generic parameters and omitted types are holes. To make the figure easier to read, I’ve avoided deduplicating repeated uses of the same objects for all the holes and constants.
A binary term representing(1+2)×((1+2)/5). Note that we could make an exactly equal term if we deduplicated the Add node by making both the Mult and Div nodes point to a single Add node.
A binary term representing 6×(6/5). Again, we could optionally have deduplicated the 6 by making the Mult and Div point to a single 6 node.
The anti-unification of the terms in figures 10.10 and 10.11. All the structural similarities are preserved; all the differences have become holes.
Two binary terms, each representing a code change. We can deduce a common change pattern by anti-unifying the two changes.
Summary
- Unification deduces specific solutions by finding values for holes; anti-unification identifies structural similarities between things by creating new holes.
- Unification solves equations on binary terms by gradually building a substitution that fills in the holes or by deducing a contradiction showing that the equation is unsolvable.
- We avoid infinite recursion with an occurs check to ensure that no hole is substituted for a term which contains itself. Remember that holes can alias other holes.
- Robinson’s algorithm has a terrible worst case but acceptable performance on the problems we typically want to solve, so it’s used more frequently than other, more complex algorithms that have better asymptotic performance.
- Unification is often used in compilers for type inference and similar logical deductions.
- By combining unification with backtracking search, we can solve general problems in first-order logic. Languages such as Prolog use this technique.
- The first-order binary-term anti-unification problem is this: given two binary terms, find the most specific term that can be transformed into both by a substitution.
- A recursive anti-unification algorithm identifies common patterns by recursively traversing two terms from the top down, creating substitution dictionaries as it goes.
- This algorithm is worst-case quadratic in time if implemented naïvely but can be made linear with memoization.
- Anti-unification isn’t used as often as unification, but it can be a powerful technique for program analysis, particularly in variations of clone detection.
Fabulous Adventures in Data Structures and Algorithms ebook for free
