School of Computing

Compilation of combinatory reduction systems

Stefan Kahrs

In Jan Heering, Karl Meinke, Bernhard M"oller, and Tobias Nipkow, editors, Higher-Order Algebra, Logic, and Term Rewriting, volume 816 of Lecture Notes in Computer Science, pages 182-196. Springer, September 1993.

Abstract

Combinatory Reduction Systems generalise Term Rewriting Systems. They are powerful enough to express $\beta$-reduction of $\lambda$-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.

Download publication 74 kbytes

Bibtex Record

@conference{574,
author = {Stefan Kahrs},
title = {Compilation of combinatory reduction systems},
month = {September},
year = {1993},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {},
doi = {},
url = {http://www.cs.kent.ac.uk/pubs/1993/574},
    booktitle = {Higher-Order Algebra, Logic, and Term Rewriting},
    editor = {Jan Heering and Karl Meinke and Bernhard M"oller and Tobias Nipkow},
    publisher = {Springer},
    refereed = {yes},
    series = {Lecture Notes in Computer Science},
    volume = {816},
}

School of Computing, University of Kent, Canterbury, Kent, CT2 7NF

Enquiries: +44 (0)1227 824180 or contact us.

Last Updated: 21/03/2014