First-order binary term unification finds substitutions that make two structured terms identical. Terms contain constants, named holes, and binary symbols; a substitution maps holes to terms and can recursively replace bound holes. section 10.1
The technique combines a compact term representation with recursive substitution:
- Represent constants by value, holes by name, and binary symbols by a name plus left and right child terms. section 10.1
- Store bindings in a mutable dictionary, such as X→t; holes absent from the dictionary remain free. section 10.1
- Substitute recursively through bound holes and symbol children, allocating a new symbol only when a child changes. section 10.1
- Reuse the same mechanism for type inference, where generic parameters and omitted types become holes in binary terms. section 10.3
Unifying immutable-stack terms
Treat an immutable stack as ImStack(left, right). Unifying ImStack(X, ImStack(X, EmptyStack)) with ImStack(2, Y) requires X→2 and Y→ImStack(2, EmptyStack). Replacing both bound holes makes the terms identical. section 10.1
Listing 10.1 The binary term data structure with substitution logic
using Substitution = System.Collections.Generic.Dictionary<Hole, BinTerm>;
abstract record class BinTerm
{
public bool IsBoundHole(Substitution subst) =>
this is Hole h && subst.ContainsKey(h);
public BinTerm Substitute(Substitution subst)
{
if (this.IsBoundHole(subst))
return subst[(Hole)this].Substitute(subst); #1
if (this is Symbol s)
{
var left = s.Left.Substitute(subst);
var right = s.Right.Substitute(subst);
if (!ReferenceEquals(left, s.Left) ||
!ReferenceEquals(right, s.Right))
return new Symbol(s.Name, left, right);
}
return this;
}
}
sealed record class Constant(object Value) : BinTerm
{
public override string ToString() => $"{Value}";
}
sealed record class Hole(string Name) : BinTerm
{
public override string ToString() => Name;
}
sealed record class Symbol(string Name, BinTerm Left, BinTerm Right)
: BinTerm
{
public override string ToString() => $"{Name}({Left},{Right})";
}
The C# term hierarchy and Substitute implementation expose the representation, recursive binding lookup, structural traversal, and selective allocation. section 10.1
Unification also supports logic programming: combined with backtracking, it fills query holes with possible values. It can solve first-order logic problems and encode type-inference constraints. section 10.3
