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