Simulation in the call-by-need lambda-calculus with letrec

Manfred Schmidt-Schauss, David Sabel, Elena Machkasova

Research output: Chapter in Book/Report/Conference proceedingConference contribution

10 Scopus citations

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.

Original languageEnglish (US)
Title of host publicationProceedings of the 21st International Conference on Rewriting Techniques and Applications, RTA 2010
Pages295-310
Number of pages16
StatePublished - Dec 1 2010
Event21st International Conference on Rewriting Techniques and Applications, RTA 2010 - Edinburgh, United Kingdom
Duration: Jul 11 2010Jul 13 2010

Publication series

NameLeibniz International Proceedings in Informatics, LIPIcs
Volume6
ISSN (Print)1868-8969

Conference

Conference21st International Conference on Rewriting Techniques and Applications, RTA 2010
Country/TerritoryUnited Kingdom
CityEdinburgh
Period7/11/107/13/10

Keywords

  • Bisimulation
  • Call-by-need
  • Contextual equivalence
  • Lambda calculus
  • Letrec
  • Semantics

Cite this