Canonical Forms and Unification.

Abstract
Fay has described a complete T-unification for equational theories T that possess a complete set of reductions as defined by Knuth and Bendix. This algorithm relies essentially on using the narrowing process defined by Lankford. In this paper it is first studied the relations between narrowing and unification and it gives a new version of Fay's algorithm. It then shows how to eliminate many redundancies in this algorithm and gives a sufficient condition for its termination. Finally it is shown how to extend the previous results to various kinds of canonical term rewriting systems.