Lambda calculus with explicit recursion
This paper is concerned with the study of $lambda$-calculus with explicit recursion, namely of cyclic $lambda$-graphs. The starting point is to treat a $lambda$-graph as a system of recursion equations involving $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 `substitution' operation. This leads to a family of $lambda$-graph calculi, which can be seen as an extension of the family of $lambda sigma$-calculi ($lambda$-calculi with explicit substitution). While the $lambda sigma$-calculi treat the let-construct as a first-class citizen, our calculi support the letrec, a feature that is essential to reason about time and space behavior of functional languages and also about compilation and optimizations of programs.
|Applicative Programming (acm D.1.1), Formal Definitions and Theory (acm D.3.1), Models of Computation (acm F.1.1), Mathematical Logic (acm F.4.1), Grammars and Other Rewriting Systems (acm F.4.2)|
|Department of Computer Science [CS]|
|Organisation||Specification and Analysis of Embedded Systems|
Ariola, Z.M, & Klop, J.W. (1996). Lambda calculus with explicit recursion. Department of Computer Science [CS]. CWI.