Some Undecidable Approximations of TRSs

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.