  We investigate the relationship between finite terms in {\lambda}-letrec, the
{\lambda}-calculus with letrec, and the infinite {\lambda}-terms they express.
We say that a lambda-letrec term expresses a lambda-term if the latter can be
obtained as an infinite unfolding of the former. Unfolding is the process of
substituting occurrences of function variables by the right-hand side of their
definition.
  We consider the following questions: (i) How can we characterise those
infinite {\lambda}-terms that are {\lambda}-letrec-expressible? (ii) Given two
{\lambda}-letrec terms, how can we determine whether they have the same
unfolding? (iii) Given a {\lambda}-letrec term, can we find a more compact
version of the term with the same unfolding? To tackle these questions we
introduce and study the following formalisms: (i) a rewriting system for
unfolding {\lambda}-letrec terms into {\lambda}-terms (ii) a rewriting system
for `observing' {\lambda}-terms by dissecting their term structure (iii)
higher-order and first-order graph formalisms together with translations
between them as well as translations from and to {\lambda}-letrec.
  We identify a first-order term graph formalism on which bisimulation
preserves and reflects the unfolding semantics of {\lambda}-letrec and which is
closed under functional bisimulation. From this we derive efficient methods to
determine whether two terms are equivalent under infinite unfolding and to
compute the maximally shared form of a given {\lambda}-letrec term.
