{"@context":"https:\/\/schema.org\/","@type":"ScholarlyArticle","@id":"#article6740","name":"Termination of linear bounded term rewriting systems","abstract":"For the whole class of linear term rewriting systems and for each integer k, we define k-bounded rewriting as a restriction of the usual notion of rewriting. \r\nWe show that the k-bounded uniform termination, the k-bounded termination, the inverse k-bounded uniform, and the inverse k-bounded problems are decidable.\r\nThe k-bounded class (BO(k)) is, by definition, the set of linear systems for \r\nwhich every derivation can be replaced by a k-bounded derivation. In general, for BO(k) systems, the uniform (respectively inverse uniform) k-bounded termination problem is not equivalent to the uniform (resp. inverse uniform) termination problem, and the k-bounded (respectively inverse k-bounded) termination problem is not equivalent to the termination (respectively inverse termination) problem. \r\nThis leads us to\r\ndefine more restricted classes for which these problems are equivalent: the classes BOLP(k) of \r\nk-bounded 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 k-bounded derivation of length n. \r\nWe define the class BOLP of bounded systems that have the length preservation property as the union of all the BOLP(k) classes.\r\nThe class BOLP contains (strictly) several already known classes of systems:\r\nthe inverse left-basic semi-Thue systems,\r\nthe linear growing term rewriting systems, the inverse Linear-Finite-Path-Ordering systems, the strongly bottom-up systems.","keywords":["Term rewriting","termination","rewriting strategy"],"author":[{"@type":"Person","name":"Durand, Ir\u00e8ne","givenName":"Ir\u00e8ne","familyName":"Durand"},{"@type":"Person","name":"S\u00e9nizergues, G\u00e9raud","givenName":"G\u00e9raud","familyName":"S\u00e9nizergues"},{"@type":"Person","name":"Sylvestre, Marc","givenName":"Marc","familyName":"Sylvestre"}],"position":25,"pageStart":341,"pageEnd":356,"dateCreated":"2010-07-06","datePublished":"2010-07-06","isAccessibleForFree":true,"license":"https:\/\/creativecommons.org\/licenses\/by-nc-nd\/3.0\/legalcode","copyrightHolder":[{"@type":"Person","name":"Durand, Ir\u00e8ne","givenName":"Ir\u00e8ne","familyName":"Durand"},{"@type":"Person","name":"S\u00e9nizergues, G\u00e9raud","givenName":"G\u00e9raud","familyName":"S\u00e9nizergues"},{"@type":"Person","name":"Sylvestre, Marc","givenName":"Marc","familyName":"Sylvestre"}],"copyrightYear":"2010","accessMode":"textual","accessModeSufficient":"textual","creativeWorkStatus":"Published","inLanguage":"en-US","sameAs":"https:\/\/doi.org\/10.4230\/LIPIcs.RTA.2010.341","publisher":"Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik","isPartOf":{"@type":"PublicationVolume","@id":"#volume6209","volumeNumber":6,"name":"Proceedings of the 21st International Conference on Rewriting Techniques and Applications","dateCreated":"2010-07-06","datePublished":"2010-07-06","editor":{"@type":"Person","name":"Lynch, Christopher","givenName":"Christopher","familyName":"Lynch"},"isAccessibleForFree":true,"publisher":"Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik","hasPart":"#article6740","isPartOf":{"@type":"Periodical","@id":"#series116","name":"Leibniz International Proceedings in Informatics","issn":"1868-8969","isAccessibleForFree":true,"publisher":"Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik","hasPart":"#volume6209"}}}