TY - JOUR
T1 - Counterexamples to applicative simulation and extensionality in non-deterministic call-by-need lambda-calculi with letrec
AU - Schmidt-Schauß, Manfred
AU - Sabel, David
AU - MacHkasova, Elena
PY - 2011/7/31
Y1 - 2011/7/31
N2 - 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.
AB - 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.
KW - Contextual semantics
KW - Formal semantics
KW - Program correctness
KW - Programming calculi
UR - http://www.scopus.com/inward/record.url?scp=79955717521&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=79955717521&partnerID=8YFLogxK
U2 - 10.1016/j.ipl.2011.04.011
DO - 10.1016/j.ipl.2011.04.011
M3 - Article
AN - SCOPUS:79955717521
VL - 111
SP - 711
EP - 716
JO - Information Processing Letters
JF - Information Processing Letters
SN - 0020-0190
IS - 14
ER -