Folding variant narrowing and optimal variant termination

Santiago Escobar, Ralf Sasse, José Meseguer

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

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.

Original languageEnglish (US)
Title of host publicationRewriting Logic and Its Applications - 8th International Workshop, WRLA 2010, Held as a Satellite Event of ETAPS 2010, Revised Selected Papers
Pages52-68
Number of pages17
DOIs
StatePublished - 2010
Event8th International Workshop on Rewriting Logic and Its Applications, WRLA 2010, Held as a Satellite Event of ETAPS 2010 - Paphos, Cyprus
Duration: Mar 20 2010Mar 21 2010

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume6381 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other8th International Workshop on Rewriting Logic and Its Applications, WRLA 2010, Held as a Satellite Event of ETAPS 2010
CountryCyprus
CityPaphos
Period3/20/103/21/10

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Folding variant narrowing and optimal variant termination'. Together they form a unique fingerprint.

Cite this