2026-07-24T10:07:20Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:4063 2024-03-06T10:34:46Z ddc:004 open_access

Expressibility in the Lambda Calculus with Mu Grabmayer, Clemens Rochel, Jan lambda-calculus lambda-calculus with letrec unfolding semantics regularity for infinite lambda-terms binding-capturing chain 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Clemens Grabmayer and Jan Rochel 2013 Is Part Of LIPIcs, Volume 21, 24th International Conference on Rewriting Techniques and Applications (RTA 2013) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.RTA.2013.206 urn:nbn:de:0030-drops-40635 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2013.206 eng https://creativecommons.org/licenses/by/3.0/legalcode