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

How to prove similarity a precongruence in nondeterministic callbyneed lambda calculi
(2006)

Matthias Mann
Manfred SchmidtSchauß
 Extending the method of Howe, we establish a large class of untyped higherorder calculi, in particular such with callbyneed evaluation, where similarity, also called applicative simulation, can be used as a proof tool for showing contextual preorder. The paper also demonstrates that Mann’s approach using an intermediate “approximation” calculus scales up well from a basic callbyneed nondeterministic lambdacalculus to more expressive lambda calculi. I.e., it is demonstrated, that after transferring the contextual preorder of a nondeterministic callbyneed lambda calculus to its corresponding approximation calculus, it is possible to apply Howe’s method to show that similarity is a precongruence. The transfer is not treated in this paper. The paper also proposes an optimization of the similaritytest by cutting off redundant computations. Our results also applies to deterministic or nondeterministic callbyvalue lambdacalculi, and improves upon previous work insofar as it is proved that only closed values are required as arguments for similaritytesting instead of all closed expressions.