2026-07-20T10:52:09Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:2659 2024-03-06T10:33:30Z ddc:004 open_access

Simulation in the Call-by-Need Lambda-Calculus with letrec Schmidt-Schauss, Manfred Sabel, David Machkasova, Elena Lambda calculus semantics contextual equivalence bisimulation,call-by-need 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Manfred Schmidt-Schauss and David Sabel and Elena Machkasova 2010 Is Part Of LIPIcs, Volume 6, Proceedings of the 21st International Conference on Rewriting Techniques and Applications (2010) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.RTA.2010.295 urn:nbn:de:0030-drops-26593 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2010.295 eng https://creativecommons.org/licenses/by-nc-nd/3.0/legalcode