A logic variable is an unfilled place in a term, called a hole here. A hole is free relative to a substitution when that substitution has no replacement for it. Once the hole is a key in the substitution, it is bound. The same named hole can occur more than once, so filling it imposes the same choice everywhere it occurs. section 10.1 section 10.1.2
A binary term is a named hole, a constant, or a symbol with left and right child terms. A substitution is a dictionary from holes to terms. This is not a variable in the storage-location sense: it is a named part of a structure whose replacement can be deduced. section 10.1
Fill two stack-shaped terms
Consider `ImStack(X, ImStack(X, EmptyStack))` and `ImStack(2, Y)`. Making them equal requires `X → 2` and `Y → ImStack(X, EmptyStack)`. Substitution must continue inside Y’s replacement: X there must become 2 as well. section 10.1 section 10.1.1
Unification compares two terms and builds a substitution or reports failure. Before assigning a hole, it must follow any existing binding and check whether the proposed replacement contains that hole—even through other bound holes. Otherwise, an alias such as `X → Y` followed by a term for Y containing X can make substitution recurse without end. A previously bound hole also cannot silently acquire a contradictory second meaning. section 10.1.2 section 10.1.1
Figure 10.4 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.
The diagram makes the indirect cycle visible: X aliases Y, while Y is assigned a stack containing X. section 10.1.2
Anti-unification uses holes in the opposite direction. Rather than filling them to make terms equal, it preserves shared structure and puts holes where terms differ. For `Mult(Add(1,2), Div(Add(1,2),5))` and `Mult(6, Div(6,5))`, the most specific shared term is `Mult(A, Div(A,5))`. Reusing A records that both differing positions match within each original term; separate substitutions recover the originals. section 10.4 section 10.5
Holes also represent unknown types during type inference: generic parameters and omitted types become terms that unification can resolve. Combined with backtracking search, unification supports logical deductions from rules and facts. section 10.3 section 10.7
