Compilation of combinatory reduction systems.
In: Heering, Jan and Meinke, Karl and Möller, B. and Nipkow, Tobias, eds.
Higher-Order Algebra, Logic, and Term Rewriting.
Lecture Notes in Computer Science, 816.
Combinatory Reduction Systems generalise Term Rewriting Systems. They are powerful enough to express β-reduction of λ-calculus as a single rewrite rule. The additional expressive power has its price --- CRSs are much harder to implement than ordinary TRSs. We propose an abstract machine suitable for executing CRSs. We define what it means to execute an instruction, and give a translation from CRS rules into sequences of instructions. Applying a rewrite rule to a term is realised by initialising the machine with this term, and then successively executing the instructions of the compiled rule.
- Depositors only (login required):