Cyclic lambda graph rewriting
Zena M. Ariola, Jan Willem Klop · 2002
Studies cyclic /spl lambda/-graphs. The starting point is to treat a /spl lambda/-graph as a system of recursion equations involving /spl lambda/-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 /spl lambda/-graph calculi, which are inspired by the family of /spl lambdaspl sigma/-calculi (/spl lambda/-calculi with explicit substitution). However, these concern acyclic expressions only. In this paper we are not concerned with optimality questions for acyclic /spl lambda/-reduction. We also indicate how Wadsworth's (1978) interpreter can be simulated in the /spl lambda/-graph rewrite rules that we propose.>