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.
 32

A finite simulation method in a nondeterministic callbyneed calculus with letrec, constructors and case
(2008)

Manfred SchmidtSchauß
Elena Machkasova
 The paper proposes a variation of simulation for checking and proving contextual equivalence in a nondeterministic callbyneed lambdacalculus with constructors, case, seq, and a letrec with cyclic dependencies. It also proposes a novel method to prove its correctness. The calculus' semantics is based on a smallstep rewrite semantics and on mayconvergence. The cyclic nature of letrec bindings, as well as nondeterminism, makes known approaches to prove that simulation implies contextual equivalence, such as Howe's proof technique, inapplicable in this setting. The basic technique for the simulation as well as the correctness proof is called preevaluation, which computes a set of answers for every closed expression. If simulation succeeds in finite computation depth, then it is guaranteed to show contextual preorder of expressions.