On the descriptive power of term rewriting systems
type: Item
instance of: scholarly article
title: On the descriptive power of term rewriting systems
zbMATH Open document ID: 0614.68032
DOI: 10.1016/S0747-7171(86)80017-7
author: Jürgen Avenhaus
published in: Journal of Symbolic Computation
publication date: 1986-01-01T00:00:00Z
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.
Mathematics Subject Classification ID: 68W30
Mathematics Subject Classification ID: 68Q65
zbMATH DE Number: 3995050
zbMATH Keywords: descriptive power of term rewriting systems
zbMATH Keywords: string rewriting systems
MaRDI profile type: Publication
cites work: Algebraic simplification
cites work: Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
cites work: Q5581665
cites work: About the rewriting systems produced by the Knuth-Bendix completion algorithm
cites work: Complete Sets of Reductions for Some Equational Theories
Recommended article: About the descriptive power of certain classes of finite string-rewriting systems
Recommended article: Q3757892
Recommended article: Q4364373
Recommended article: Q4376886
Recommended article: On sufficient-completeness and related properties of term rewriting systems
Recommended article: Foundations of Software Science and Computation Structures
Recommended article: Q5313795
Recommended article: Q3817590
Recommended article: Q4038704
Recommended article: Q2778880
description: scientific article; zbMATH DE number 3995050