Unification

Unification finds substitutions for holes that make two terms identical. An immutable stack with unknown elements can be treated as a binary tree: instead of reasoning about stacks, compare its structure and solve for the missing parts. A successful substitution supplies a value for each bound hole; a contradiction means the terms cannot unify. section 10.0 section 10.1

A binary term is a named hole, a constant, or a named symbol with left and right child terms. Constants match when their values match; symbols match when their names and corresponding children match. A substitution maps holes to terms. Applying it recursively matters: a replacement may itself contain a hole that has since been bound. section 10.1 section 10.1.1

Robinson’s first-order binary-term algorithm builds a substitution as it compares terms:

• Look up any holes already bound by the substitution, then succeed immediately if the resulting terms are equal. section 10.1.2
• If either term is an unbound hole, bind it to the other term only if an occurs check finds no path back to that hole through the term or existing bindings. section 10.1.2
• If both terms are symbols with the same name, recursively compare their left children and then their right children. Otherwise, fail. section 10.1.1 section 10.1.2

The lookup and occurs check repair two tempting mistakes. Binding a hole without checking for self-reference can make substitution recurse forever. Checking only for the hole’s literal appearance is still insufficient: one hole can alias another, completing a cycle indirectly. Looking up an existing binding also prevents a later comparison from assigning the same hole a contradictory value. section 10.1.1 section 10.1.2

Performance has a catch. Expanding a substitution into a tree can allocate exponentially many nodes: a four-hole example produces 16 nodes, and adding holes doubles the result. Structural equality and occurs checks add work too. Deduplicating repeated terms can represent the expanding tree as a linear-size graph. Despite its poor worst case, Robinson’s algorithm performs acceptably on typical problems. section 10.2 section 10.7

Unification also combines with backtracking search for first-order logic problems, as in Prolog. Its direction is from general to specific: fill holes to satisfy an equality. Anti-unification goes the other way, replacing differences with holes to expose a common structure. section 10.7

abstract record class BinTerm
{
    [...]
    public BinTerm LookUpBoundHole(Substitution subst) 
    {
        var newTerm = this;
        while (newTerm.IsBoundHole(subst))
            newTerm = subst[(Hole)newTerm];
        return newTerm; #1
    }

    public Substitution? Unify(BinTerm t2) #2
    {
        var subst = new Substitution();
        return Unify(this, t2, subst) ? subst : null;
    }

    private static bool Unify(BinTerm t1, BinTerm t2, Substitution subst) #3
    {
        t1 = t1.LookUpBoundHole(subst);
        t2 = t2.LookUpBoundHole(subst); 
        if (t1 == t2) 
            return true;
        if (t1 is Hole h1 && !h1.OccursIn(t2, subst)) #4
        {
            subst.Add(h1, t2);
            return true;
        }
        if (t2 is Hole h2 && !h2.OccursIn(t1, subst))
        {
            subst.Add(h2, t1);
            return true;
        }
        if (t1 is Symbol s1 && t2 is Symbol s2 && s1.Name == s2.Name)
            return Unify(s1.Left, s2.Left, subst) && 
                Unify(s1.Right, s2.Right, subst);
        return false;
    }
}

The C# implementation makes bound-hole lookup, the occurs check, and recursive unification visible together. section 10.1.2