A bound hole is a hole used as a key in a substitution, so it has an assigned replacement term. A hole absent from that dictionary is free. Substitutions answer the question, “What term goes in this hole?” section 10.1
Bound holes matter throughout binary-term unification:
- Substitute replaces a bound hole with its mapped term and recurses, because that replacement may contain other bound holes. section 10.1
- Unification looks up bound holes before comparing terms, then extends the substitution only for free holes. section 10.1.2
- Occurs checking follows bound-hole mappings recursively, preventing circular substitutions and unbounded recursion. section 10.1.2
A substitution in action
Unifying ImStack(X, ImStack(X, EmptyStack)) with ImStack(2, Y) can produce X → 2 and Y → ImStack(X, EmptyStack). Both terms then substitute to ImStack(2, ImStack(2, EmptyStack)). section 10.1 section 10.1.2
Figure 10.1 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?
Visualize holes as missing pieces of immutable stacks, then treat the substitution as the assignment that makes the structures identical. section 10.1
