On the descriptive power of term rewriting systems

DOI10.1016/S0747-7171(86)80017-7MaRDI QIDQ1819932zbMATH OpenFDO

Authors Jürgen Avenhaus

Publication date 1986

Published in Journal of Symbolic Computation (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/S0747-7171(86)80017-7

zbMATH Keywords

descriptive power of term rewriting systemsstring rewriting systems

Mathematics Subject Classification ID

Abstract data types; algebraic specification (68Q65) Symbolic computation and algebraic computation (68W30)

Review text

The paper discusses the descriptive power of term rewriting systems in the following sense: Let T be the set of terms over a fixed signature. The pair (\(\sim,N)\), where \(\sim\) is a congruence on T and N is a set of representatives for \(\sim\), is said to be definable by a term rewriting system (TRS) R if \(\sim\) is the congruence generated by R and N is the set of R-normal forms. The paper gives necessary and sufficient conditions on (\(\sim,N)\) to be definable by a - possibly infinite - TRS. It turns out that (\(\sim,N)\) may be definable by a TRS but not by a uniquely terminating (i.e. complete) one. So the descriptive power of weakly uniquely terminating TRSs (i.e. infinite derivation sequences may exist) is strictly greater than that of uniquely terminating ones. In order to find a minimal TRS defining (\(\sim,N)\) the reduced TRS R for (\(\sim,N)\) is introduced. It may fail to define (\(\sim,N)\), but if every term has an R-normal form then R is a minimal TRS defining (\(\sim,N)\). For string rewriting systems (\(\sim,N)\) is definable by a SRS iff N is subword-closed. The conjecture that every such (\(\sim,N)\) is definable by a uniquely terminating SRS is disproved.

Recommendations

• About the descriptive power of certain classes of finite string-rewriting systems
• scientific article; zbMATH DE number 4006231
• scientific article; zbMATH DE number 1088026
• scientific article; zbMATH DE number 1118018
• On sufficient-completeness and related properties of term rewriting systems
• Foundations of Software Science and Computation Structures
• scientific article; zbMATH DE number 2201367
• scientific article; zbMATH DE number 4090779
• scientific article; zbMATH DE number 177826
• scientific article; zbMATH DE number 1722708

Cites work

• About the rewriting systems produced by the Knuth-Bendix completion algorithm
• Algebraic simplification
• Complete Sets of Reductions for Some Equational Theories
• Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
• scientific article; zbMATH DE number 3299786 (Why is no real title available?)

Cited in

(4)

• scientific article; zbMATH DE number 4016185 (Why is no real title available?)
• Algebraic semantics and complexity of term rewriting systems
• scientific article; zbMATH DE number 2201367 (Why is no real title available?)
• Lambda-definable term rewriting systems

This page was built for publication: On the descriptive power of term rewriting systems

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