Unification in Permutative Equational Theories is Undecidable

Abstract

An equational theory E is permutative if in every valid equation s =E t the terms s and t have the same symbols with the same number of occurrences. The class of permutative equational theories includes associativity and commutativity and hence is important for unification theory, for term rewriting systems modulo equational theories and corresponding completion procedures. It is shown in this research note that there is no algorithm that decides E-unifiability of terms for all permutative theories. The proof technique is to provide for every Turing machine M a permutative theory with a confluent term rewriting system such that narrowing on certain terms simulates the Turing machine M.