TY - GEN
T1 - Folding variant narrowing and optimal variant termination
AU - Escobar, Santiago
AU - Sasse, Ralf
AU - Meseguer, José
N1 - 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 - 2010
Y1 - 2010
N2 - If a set of equations EUAx is such that E is confluent, terminating, and coherent modulo Ax, narrowing with E modulo Ax provides a complete EUAx-unification algorithm. However, except for the hopelessly inefficient case of full narrowing, nothing 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. In this work we propose an effective strategy based on the idea of the EUAx-variants of a term that we call folding variant narrowing. This strategy is complete, both for computing EUAx-unifiers and for computing a minimal complete set of variants for any input term. And it is optimally variant terminating in the sense of terminating for an input term t iff t has a finite, complete set of variants. The applications of folding variant narrowing go beyond providing a complete EUAx-unification algorithm: computing the EUAx-variants of a term may be just as important as computing EUAx-unifiers in recent applications of folding variant narrowing such as termination methods modulo axioms, and checking confluence and coherence of rules modulo axioms.
AB - If a set of equations EUAx is such that E is confluent, terminating, and coherent modulo Ax, narrowing with E modulo Ax provides a complete EUAx-unification algorithm. However, except for the hopelessly inefficient case of full narrowing, nothing 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. In this work we propose an effective strategy based on the idea of the EUAx-variants of a term that we call folding variant narrowing. This strategy is complete, both for computing EUAx-unifiers and for computing a minimal complete set of variants for any input term. And it is optimally variant terminating in the sense of terminating for an input term t iff t has a finite, complete set of variants. The applications of folding variant narrowing go beyond providing a complete EUAx-unification algorithm: computing the EUAx-variants of a term may be just as important as computing EUAx-unifiers in recent applications of folding variant narrowing such as termination methods modulo axioms, and checking confluence and coherence of rules modulo axioms.
UR - http://www.scopus.com/inward/record.url?scp=78349254194&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=78349254194&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-16310-4_5
DO - 10.1007/978-3-642-16310-4_5
M3 - Conference contribution
AN - SCOPUS:78349254194
SN - 3642163092
SN - 9783642163098
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 52
EP - 68
BT - Rewriting Logic and Its Applications - 8th International Workshop, WRLA 2010, Held as a Satellite Event of ETAPS 2010, Revised Selected Papers
T2 - 8th International Workshop on Rewriting Logic and Its Applications, WRLA 2010, Held as a Satellite Event of ETAPS 2010
Y2 - 20 March 2010 through 21 March 2010
ER -