Abstract
We address a problem connected to the unfolding semantics of functional programming languages: give a useful characterization of those infinite lambdaterms that are lambdaletrecexpressible in the sense that they arise as infinite unfoldings of terms in lambdaletrec, the lambdacalculus with letrec. We provide two characterizations, using concepts we introduce for infinite lambdaterms: regularity, strong regularity, and bindingâ€“capturing chains.
It turns out that lambdaletrecexpressible infinite lambdaterms
form a proper subclass of the regular infinite lambdaterms.
In this paper we establish these characterizations only for
expressibility in lambdamu, the lambdacalculus with explicit murecursion. We show that for all infinite lambdaterms T the following are equivalent: (i): T is lambdamuexpressible; (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 lambdaterms as two different generalizations of regularity for infinite firstorder terms: as the existence of only finitely many subterms that are defined as the reducts of two rewrite systems for decomposing lambdaterms. These rewrite systems act on infinite lambdaterms furnished with a bracketed prefix of abstractions for collecting decomposed lambdaabstractions and keeping the terms closed under decomposition. They differ in which vacuous abstractions in the prefix are removed.
BibTeX  Entry
@InProceedings{grabmayer_et_al:LIPIcs:2013:4063,
author = {Clemens Grabmayer and Jan Rochel},
title = {{Expressibility in the Lambda Calculus with Mu}},
booktitle = {24th International Conference on Rewriting Techniques and Applications (RTA 2013)},
pages = {206222},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783939897538},
ISSN = {18688969},
year = {2013},
volume = {21},
editor = {Femke van Raamsdonk},
publisher = {Schloss DagstuhlLeibnizZentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2013/4063},
URN = {urn:nbn:de:0030drops40635},
doi = {10.4230/LIPIcs.RTA.2013.206},
annote = {Keywords: lambdacalculus, lambdacalculus with letrec, unfolding semantics, regularity for infinite lambdaterms, bindingcapturing chain}
}
Keywords: 

lambdacalculus, lambdacalculus with letrec, unfolding semantics, regularity for infinite lambdaterms, bindingcapturing chain 
Collection: 

24th International Conference on Rewriting Techniques and Applications (RTA 2013) 
Issue Date: 

2013 
Date of publication: 

24.06.2013 