Files in this item



application/pdfjlap-postprint-fixes.pdf (443kB)
(no description provided)PDF


Title:Folding Variant Narrowing and Optimal Variant Termination
Author(s):Escobar, Santiago; Sasse, Ralf; Meseguer, José
Subject(s):Narrowing modulo
Terminating Narrowing Strategy
Equational Unification
Abstract: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$.
Issue Date:2012
Citation Info:Journal of Logic and Algebraic Programming
Publication Status:published or submitted for publication
Peer Reviewed:is peer reviewed
Date Available in IDEALS:2012-07-02

This item appears in the following Collection(s)

Item Statistics