Decidability for left-linear growing term rewriting systems.

DOI10.1006/inco.2002.3157zbMath1049.68075OpenAlexW642373709MaRDI QIDQ1400714

Takashi Nagaya, Yoshihito Toyama

Publication date: 2002

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://semanticscholar.org/paper/4c2bb7213bcec5626db23c44b7dec1a63624e235

zbMATH Keywords

sequentialityjoinabilityreachabiilty

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Related Items

Controlled Term Rewriting ⋮ Term Rewriting with Prefix Context Constraints and Bottom-Up Strategies ⋮ On tree automata that certify termination of left-linear term rewriting systems ⋮ Modularity in term rewriting revisited ⋮ First-order theory of rewriting for linear variable-separated rewrite systems: automation, formalization, certification ⋮ Levels of undecidability in rewriting ⋮ Match-Bounds with Dependency Pairs for Proving Termination of Rewrite Systems ⋮ Formalized Proofs of the Infinity and Normal Form Predicates in the First-Order Theory of Rewriting ⋮ New Undecidability Results for Properties of Term Rewrite Systems ⋮ Normalization properties for shallow TRS and innermost rewriting ⋮ Decidable call-by-need computations in term rewriting ⋮ Beyond Dependency Graphs ⋮ Undecidable properties of flat term rewrite systems ⋮ Bottom-up rewriting for words and terms ⋮ Unique Normalization for Shallow TRS ⋮ Match-bounds revisited ⋮ Non-linear rewrite closure and weak normalization ⋮ Decidability of Innermost Termination and Context-Sensitive Termination for Semi-Constructor Term Rewriting Systems

Cites Work

• Deterministic tree pushdown automata and monadic tree rewriting systems
• Linear generalized semi-monadic rewrite systems effectively preserve recognizability
• Bottom-up tree pushdown automata: Classification and connection with rewrite systems
• Decidable call-by-need computations in term rewriting
• Sequentiality, monadic second-order logic and tree automata.
• NV-Sequentiality: A Decidable Condition for Call-by-Need Computations in Term-Rewriting Systems
• Term Rewriting and All That
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item