Technical report Frank / JohannWolfgangGoetheUniversität, Fachbereich Informatik und Mathematik, Institut für Informatik
2 search hits
 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.
 32 [v.2]

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

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.