- -

Folding variant narrowing and optimal variant termination

RiuNet: Institutional repository of the Polithecnic University of Valencia

Share/Send to

Cited by

Statistics

Folding variant narrowing and optimal variant termination

Show simple item record

Files in this item

dc.contributor.author Escobar Román, Santiago es_ES
dc.contributor.author Sasse, Ralf es_ES
dc.contributor.author Meseguer, José es_ES
dc.date.accessioned 2014-05-23T07:17:45Z
dc.date.issued 2012-11
dc.identifier.issn 1567-8326
dc.identifier.uri http://hdl.handle.net/10251/37697
dc.description.abstract Automated reasoning modulo an equational theory E is a fundamental technique in many applications. If E can be split as a disjoint union E u 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 u 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 u 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. © 2012 Elsevier Inc. All rights reserved es_ES
dc.description.sponsorship 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. en_EN
dc.format.extent 31 es_ES
dc.language Inglés es_ES
dc.publisher Elsevier es_ES
dc.relation EU (FEDER) es_ES
dc.relation Spanish MEC/MICINN [TIN 2010-21062-C02-02] es_ES
dc.relation Generalitat Valenciana [PROMETEO2011/052] es_ES
dc.relation NSF [CNS 07-16638, CNS 08-31064, CNS 09-04749, CCF 09-05584] es_ES
dc.relation.ispartof Journal of Logic and Algebraic Programming es_ES
dc.rights Reserva de todos los derechos es_ES
dc.subject Narrowing modulo es_ES
dc.subject Terminating narrowing strategy es_ES
dc.subject Variants es_ES
dc.subject Equational unification es_ES
dc.subject.classification LENGUAJES Y SISTEMAS INFORMATICOS es_ES
dc.title Folding variant narrowing and optimal variant termination es_ES
dc.type Artículo es_ES
dc.identifier.doi 10.1016/j.jlap.2012.01.002
dc.rights.accessRights Abierto es_ES
dc.contributor.affiliation Universitat Politècnica de València. Departamento de Sistemas Informáticos y Computación - Departament de Sistemes Informàtics i Computació es_ES
dc.description.bibliographicCitation Escobar Román, S.; Sasse, R.; Meseguer, J. (2012). Folding variant narrowing and optimal variant termination. Journal of Logic and Algebraic Programming. 81(7):898-928. doi:10.1016/j.jlap.2012.01.002 es_ES
dc.description.accrualMethod Senia es_ES
dc.relation.publisherversion http://dx.doi.org/10.1016/j.jlap.2012.01.002 es_ES
dc.description.upvformatpinicio 898 es_ES
dc.description.upvformatpfin 928 es_ES
dc.type.version info:eu repo/semantics/publishedVersion es_ES
dc.description.volume 81 es_ES
dc.description.issue 7 es_ES
dc.relation.senia 241068


This item appears in the following Collection(s)

Show simple item record