Some Undecidable Approximations of TRSs

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.