Paper: Cyclic lambda graph rewriting (at LICS 1994)
Authors: Zena Ariola Jan Willem KlopAbstract
Studies cyclic λ-graphs. The starting point is to treat a λ-graph as a system of recursion equations involving λ-terms, and to manipulate such systems in an unrestricted manner, using equational logic, just as is possible for first-order term rewriting. Surprisingly, now the confluence property breaks down in an essential way. Confluence can be restored by introducing a restraining mechanism on the `copying' operation. This leads to a family of λ-graph calculi, which are inspired by the family of λσ-calculi (λ-calculi with explicit substitution). However, these concern acyclic expressions only. In this paper we are not concerned with optimality questions for acyclic λ-reduction. We also indicate how Wadsworth's (1978) interpreter can be simulated in the λ-graph rewrite rules that we propose
BibTeX
@InProceedings{AriolaKlop-Cycliclambdagraphre, author = {Zena Ariola and Jan Willem Klop}, title = {Cyclic lambda graph rewriting}, booktitle = {Proceedings of the Ninth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1994}, year = 1994, editor = {Samson Abramsky}, month = {July}, pages = {416--425}, location = {Paris, France}, publisher = {IEEE Computer Society Press} }