Folding Variant Narrowing and Optimal Variant Termination

Automated reasoning modulo an equational theory $\caE$ is a fundamental technique in many applications. If $\caE$ can be split as a disjoint union $E\!\cup \!Ax$ in such a way that $E$ is confluent, terminating, sort-decreasing, and coherent modulo a set of equational axioms $Ax$, narrowing with $E$ modulo $Ax$ provides a complete $\caE$-unification algorithm. However, except for the hopelessly inefficient case of full narrowing, little seems to be known about effective narrowing strategies in the general modulo case beyond the quite depressing observation that basic narrowing is \emph{incomplete} modulo $AC$. Narrowing with equations $E$ modulo axioms $Ax$ can be turned into a practical automated reasoning technique by systematically exploiting the notion of $E,Ax$-\emph{variants} of a term. After reviewing such a notion, originally proposed by Comon-Lundh and Delaune, and giving various necessary and/or sufficient conditions for it, we explain how narrowing strategies can be used to obtain narrowing algorithms modulo axioms that are: (i) \emph{variant-complete} (generate a complete set of variants for any input term), (ii) \emph{minimal} (such a set does not have redundant variants), and (iii) \emph{optimally variant-terminating} (the strategy will terminate for an input term $t$ iff $t$ has a finite complete set of variants). We define a strategy called \emph{folding variant narrowing} that satisfies above properties (i)--(iii); in particular, when $E \cup Ax$ has the \emph{finite variant property}, that is, when any term $t$ has a finite complete set of variants, this strategy terminates on any input term and provides a \emph{finitary} $E \cup Ax$-unification algorithm. We also explain how folding variant narrowing has a number of interesting applications in areas such as unification theory, cryptographic protocol verification, and proofs of termination, confluence and coherence of a set of rewrite rules $R$ modulo an equational theory $E$.published or submitted for publicationis peer reviewe