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

Authors Manfred Schmidt-Schauss, David Sabel, Elena Machkasova

Thumbnail PDF


  • Filesize: 181 kB
  • 16 pages

Document Identifiers

Author Details

Manfred Schmidt-Schauss
David Sabel
Elena Machkasova

Cite AsGet BibTex

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)


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.
  • Lambda calculus
  • semantics
  • contextual equivalence
  • bisimulation,call-by-need


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads