# Lambda calculus plus letrec

The paper consists of three parts.
#### Part I:

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.

#### Part II:

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.

#### Part III:

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.

#### Available in:
ps,
pdf,