Technical report Frank / JohannWolfgangGoetheUniversität, Fachbereich Informatik und Mathematik, Institut für Informatik
2 search hits
 40

Simulation in the callbyneed lambdacalculus with letrec
(2010)

Manfred SchmidtSchauß
David Sabel
Elena Machkasova
 This paper shows the equivalence of applicative similarity and contextual approximation, and hence also of bisimilarity and contextual equivalence, in the deterministic callbyneed 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 callbyneed lambda calculus with letrec is an isomorphism between the respective termmodels.We show that the equivalence property proven in this paper transfers to a callbyneed letrec calculus developed by Ariola and Felleisen.
 38

Counterexamples to simulation in nondeterministic callbyneed lambdacalculi with letrec
(2009)

Manfred SchmidtSchauß
Elena Machkasova
David Sabel
 This note shows that in nondeterministic extended lambda calculi with letrec, the tool of applicative (bi)simulation is in general not usable for contextual equivalence, by giving a counterexample adapted from data flow analysis. It also shown that there is a flaw in a lemma and a theorem concerning finite simulation in a conference paper by the first two authors.