Finite acyclic theories are unitary (Q1260765)

The paper deals with unification modulo an equational theory \(E\): Given a problem \(P=\{u_ i=v_ i\mid 1\leq i\leq n\}\), a substitution \(\sigma\) is a solution (a unifier) of \(P\) if \(\sigma(u_ i)=_ E\sigma(v_ i)\) for \(1\leq i\leq n\). A set \(M_ E(P)\) of unifiers is a minimal complete set of unifiers if (i) any unifier is an \(E\)-instance of a substitution \(M_ E(P)\) and (ii) \(M_ E(P)\) contains no two substitutions which are \(E\)-equal. Equational theories can be classified according to their minimal complete sets of unifiers. \(E\) is called unitary, finitary or infinitary if for every solvable problem \(P\) such a set \(M_ E(P)\) exists which is a singleton, a finite set or an infinite set, respectively. \(E\) is called nullary if for some solvable \(P\) no \(M_ E(P)\) exists. Almost nothing is known about which properties of \(E\) imply that \(E\) is in any of these classes. Clearly, if \(E=\emptyset\) then we have the free unification problem and \(E\) is unitary by Robinson's unification algorithm. The paper gives a non-trivial class of equational theories which are unitary: Let \(E\) be presented by a finite set \(E'=\{s_ i=t_ i| 1\leq i\leq m\}\). The main result of the paper states that \(E\) is unitary if \(E\) is finite and \(E'\) is acyclic. More precisely, if \(P=\{u=v\}\) consists of one equation only and there exists an \(E\)-unifier of \(P\), then \(M_ E(P)\) is a singleton. To explain this let \(top(s)=f\) if term \(s\) has the form \(s=f(s_ 1,\dots,s_ n)\). Now, \(E\) is finite, if every \(E\)-congruence class is finite. \(E'\) is acyclic of \((\alpha)\) \(top(s_ i)\neq top(t_ i)\) for \(1\leq i\leq m\), \((\beta)\) \(\{top(s_ i),top(t_ i)\}\neq\{top(s_ j),top(t_ j)\}\) for \(i\neq j\) and \((\gamma)\) for any function symbols \(f,g\) there is at most one sequence \(i_ 1,\dots,i_ k\) such that \(f=top(s_{i_ 1})\), \(g=top(t_{i_ k})\), \(s_{i_ j}=t_{i_ j}\) in \(E'\) and \(top(t_{i_ j})=top(s_{i_{j+1}})\). An algorithm is given that on input \(u=v\) computes a most general \(E\)- unifier if its stops and an \(E\)-unifier exists. It is conjectured that the algorithm always stops if an \(E\)-unifier exists. But, it may not stop if an \(E\)-unifier does not exist.