Counterexamples to applicative simulation and extensionality in non-deterministic call-by-need lambda-calculi with letrec
This note provides an example that demonstrates that in non-deterministic call-by-need lambda-calculi extended with cyclic let, extensionality as well as applicative bisimulation in general may not be used as criteria for contextual equivalence w.r.t. may- and two different forms of must-convergence. We also outline how the counterexample can be adapted to other calculi. (C) 2011 Elsevier B.V. All rights reserved.
contextual semantics formal semantics programming calculi program correctness