An occurs check is a unification test that rejects binding a hole to a term containing that same hole. Without it, contradictory requirements can corrupt a substitution or create a cyclic substitution whose later expansion recurses forever. section 10.1.1 section 10.1.2
Apply the check as part of recursive binary-term unification:
- Look up already-bound holes in both terms. section 10.1.2
- If one term is a hole, search the other term and its bound-hole values for that hole. Fail when it occurs; otherwise add the binding. section 10.1.2
- Deduplicate holes while traversing, because the same hole may appear repeatedly. section 10.1.2
- If both terms are same-named symbols, recursively unify corresponding children; otherwise report failure. section 10.1.2
Rejecting a self-containing stack
Suppose one side requires X to equal 2 while another requires X to equal ImStack(2, X). Binding X to the stack would make X occur inside its own replacement, so the occurs check fails cleanly instead of allowing substitution to recurse without bound. section 10.1.1 section 10.1.2
Listing 10.2 The occurs-check algorithm
abstract record class BinTerm
{
// [...]
public IEnumerable<Hole> AllHoles()
{
var stack = new Stack<BinTerm>(); #1
stack.Push(this);
var seen = new HashSet<Hole>(); #2
while (stack.Count > 0)
{
var current = stack.Pop();
if (current is Hole h && !seen.Contains(h))
{
seen.Add(h);
yield return h;
}
else if (current is Symbol s)
{
stack.Push(s.Right);
stack.Push(s.Left);
}
}
}
}
sealed record class Hole(string Name) : BinTerm
{
public bool OccursIn(BinTerm term, Substitution subst)
{
foreach (Hole hole in term.AllHoles()) #3
{
if (this == hole) #4
return true;
if (hole.IsBoundHole(subst) &&
this.OccursIn(subst[hole], subst)) #5
return true;
}
return false;
}
public override string ToString() => Name;
}
Inspect the iterative hole traversal and duplicate suppression used to implement the occurs check. section 10.1.2
