Bottom-up rewriting for words and terms

TL;DR

This paper introduces the concept of bottom-up rewriting for linear term rewriting systems, analyzes its properties, and defines subclasses with decidable membership, expanding understanding of recognizability preservation.

Contribution

It defines bottom-up rewriting for linear systems, analyzes its complexity, and introduces subclasses with decidable membership, including a polynomial sufficient condition for SBU systems.

Findings

Bottom-up rewriting preserves recognizability effectively.

Membership in the BU class is undecidable.

Decidable subclasses SBU(k) are introduced with polynomial conditions.

Abstract

For the whole class of linear term rewriting systems, we define \emph{bottom-up rewriting} which is a restriction of the usual notion of rewriting. We show that bottom-up rewriting effectively inverse-preserves recognizability and analyze the complexity of the underlying construction. The Bottom-Up class (BU) is, by definition, the set of linear systems for which every derivation can be replaced by a bottom-up derivation. Membership to BU turns out to be undecidable, we are thus lead to define more restricted classes: the classes SBU(k), k in N of Strongly Bottom-Up(k) systems for which we show that membership is decidable. We define the class of Strongly Bottom-Up systems by SBU = U_{k in \} SBU(k). We give a polynomial sufficient condition for a system to be in $\SBU$. The class SBU contains (strictly) several classes of systems which were already known to inverse preserve recognizability: the inverse left-basic semi-Thue systems (viewed as unary term rewriting systems), the linear growing term rewriting systems, the inverse Linear-Finite-Path-Ordering systems.