TY  - CONF
A1  - Schmidt-Schauß, Manfred
A1  - Sabel, David
A1  - Machkasova, Elena
T1  - Simulation in the call-by-need lambda-calculus with letrec
T2  - Proceedings of the 21st International Conference on Rewriting Techniques and Applications (RTA'10)
N2  - 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. 1998 ACM Subject Classification: F.4.2, F.3.2, F.3.3, F.4.1. Key words and phrases: semantics, contextual equivalence, bisimulation, lambda calculus, call-by-need, letrec.
KW  - semantics
KW  - contextual equivalence
KW  - bisimulation
KW  - lambda calculus
KW  - call-by-need
KW  - letrec
Y1  - 2010
UR  - http://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/20403
UR  - https://nbn-resolving.org/urn:nbn:de:hebis:30-68385
SN  - 978-3-939897-18-7
SN  - 1868-8969
N1  - (c) M. Schmidt-Schauß, D. Sabel, and E. Machkasova ; CC Creative Commons Non-Commercial No Derivatives License
SP  - 295
EP  - 310
PB  - Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH
CY  - Wadern
ER  -