Expressibility in the Lambda Calculus with Mu

Abstract

We address a problem connected to the unfolding semantics of functional programming languages: give a useful characterization of those infinite lambda-terms that are lambda-letrec-expressible in the sense that they arise as infinite unfoldings of terms in lambda-letrec, the lambda-calculus with letrec. We provide two characterizations, using concepts we introduce for infinite lambda-terms: regularity, strong regularity, and binding–capturing chains. 
It turns out that lambda-letrec-expressible infinite lambda-terms 
form a proper subclass of the regular infinite lambda-terms. 
In this paper we establish these characterizations only for 
expressibility in lambda-mu, the lambda-calculus with explicit mu-recursion. We show that for all infinite lambda-terms T the following are equivalent: (i): T is lambda-mu-expressible; (ii): T is strongly regular; (iii): T is regular, and it only has finite binding–capturing chains.

We define regularity and strong regularity for infinite lambda-terms  as two different generalizations of regularity for infinite first-order terms: as the existence of only finitely many subterms that are defined as the reducts of two rewrite systems for decomposing lambda-terms. These rewrite systems act on infinite lambda-terms furnished with a bracketed prefix of abstractions for collecting decomposed lambda-abstractions and keeping the terms closed under decomposition. They differ in which vacuous abstractions in the prefix are removed.