DROPS

Document

DOI: 10.4230/LIPIcs.RTA.2013.239

Extending Abramsky's Lazy Lambda Calculus: (Non)-Conservativity of Embeddings

Authors: Manfred Schmidt-Schauß, Elena Machkasova, and David Sabel

Published in: LIPIcs, Volume 21, 24th International Conference on Rewriting Techniques and Applications (RTA 2013)

Abstract

Our motivation is the question whether the lazy lambda calculus, a pure lambda calculus with the leftmost outermost rewriting strategy, considered under observational semantics, or extensions thereof, are an adequate model for semantic equivalences in real-world purely functional programming languages, in particular for a pure core language of Haskell. We explore several extensions of the lazy lambda calculus: addition of a seq-operator, addition of data constructors and case-expressions, and their combination, focusing on conservativity of these extensions. In addition to untyped calculi, we study their monomorphically and polymorphically typed versions. For most of the extensions we obtain non-conservativity which we prove by providing counterexamples. However, we prove conservativity of the extension by data constructors and case in the monomorphically typed scenario.

Cite as

Manfred Schmidt-Schauß, Elena Machkasova, and David Sabel. Extending Abramsky's Lazy Lambda Calculus: (Non)-Conservativity of Embeddings. In 24th International Conference on Rewriting Techniques and Applications (RTA 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 21, pp. 239-254, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@InProceedings{schmidtschau_et_al:LIPIcs.RTA.2013.239,
  author =	{Schmidt-Schau{\ss}, Manfred and Machkasova, Elena and Sabel, David},
  title =	{{Extending Abramsky's Lazy Lambda Calculus: (Non)-Conservativity of Embeddings}},
  booktitle =	{24th International Conference on Rewriting Techniques and Applications (RTA 2013)},
  pages =	{239--254},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-53-8},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{21},
  editor =	{van Raamsdonk, Femke},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2013.239},
  URN =		{urn:nbn:de:0030-drops-40651},
  doi =		{10.4230/LIPIcs.RTA.2013.239},
  annote =	{Keywords: lazy lambda calculus, contextual semantics, conservativity}
}

Document

DOI: 10.4230/LIPIcs.RTA.2010.295

Simulation in the Call-by-Need Lambda-Calculus with letrec

Authors: Manfred Schmidt-Schauss, David Sabel, and Elena Machkasova

Published in: LIPIcs, Volume 6, Proceedings of the 21st International Conference on Rewriting Techniques and Applications (2010)

Abstract

This paper shows the equivalence of applicative similarity and contextual approximation, and hence also of bisimilarity and contextual equivalence, in the deterministic call-by-need lambda calculus with letrec. Bisimilarity simplifies equivalence proofs in the calculus and opens a way for more convenient correctness proofs for program transformations. Although this property may be a natural one to expect, to the best of our knowledge, this paper is the first one providing a proof. The proof technique is to transfer the contextual approximation into Abramsky's lazy lambda calculus by a fully abstract and surjective translation. This also shows that the natural embedding of Abramsky's lazy lambda calculus into the call-by-need lambda calculus with letrec is an isomorphism between the respective term-models. We show that the equivalence property proven in this paper transfers to a call-by-need letrec calculus developed by Ariola and Felleisen.

Cite as

Manfred Schmidt-Schauss, David Sabel, and Elena Machkasova. Simulation in the Call-by-Need Lambda-Calculus with letrec. In Proceedings of the 21st International Conference on Rewriting Techniques and Applications. Leibniz International Proceedings in Informatics (LIPIcs), Volume 6, pp. 295-310, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{schmidtschauss_et_al:LIPIcs.RTA.2010.295,
  author =	{Schmidt-Schauss, Manfred and Sabel, David and Machkasova, Elena},
  title =	{{Simulation in the Call-by-Need Lambda-Calculus with letrec}},
  booktitle =	{Proceedings of the 21st International Conference on Rewriting Techniques and Applications},
  pages =	{295--310},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-18-7},
  ISSN =	{1868-8969},
  year =	{2010},
  volume =	{6},
  editor =	{Lynch, Christopher},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2010.295},
  URN =		{urn:nbn:de:0030-drops-26593},
  doi =		{10.4230/LIPIcs.RTA.2010.295},
  annote =	{Keywords: Lambda calculus, semantics, contextual equivalence, bisimulation,call-by-need}
}

Search Results

Documents authored by Machkasova, Elena

Extending Abramsky's Lazy Lambda Calculus: (Non)-Conservativity of Embeddings

Abstract

Cite as

Simulation in the Call-by-Need Lambda-Calculus with letrec

Abstract

Cite as

Thanks for your feedback!

Could not send message