Bottom-up rewriting for words and terms. (March 2015)

• Record Type: Journal Article
• Authors: Durand, I.; Sénizergues, G.
• Is Part Of: Journal of symbolic computation. Volume 67(2015)
• Page Start: 93
• Page End: 121
• Publication Date: 2015-03
• Subjects: 68Q42 -- 03D03 -- 03D40; Term rewriting systems -- Semi-Thue systems -- Regularity preservation -- Accessibility problem; Mathematics -- Data processing -- Periodicals; Numerical analysis -- Data processing -- Periodicals; Automatic programming (Computer science) -- Periodicals; Mathématiques -- Informatique -- Périodiques; Analyse numérique -- Informatique -- Périodiques; Programmation automatique -- Périodiques; Automatic programming (Computer science); Mathematics -- Data processing; Numerical analysis -- Data processing; Periodicals; Electronic journals; 510.285
• DOI: 10.1016/j.jsc.2014.06.001
• Languages: English
• ISSNs: 0747-7171

Abstract

Abstract: For the whole class of linear term rewriting systems, we define bottom-up rewriting which is a restriction of the usual notion of rewriting. We show that bottom-up rewriting effectively inverse-preserves recognizability. 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. Since membership to BU turns out to be undecidable, we are led to define more restricted classes: the classes SBU ( k ), k ∈ 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 = ⋃ k ∈ N SBU ( k ) . We give a polynomial-time 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.