Some Undecidable Approximations of TRSs

J. Ketema

Research output: Contribution to JournalArticleAcademicpeer-review

Abstract

In this paper we study the decidability of reachability, normalisation, and neededness in n-shallow and n-growing TRSs. In an n-growing TRS, a variable that occurs both on the left- and right-hand side of a rewrite rule must be at depth n on the left-hand side and at depth greater than n on the right-hand side. In an n-shallow TRS, a variable that occurs both on the left- and right-hand side of a rewrite rule must be at depth n on both sides. The n-growing and n-shallow TRSs are generalisations of the growing and shallow TRSs as introduced by Jacquemard and Comon. For both shallow and growing TRSs reachability, normalisation, and (in the orthogonal case) neededness are decidable. However, as we show, these results do not generalise to n-growing and n-shallow TRSs. Consequently, no algorithm exists that performs a needed reduction strategy in n-growing or n-shallow TRSs. © 2005 Elsevier B.V. All rights reserved.
Original languageEnglish
Pages (from-to)51-63
JournalElectronic Notes in Theoretical Computer Science
Volume124
DOIs
Publication statusPublished - 2005

Bibliographical note

DBLP:journals/entcs/KetemaKO05
Proceedings title: Proceedings of the 4th International Workshop on Reduction Strategies in Rewriting and Programming (WRS 2004)
Publisher: Elsevier

Fingerprint Dive into the research topics of 'Some Undecidable Approximations of TRSs'. Together they form a unique fingerprint.

Cite this