On interreduction of semi-complete term rewriting systems (Q5941203)

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.