On interreduction of semi-complete term rewriting systems (Q5941203): Difference between revisions
From MaRDI portal
Created a new Item |
Added link to MaRDI item. |
||
links / mardi / name | links / mardi / name | ||
Revision as of 01:49, 30 January 2024
scientific article; zbMATH DE number 1635368
Language | Label | Description | Also known as |
---|---|---|---|
English | On interreduction of semi-complete term rewriting systems |
scientific article; zbMATH DE number 1635368 |
Statements
On interreduction of semi-complete term rewriting systems (English)
0 references
20 August 2001
0 references
For a complete, i.e., confluent and terminating Term Rewriting System (TRS) it is well-known that simplification (also called interreduction) into an equivalent canonical, i.e., complete and interreduced TRS is easily possible. This can be achieved by first normalizing all right-hand sides of the TRS and then deleting all rules with a reducible left-hand side. Here we investigate the logical and operational preservation properties of the same simplification operations for semi-complete, i.e., confluent and weakly terminating TRSs. Surprisingly, it turns out that for semi-complete TRSs these simplifications are neither operationally harmless nor logically correct: Semi-completeness may get lost and the induced equational theory need not be preserved. We also provide sufficient criteria for the preservation of semi-completeness and of the induced equational theory. In particular, we show that orthogonal TRSs enjoy all these preservation properties. In the general case, for a given semi-complete TRS an equivalent semi-canonical, i.e., semi-complete and interreduced system need not even exist.
0 references
theory of computation
0 references
term rewriting
0 references
confluence
0 references
termination
0 references
semi-completeness
0 references
right-normalization
0 references
interreduction
0 references