| Article ID | Journal | Published Year | Pages | File Type |
|---|---|---|---|---|
| 427923 | Information Processing Letters | 2011 | 6 Pages |
Abstract
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.
► Non-deterministic call-by-need lambda-calculi with letrec are not extensional. ► Applicative bisimulation is unsound in such calculi. ► The counterexample can be adapted to other extended pure lambda-calculi.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
Authors
Manfred Schmidt-Schauß, David Sabel, Elena Machkasova,