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]
Specification and Analysis of Embedded Systems

Ariola, Z.M, & Klop, J.W. (1996). Lambda calculus with explicit recursion. Department of Computer Science [CS]. CWI.