TY  - UNPD
A1  - Schmidt-Schauß, Manfred
A1  - Sabel, David
A1  - Machkasova, Elena
T1  - Simulation in the call-by-need lambda-calculus with letrec
T2  - Technical report Frank / Johann-Wolfgang-Goethe-Universität, Fachbereich Informatik und Mathematik, Institut für Informatik ; 40
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.
T3  - Technical report Frank / Johann-Wolfgang-Goethe-Universität, Fachbereich Informatik und Mathematik, Institut für Informatik - 40 
KW  - Formale Semantik
KW  - Lambda-Kalkül
KW  - Kontextuelle Gleichheit
KW  - semantics
KW  - lambda calculus
KW  - contextual equivalence
KW  - letrec
Y1  - 2010
UR  - http://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/7828
UR  - https://nbn-resolving.org/urn:nbn:de:hebis:30-77888
UR  - http://www.ki.informatik.uni-frankfurt.de/papers/frank/frank-40.pdf
PB  - Johann Wolfgang Goethe-Univ., Fachbereich Informatik und Mathematik, Inst. für Informatik, Research group for Artificial Intelligence and Software Technology
CY  - Frankfurt [am Main]
ER  -