Expressibility in the Lambda Calculus with Mu

Authors Clemens Grabmayer, Jan Rochel

Thumbnail PDF


  • Filesize: 1.06 MB
  • 17 pages

Document Identifiers

Author Details

Clemens Grabmayer
Jan Rochel

Cite AsGet BibTex

Clemens Grabmayer and Jan Rochel. Expressibility in the Lambda Calculus with Mu. In 24th International Conference on Rewriting Techniques and Applications (RTA 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 21, pp. 206-222, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)


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.
  • lambda-calculus
  • lambda-calculus with letrec
  • unfolding semantics
  • regularity for infinite lambda-terms
  • binding-capturing chain


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail