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 letrsc, a feature that is essential to reason about time and space behavior of functional languages and also about compilation and optimizations of programs. (C) 1997 Academic Press.