Minimal term rewriting systems

Formally well-founded compilation techniques for Term Rewriting Systems (TRSs) are presented. TRSs are compiled into Minimal Term Rewriting Systems (MTRSs), a subclass of TRSs in which all rules have an extremely simple form. A notion of simulation of (rewrite) relations is presented, under which an MTRSs can be said to simulate a TRS. The MTRS rules can be directly interpreted as instructions for an extremely simple Abstract Rewriting Machine (ARM). Favourable practical results have already been obtained with an earlier version of ARM.