- -

Innermost Termination of Context-Sensitive Rewriting

RiuNet: Institutional repository of the Polithecnic University of Valencia

Share/Send to

Cited by

Statistics

Innermost Termination of Context-Sensitive Rewriting

Show simple item record

Files in this item

dc.contributor.author Alarcón Jiménez, Beatriz
dc.contributor.author Lucas, Salvador
dc.date.accessioned 2011-05-04T07:04:06Z
dc.date.available 2011-05-04T07:04:06Z
dc.date.issued 2011-05-04
dc.identifier.uri http://hdl.handle.net/10251/10796
dc.description.abstract Innermost context-sensitive rewriting (CSR) has been proved useful for modeling the computational behavior of programs of algebraic languages like Maude, OBJ, etc, which incorporate an innermost strategy which is used to break down the nondeterminism which is inherent to reduction relations. Furthermore, innermost termination of rewriting is often easier to prove than termination. Thus, under appropriate conditions, a useful strategy for proving termination of rewriting is trying to prove termination of innermost rewriting. This phenomenon has also been investigated for context-sensitive rewriting. Up to now, only few transformation-based methods have been proposed and used to (specifically) prove termination of innermost CSR. Powerful and e cient techniques for proving (innermost) termination of (unrestricted) rewriting like the dependency pair framework have not been considered yet. In this work, we investigate the adaptation of the dependency pair framework to innermost CSR. We provide a suitable notion of innermost context-sensitive dependency pair and show how to extend and adapt the main notions which conform the framework (chain, termination problem, processor, etc.). Thanks to the innermost context-sensitive dependency pairs, we can now use powerful techniques for proving termination of innermost CSR. This is made clear by means of some benchmarks showing that our techniques dramatically improve over previously existing transformational techniques, thus establishing the new state-of-the-art in the area. We have implemented them as part of the termination tool MU-TERM. es_ES
dc.language Inglés es_ES
dc.relation.ispartofseries ELP-TR;AL2011
dc.rights Reserva de todos los derechos es_ES
dc.subject Context-sensitive rewriting es_ES
dc.subject Dependency pairs
dc.subject Term rewriting
dc.subject Program termination
dc.title Innermost Termination of Context-Sensitive Rewriting es_ES
dc.type Informe es_ES
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ó
dc.description.bibliographicCitation Alarcón Jiménez, B.; Lucas, S. (2011). Innermost Termination of Context-Sensitive Rewriting. http://hdl.handle.net/10251/10796 es_ES


This item appears in the following Collection(s)

Show simple item record