A binary term is an immutable binary tree built from three kinds of node: a named hole, a valued constant, or a named symbol with left and right child terms. Symbols are written name(left, right). This small vocabulary lets a problem about stacks—or one about types—be expressed as a problem about tree structure. section 10.1 section 10.3
Structural equality follows the nodes:
- Constants are equal when their values match; holes are equal when their names match. section 10.1
- Symbols are equal when their names and corresponding children match. All other pairs are unequal. section 10.1
- A substitution maps holes to terms. Applying it follows bindings and substitutes within child terms. section 10.1
Two stacks, one tree equation
Represent a two-item stack as ImStack(X, ImStack(X, EmptyStack)) and another as ImStack(2, Y). Making them equal requires X = 2 and Y = ImStack(2, EmptyStack). The repeated X matters: both occurrences must receive the same term. section 10.1
Unification seeks a substitution that makes two terms equal, or detects that no such substitution exists. An occurs check prevents binding a hole to a term containing that same hole, which would make substitution recurse indefinitely. Anti-unification runs in the other direction: it preserves shared structure and replaces differences with holes, producing a term that can be substituted back into either input. section 10.7
Keep the shared expression shape
Anti-unifying Mult(Add(1,2), Div(Add(1,2),5)) with Mult(6, Div(6,5)) yields Mult(A, Div(A,5)). Substituting Add(1,2) or 6 for A recovers the respective input; reusing A records that the differing part occurs twice in each. section 10.5
Immutable terms do not automatically make substitution cheap. Repeatedly expanding bound holes can produce an exponential-size tree; structural equality and occurs checks can also revisit large subterms. Deduplicating equivalent terms turns the illustrated expanded tree into a linear-size shared graph and permits reference-equality checks. Such optimizations change the representation and costs, not what the terms mean. section 10.2
Figure 10.8 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.
Compare the shared graph with an expanded unification result to see why deduplicating terms can avoid exponential growth. section 10.2
