TY - JOUR

T1 - Folding variant narrowing and optimal variant termination

AU - Escobar, Santiago

AU - Sasse, Ralf

AU - Meseguer, José

N1 - Funding Information:
S. Escobar has been partially supported by the EU (FEDER) and the Spanish MEC/MICINN under Grant TIN 2010-21062-C02-02, and by Generalitat Valenciana PROMETEO2011/052. R. Sasse and J. Meseguer have been partially supported by NSF Grants CNS 07-16638, CNS 08-31064, CNS 09-04749, and CCF 09-05584.

PY - 2012/10

Y1 - 2012/10

N2 - Automated reasoning modulo an equational theory E is a fundamental technique in many applications. If E can be split as a disjoint union E∪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 E-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 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-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) variant-complete (generate a complete set of variants for any input term), (ii) minimal (such a set does not have redundant variants), and (iii) are 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 folding variant narrowing that satisfies above properties (i)-(iii); in particular, when E∪Ax has the 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 finitary E∪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.

AB - Automated reasoning modulo an equational theory E is a fundamental technique in many applications. If E can be split as a disjoint union E∪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 E-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 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-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) variant-complete (generate a complete set of variants for any input term), (ii) minimal (such a set does not have redundant variants), and (iii) are 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 folding variant narrowing that satisfies above properties (i)-(iii); in particular, when E∪Ax has the 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 finitary E∪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.

KW - Equational unification

KW - Narrowing modulo

KW - Terminating narrowing strategy

KW - Variants

UR - http://www.scopus.com/inward/record.url?scp=84865582074&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84865582074&partnerID=8YFLogxK

U2 - 10.1016/j.jlap.2012.01.002

DO - 10.1016/j.jlap.2012.01.002

M3 - Article

AN - SCOPUS:84865582074

SN - 1567-8326

VL - 81

SP - 898

EP - 928

JO - Journal of Logic and Algebraic Programming

JF - Journal of Logic and Algebraic Programming

IS - 7-8

ER -