Implementing first-order rewriting with constructor systems (Q1112601): Difference between revisions

Most first-order term rewriting systems used in functional programming require argument patterns to be built from constructor symbols in order to allow simple efficient implementations, although more general classes such as linear nonambiguous systems [\textit{G. Huet} and \textit{J.-J. Levy}, ``Computations in nonambiguous linear term rewriting systems'', Tech. Rep. 359, INRIA, France (1979)] have greater expressive power. In Inf. Process. Lett. 20, 83-85 (1985; Zbl 0566.68036) we presented a technique for implementing linear nonambiguous systems with an underlying engine that uses constructor-based definitions and showed that the required translation causes an expansion in system size that is quadratic in the worst case, but relatively small in realistic cases such as the LISP interpreter of \textit{C. M. Hoffmann} and \textit{M. O'Donnell} [ACM Trans. Program. Lang. Syst. 4, 83-112 (1982; Zbl 0481.68008)]. We show that the technique is applicable to three other classes - where applicability means preservation of defining characteristics and normal forms - if rewriting in the translated system respects a weak ordering on the new equations. The three classes are semi-regular (confluent non- overlapping), canonical (confluent terminating) and confluent call-by- value systems.