Resumen:
The 2D Dependency Pair Framework for conditional rewrite systems

Fecha

2018-09-17

Editor

Sistedes

Publicado en

Actas de las XVIII Jornadas de Programación y Lenguajes (PROLE 2018)

Licencia Creative Commons

Resumen

Different termination properties of conditional term rewriting systems have been recently described emphasizing the bidimensional nature of the termination behavior of conditional rewriting. The absence of infinite sequences of rewriting steps (termination in the usual sense), provides the horizontal dimension. The absence of infinitely many attempts to launch the subsidiary processes that are required to check the rule’s condition and perform a single rewriting step has been called V-termination and provides the vertical dimension. We have characterized these properties by means of appropriate notions of dependency pairs and dependency chains. In this paper we introduce a 2D Dependency Pair Framework for automatically proving and disproving all these termination properties. Our implementation of the framework as part of the termination tool MU-TERM and the benchmarks obtained so far suggest that the 2D Dependency Pair Framework is currently the most powerful technique for proving operational termination of conditional term rewriting systems.

Descripción

Acerca de Lucas, Salvador

Palabras clave

Conditional Term Rewriting, Dependency Pairs, Operational Termination, Program Analysis
Página completa del ítem
Notificar un error en este resumen
Mostrar cita
Mostrar cita en BibTeX
Descargar cita en BibTeX