© University of Kent - Contact | Feedback | Legal | FOI | Cookies
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 kbytesBibtex 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}, }