On the correspondence between two classes of reduction systems (Q1059392): Difference between revisions

We consider the relationship between two classes of term rewriting systems. In one class, there is a sharp distinction between data constructors and computable functions, which is absent, in the other. Both classes contain systems described by sets of left-linear rules without critical pairs in the sense of Knuth-Bendix. We show that although the class based on constructors appears to be a special case, it is in fact powerful enough to simulate the larger class, and thus certain problems such as sequentiality in the larger class can be reduced via simulation to the technically simpler environment of constructor systems.