Folding variant narrowing and optimal variant termination (Q1931909)

This paper presents a detailed discussion of narrowing strategies modulo axioms. If an equational theory can be represented as a disjoint union \(E\cup Ax\) of a set of equations \(E\) and a set of equational axioms \(Ax\), where \(E\) is confluent, terminating, sort-decreasing, and coherent modulo \(Ax\), then narrowing with \(E\) modulo \(Ax\) provides a complete \((E\cup Ax)\)-unification algorithm. Full narrowing is quite inefficient. Therefore, to reduce the search space, narrowing strategies are employed. It is desirable that a narrowing strategy retains the completeness property of unrestricted narrowing. In particular, for narrowing with \(E\) modulo \(Ax\), one would wish to have an efficient strategy which is complete for computing \(E\cup Ax\) unifiers. Another potential benefit of narrowing strategies is that they may sometimes terminate when the full narrowing generates an infinite search space. The paper studies such strategies for narrowing modulo axioms. Their definition is based on the notion of \textit{variant}, introduced in [\textit{H.~Comon-Lundh} and \textit{S.~Delaune}, Lect. Notes Comput. Sci. 3467, 294--307 (2005; Zbl 1078.68059)]. The notions of variant-complete and optimally variant-terminating strategies are introduced. Variant-complete strategies compute a complete set of variants. Optimally variant-terminating ones terminate iff there is a finite complete set of variants. For narrowing with \(E\) modulo \(Ax\), variant-complete and optimally variant-terminating strategies can be used to construct complete \((E\cup Ax)\)-unification algorithms (if \(E\) is confluent, terminating, sort-decreasing, and coherent modulo \(Ax\)). To characterize concrete instances of variant-complete and optimally variant-terminating strategies, the authors associate to each narrowing strategy its folding version. While the strategy specifies which narrowing steps are allowed from a term, its folding version avoids repeated generation of variants. It is proved that the folding version of a complete strategy is variant-complete. Moreover, if the strategy satisfies the additional property of being a variant-narrowing strategy, then its folding version, folding-variant narrowing, is both variant-complete and optimally variant-terminating. Folding-variant narrowing provides a complete, minimal, and terminating algorithm for computing \((E\cup Ax)\)-unifiers, when \(E\cup Ax\) has the finite variant property (any term has a finite complete set of variants). Moreover, there is an algorithm which, under certain assumptions on \(E\cup Ax\), can report whether this set has the finite variant property. Applications of folding-variant narrowing in unification theory, cryptographic protocol verification, proofs of termination, confluence and coherence of a set of rewrite rules modulo an equational theory are also discussed.