Durand, Irène ;
Sénizergues, Géraud ;
Sylvestre, Marc
Termination of linear bounded term rewriting systems
Abstract
For the whole class of linear term rewriting systems and for each integer k, we define kbounded rewriting as a restriction of the usual notion of rewriting.
We show that the kbounded uniform termination, the kbounded termination, the inverse kbounded uniform, and the inverse kbounded problems are decidable.
The kbounded class (BO(k)) is, by definition, the set of linear systems for
which every derivation can be replaced by a kbounded derivation. In general, for BO(k) systems, the uniform (respectively inverse uniform) kbounded termination problem is not equivalent to the uniform (resp. inverse uniform) termination problem, and the kbounded (respectively inverse kbounded) termination problem is not equivalent to the termination (respectively inverse termination) problem.
This leads us to
define more restricted classes for which these problems are equivalent: the classes BOLP(k) of
kbounded systems that have the length preservation property. By definition, a system is BOLP(k) if every derivation of length n can be replaced by a kbounded derivation of length n.
We define the class BOLP of bounded systems that have the length preservation property as the union of all the BOLP(k) classes.
The class BOLP contains (strictly) several already known classes of systems:
the inverse leftbasic semiThue systems,
the linear growing term rewriting systems, the inverse LinearFinitePathOrdering systems, the strongly bottomup systems.
BibTeX  Entry
@InProceedings{durand_et_al:LIPIcs:2010:2662,
author = {Ir{\`e}ne Durand and G{\'e}raud S{\'e}nizergues and Marc Sylvestre},
title = {{Termination of linear bounded term rewriting systems}},
booktitle = {Proceedings of the 21st International Conference on Rewriting Techniques and Applications},
pages = {341356},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783939897187},
ISSN = {18688969},
year = {2010},
volume = {6},
editor = {Christopher Lynch},
publisher = {Schloss DagstuhlLeibnizZentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2010/2662},
URN = {urn:nbn:de:0030drops26625},
doi = {http://dx.doi.org/10.4230/LIPIcs.RTA.2010.341},
annote = {Keywords: Term rewriting, termination, rewriting strategy}
}
Keywords: 

Term rewriting, termination, rewriting strategy 
Seminar: 

Proceedings of the 21st International Conference on Rewriting Techniques and Applications

Issue date: 

2010 
Date of publication: 

06.07.2010 