Editing Unification (computer science) (section)

====Proof of termination====
For the proof of termination of the algorithm consider a triple <math>\langle n_{var}, n_{lhs}, n_{eqn}\rangle</math>
where {{math|''n''<sub>''var''</sub>}} is the number of variables that occur more than once in the equation set, {{math|''n''<sub>''lhs''</sub>}} is the number of function symbols and constants
on the left hand sides of potential equations, and {{math|''n''<sub>''eqn''</sub>}} is the number of equations.
When rule ''eliminate'' is applied, {{math|''n''<sub>''var''</sub>}} decreases, since ''x'' is eliminated from ''G'' and kept only in { ''x'' ≐ ''t'' }.
Applying any other rule can never increase {{math|''n''<sub>''var''</sub>}} again.
When rule ''decompose'', ''conflict'', or ''swap'' is applied, {{math|''n''<sub>''lhs''</sub>}} decreases, since at least the left hand side's outermost ''f'' disappears.
Applying any of the remaining rules ''delete'' or ''check'' can't increase {{math|''n''<sub>''lhs''</sub>}}, but decreases {{math|''n''<sub>''eqn''</sub>}}.
Hence, any rule application decreases the triple <math>\langle n_{var}, n_{lhs}, n_{eqn}\rangle</math> with respect to the [[lexicographical order]], which is possible only a finite number of times.

[[Conor McBride]] observes<ref>{{cite journal|last=McBride|first=Conor|title=First-Order Unification by Structural Recursion|journal=Journal of Functional Programming|date=October 2003|volume=13|issue=6|pages=1061–1076|doi=10.1017/S0956796803004957|url=http://strictlypositive.org/unify.ps.gz|access-date=30 March 2012|issn=0956-7968|citeseerx=10.1.1.25.1516|s2cid=43523380 }}</ref> that "by expressing the structure which unification exploits" in a [[dependently typed]] language such as [[Epigram (programming language)|Epigram]], [[Robinson's unification algorithm]] can be made [[recursive on the number of variables]], in which case a separate termination proof becomes unnecessary.