We establish an isomorphism between the well-formed cyclic lambda-graphs and their syntactic representations. To define the well-formed cyclic lambda-graphs we introduce the notion of a scoped lambda-graph. The well-formed lambda-graphs are those that have associated scoped lambda-graphs. The scoped lambda-graphs are represented by terms defined over lambda calculus extended with the letrec construct. On this set of terms we define a sound and complete axiom system (the representational calculus) that equates different representations of the same scoped lambda-graph. Since a well-formed lambda-graph can have different scoped lambda-graphs associated to it, we extend the representational calculus with axioms that equate different representations of the same well-formed graph. Finally, we consider the unwinding of well-formed graphs to possibly infinite trees and give a sound and complete axiomatization of tree unwinding.
We add computational power to our graphs and terms by defining beta-reduction on scoped lambda-graphs and its associated notion on terms. The representational axiom system developed in the first part combined with beta-reduction constitutes our cyclic extension of lambda calculus. In contrast to current theories, which impose restrictions on where the rewriting can take place, our reduction theory is very liberal, e.g. it allows rewriting under lambda-abstractions and on cycles. As shown previously, the reduction theory is non-confluent. We thus introduce an approximate notion of confluence, which guarantees uniqueness of infinite normal forms. We show that the infinite normal form defines a congruence on the set of terms. We relate our cyclic lambda calculus to the plain lambda calculus and to the infinitary lambda calculi. We conclude by presenting a variant of our cyclic lambda calculus, which follows the tradition of the explicit substitution calculi.
Since most implementations of non-strict functional languages rely on sharing to avoid repeating computations, we develop a variant of our cyclic lambda calculus that enforces the sharing of computations and show that the two calculi are observationally equivalent. For reasoning about strict languages we develop a call-by-value variant of the sharing calculus. We state the difference between strict and non-strict computations in terms of different garbage collection rules. We relate the call-by-value calculus to Moggi's computational lambda calculus and to Hasegawa's calculus.