= Equational unification
<Equational unification> asks for a <first-order substitution> making two <first-order terms> equal under specified <identity (mathematics)>[identities], rather than requiring them to become literally the same <first-order term>. Writing $=_E$ for equality justified by those <identity (mathematics)>[identities], a solution $\sigma$ satisfies $s\sigma=_E t\sigma$.
For example, the <first-order terms> $f(a,b)$ and $f(b,a)$ have no syntactic <unifier> when $a,b$ are distinct <constant symbols> and $f$ is an uninterpreted binary <function symbol>. If the specified <identity (mathematics)>[identity] is commutativity, $f(x,y)=f(y,x)$, then the unchanged <first-order terms> are already equal modulo that <identity (mathematics)>[identity]: the empty <first-order substitution> is an equational <unifier>.
The <identity (mathematics)>[identity] set changes the problem. Ordinary <first-order unification> can decompose equal outer constructors because equality of free <first-order terms> forces equality of corresponding arguments. Modulo commutativity, argument positions can be exchanged, so that decomposition alone would reject legitimate solutions. A useful implementation must state its <identity (mathematics)>[identities] and its notion of solution, rather than treating equality of interpreted values as syntactic equality.
Back to article page
