On the descriptive power of term rewriting systems
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.
descriptive power of term rewriting systems
scientific article; zbMATH DE number 3995050
scientific article