Counterexamples to applicative simulation and extensionality in non-deterministic call-by-need lambda-calculi with letrec

Manfred Schmidt-Schauß; David Sabel; Elena MacHkasova

doi:10.1016/j.ipl.2011.04.011

Counterexamples to applicative simulation and extensionality in non-deterministic call-by-need lambda-calculi with letrec

Manfred Schmidt-Schauß, David Sabel, Elena MacHkasova

Research output: Contribution to journal › Article › peer-review

3 Scopus citations

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.

Original language	English (US)
Pages (from-to)	711-716
Number of pages	6
Journal	Information Processing Letters
Volume	111
Issue number	14
DOIs	https://doi.org/10.1016/j.ipl.2011.04.011
State	Published - Jul 31 2011

Keywords

Contextual semantics
Formal semantics
Program correctness
Programming calculi

Access

10.1016/j.ipl.2011.04.011

Fingerprint Dive into the research topics of 'Counterexamples to applicative simulation and extensionality in non-deterministic call-by-need lambda-calculi with letrec'. Together they form a unique fingerprint.

Cite this

@article{60abeaee8b1644b199bf09c595c63473,

title = "Counterexamples to applicative simulation and extensionality in non-deterministic call-by-need lambda-calculi with letrec",

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.",

keywords = "Contextual semantics, Formal semantics, Program correctness, Programming calculi",

author = "Manfred Schmidt-Schau{\ss} and David Sabel and Elena MacHkasova",

year = "2011",

month = jul,

day = "31",

doi = "10.1016/j.ipl.2011.04.011",

language = "English (US)",

volume = "111",

pages = "711--716",

journal = "Information Processing Letters",

issn = "0020-0190",

publisher = "Elsevier",

number = "14",

}

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 -