This paper is concerned with lhe study of λ-calculus with explicit recursion, namely of 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 'substitution' operation. This leads to a family of λ-graph calculi, which can be seen as an extension of the family of λσ-calculi (λ-calculi with explicit substitution). While the λσ-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.