Uniqueness of normal forms for shallow term rewrite systems

DOI10.1145/3060144MaRDI QIDQ5278216zbMATH OpenOpenAlexFDO

Authors Nicholas Radcliffe, Luis F. T. Moraes, Rakesh M. Verma

Publication date 13 July 2017

Published in ACM Transactions on Computational Logic (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1607.00431

zbMATH Keywords

decidabilityundecidabilityterm rewrite systemsuniqueness of normal formsflat rewrite systemsshallow rewrite systems

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Abstract: Uniqueness of normal forms ($U{N}^{=}$) is an important property of term rewrite systems. $U{N}^{=}$ is decidable for ground (i.e., variable-free) systems and undecidable in general. Recently it was shown to be decidable for linear, shallow systems. We generalize this previous result and show that this property is decidable for shallow rewrite systems, in contrast to confluence, reachability and other properties, which are all undecidable for flat systems. Our result is also optimal in some sense, since we prove that the $U{N}^{=}$ property is undecidable for two classes of linear rewrite systems: left-flat systems in which right-hand sides are of depth at most two and right-flat systems in which left-hand sides are of depth at most two.

Recommendations

• Uniqueness of normal forms is decidable for shallow term rewrite systems
• A polynomial algorithm for uniqueness of normal forms of linear shallow term rewrite systems
• Unique Normalization for Shallow TRS
• On the Normalization and Unique Normalization Properties of Term Rewrite Systems
• Complexity of Normal Form Properties and Reductions for Term Rewriting Problems Complexity of Normal Form Properties and Reductions for Term Rewriting Problems

Cites work

• scientific article; zbMATH DE number 3730111 (Why is no real title available?)
• scientific article; zbMATH DE number 1962804 (Why is no real title available?)
• A polynomial algorithm for uniqueness of normal forms of linear shallow term rewrite systems
• Algorithms and reductions for rewriting problems
• Complexity of Normal Form Properties and Reductions for Term Rewriting Problems Complexity of Normal Form Properties and Reductions for Term Rewriting Problems
• Deciding confluence of certain term rewriting systems in polynomial time
• New Undecidability Results for Properties of Term Rewrite Systems
• Syntacticness, cycle-syntacticness and shallow theories
• The Confluence Problem for Flat TRSs
• Undecidable properties of flat term rewrite systems
• Unique Normalization for Shallow TRS
• Uniqueness of normal forms is decidable for shallow term rewrite systems
• Variations on the Common Subexpression Problem

Cited in

(9)

• On the Normalization and Unique Normalization Properties of Term Rewrite Systems
• Normalization properties for shallow TRS and innermost rewriting
• Complexity of Normal Form Properties and Reductions for Term Rewriting Problems Complexity of Normal Form Properties and Reductions for Term Rewriting Problems
• Unique Normalization for Shallow TRS
• Uniqueness of normal forms is decidable for shallow term rewrite systems
• Unique normal form property of higher-order rewriting systems
• A polynomial algorithm for uniqueness of normal forms of linear shallow term rewrite systems
• A fast decision procedure for uniqueness of normal forms w.r.t. conversion of shallow term rewriting systems
• Tail reduction free term rewriting systems revisited

This page was built for publication: Uniqueness of normal forms for shallow term rewrite systems

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5278216)