  We investigate the relationship between finite terms in lambda-letrec, the
lambda calculus with letrec, and the infinite lambda terms they express. As
there are easy examples of lambda-terms that, intuitively, are not unfoldings
of terms in lambda-letrec, we consider the question: How can those infinite
lambda terms be characterised that are lamda-letrec-expressible in the sense
that they can be obtained as infinite unfoldings of terms in lambda-letrec?
  For 'observing' infinite lambda-terms through repeated 'experiments' carried
out at the head of the term we introduce two rewrite systems (with rewrite
relations) -reg-> and -reg+-> that decompose the term, and produce 'generated
subterms' in two notions. Thereby the sort of the step can be observed as well
as its target, a generated subterm. In both systems there are four sorts of
decomposition steps: -lambda-> steps (decomposing a lambda-abstraction), -@0>
and -@1> steps (decomposing an application into its function and argument), and
respectively, -del-> steps (delimiting the scope of an abstraction, for
-reg->), and -S-> (delimiting of scopes, for -reg+->). These steps take place
on infinite lambda-terms furnished with a leading prefix of abstractions for
gathering previously encountered lambda-abstractions and keeping the generated
subterms closed. We call an infinite lambda-term 'regular'/'strongly regular'
if its set of -reg-> -reachable / -reg-> -reachable generated subterms is
finite. Furthermore, we analyse the binding structure of lambda-terms with the
concept of 'binding-capturing chain'.
  Using these concepts, we answer the question above by providing two
characterisations of lambda-letrec-expressibility. For all infinite
lambda-terms M, the following statements are equivalent: (i) M is
lambda-letrec-expressible; (ii) M is strongly regular; (iii) M is regular, and
it only has finite binding-capturing chains.
