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 journalArticlepeer-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 languageEnglish (US)
    Pages (from-to)711-716
    Number of pages6
    JournalInformation Processing Letters
    Volume111
    Issue number14
    DOIs
    StatePublished - Jul 31 2011

    Bibliographical note

    Copyright:
    Copyright 2011 Elsevier B.V., All rights reserved.

    Keywords

    • Contextual semantics
    • Formal semantics
    • Program correctness
    • Programming calculi

    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