Ninth Annual IEEE Symposium on

Logic in Computer Science (LICS 1994)

Paper: Cyclic lambda graph rewriting (at LICS 1994)

Authors: Zena Ariola Jan Willem Klop


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


    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}