Substitute is a recursive operation on binary terms. Given a substitution mapping holes to terms, it replaces each bound hole with its mapped term, then substitutes inside that term as well. This recursive descent removes indirect bindings, such as replacing Y with a term that still contains bound hole X. section 10.1 section 10.1.1
The implementation follows a small set of rules:
- Look up a bound hole and recursively substitute into its replacement. section 10.1
- Recurse into both children of a symbol, rebuilding it only when either child changes. section 10.1
- Return holes, constants, and unchanged symbols directly when no replacement is required. section 10.1
- Require an occurs check before creating bindings, because recursive substitutions can otherwise loop forever or produce contradictory results. section 10.1.1
Stack terms
For term1 = ImStack(X, ImStack(X, EmptyStack)) and term2 = ImStack(2, Y), unification can produce X → 2 and Y → ImStack(X, EmptyStack). Applying Substitute recursively yields ImStack(2, ImStack(2, EmptyStack)) for both terms. section 10.1 section 10.1.1
The simple operation has surprising cost. Although ordinary traversal is linear in the size of its result, shared subterms can expand repeatedly: a four-hole example allocates 16 result objects, and n arranged holes can require O(2^n) time and space. section 10.1 section 10.2
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# listing shows the recursive operation, immutable-term reuse, and conditional symbol allocation. section 10.1
