A substitution answers a concrete question: what term goes in each hole? For binary terms, it is a mutable dictionary from holes to terms, written X→t. A hole in the dictionary is bound; an absent hole is free. Applying a substitution replaces bound holes recursively, because a replacement term may contain other bound holes. section 10.1 section 10.1.1
Making two stacks equal
Consider ImStack(X,ImStack(X,EmptyStack)) and ImStack(2,Y). The substitution X→2, Y→ImStack(X,EmptyStack) makes both terms ImStack(2,ImStack(2,EmptyStack)). Replacing Y alone is not enough: its replacement still contains X. section 10.1 section 10.1.1
Constructing a valid substitution takes more care than assigning each hole on sight:
- Look up an already-bound hole before comparing terms or adding a binding. Otherwise, a later assignment can silently contradict its earlier meaning. section 10.1.2
- Before binding a hole to a term, check whether that hole occurs in the term, including through other bindings. X→Y followed by Y→ImStack(X,EmptyStack) would make substitution recurse forever. section 10.1.2
- When two symbols have the same name, unify their corresponding children using the same growing substitution; unequal constants or incompatible structures fail. section 10.1.1 section 10.1.2
Substitution can be expensive even when the input terms look small. In one family of unification problems, fully expanding n bound holes produces a binary tree of O(2ⁿ) objects. Deduplicating repeated terms instead represents that result as a linear-size graph. section 10.2
Substitutions in the opposite direction
Anti-unifying Mult(Add(1,2),Div(Add(1,2),5)) and Mult(6,Div(6,5)) yields Mult(A,Div(A,5)). Two substitutions recover the inputs: one maps A→Add(1,2), the other A→6. Reusing A preserves the repeated relationship between the differing parts. section 10.5
The same mechanism serves other problems: type inference treats unknown types as holes, while logic programming applies discovered bindings to rules and combines unification with backtracking search. section 10.3
