Sciweavers

Share
RTA
2010
Springer

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

9 years 2 months ago
Simulation in the Call-by-Need Lambda-Calculus with letrec
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 Abramlazy 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.
Manfred Schmidt-Schauß, David Sabel, Elena M
Added 16 Aug 2010
Updated 16 Aug 2010
Type Conference
Year 2010
Where RTA
Authors Manfred Schmidt-Schauß, David Sabel, Elena Machkasova
Comments (0)
books