Unification

Unification seeks substitutions for variables that make symbolic terms identical. First-order unification compares matching constructors recursively; an occurs check rejects substitutions that would make a variable contain itself.

First-order unification seeks substitutions making first-order terms identical. Constructor decomposition and the occurs check produce a most general unifier when one exists.

A most general unifier is a unifying substitution through which every other unifier factors by a further substitution. It records exactly the equality constraints forced by the terms.