A simple, efficient, and correct compilation technique for left-linear Term Rewriting Systems (TRSs) is presented. TRSs are compiled into Minimal Term Rewriting Systems (MTRSs), a subclass of TRSs, presented in [KW95d]. In MTRSs, the rules have such a simple form that they can be seen as instructions for an easily implementable abstract machine, the Abstract Rewriting Machine (ARM). In the correctness proof, it is shown that the MTRS resulting from compilation of a TRS simulates neither too much (soundness) nor too little (completeness), nor does it introduce unwarranted infinite sequences (termination conservation). The compiler and its correctness proof are largely independent of the reduction strategy.

Processors (acm D.3.4), Applicative Programming (acm D.1.1), Logic Programming (acm D.1.6)
Compilers and interpreters (msc 68N20), Models of computation (Turing machines, etc.) (msc 68Q05), Grammars and rewriting systems (msc 68Q42), Abstract data types; algebraic specification (msc 68Q65)
CWI
Department of Computer Science [CS]
Extensible programming environments

Kamperman, J.F.T, & Walters, H.R. (1996). Simulating TRSs by minimal TRSs : a simple, efficient, and correct compilation technique. Department of Computer Science [CS]. CWI.