License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.RTA.2013.206
URN: urn:nbn:de:0030-drops-40635
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2013/4063/
Go to the corresponding LIPIcs Volume Portal

Grabmayer, Clemens ; Rochel, Jan

Expressibility in the Lambda Calculus with Mu

pdf-format:
16.pdf (1 MB)

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.

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 =	{206--222},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-53-8},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{21},
  editor =	{Femke van Raamsdonk},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2013/4063},
  URN =		{urn:nbn:de:0030-drops-40635},
  doi =		{10.4230/LIPIcs.RTA.2013.206},
  annote =	{Keywords: lambda-calculus, lambda-calculus with letrec, unfolding semantics, regularity for infinite lambda-terms, binding-capturing chain}
}

Keywords: lambda-calculus, lambda-calculus with letrec, unfolding semantics, regularity for infinite lambda-terms, binding-capturing chain
Collection: 24th International Conference on Rewriting Techniques and Applications (RTA 2013)
Issue Date: 2013
Date of publication: 24.06.2013

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI