Call-by-value and nondeterminism | SpringerLink
Skip to main content
Springer Nature Link
Log in

Call-by-value and nondeterminism

  • Conference paper
  • First Online:
Typed Lambda Calculi and Applications (TLCA 1993)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 664))

Included in the following conference series:

Abstract

We consider the three classical powerdomain semantics (lower, upper and convex) for PCFnv, a nondeterministic call-by-value version of Plotkin's PCF. By a ‘Computational Adequacy Theorem’ we describe how these three semantics are related to different notions of observable behavior of nondeterministic programs. Then we investigate full abstraction: The lower powerdomain semantics turns out to be fully abstract. For the upper powerdomain semantics, full abstraction fails irreparably, i. e. there is no extension of PCFnv by computable operators, for which it is fully abstract. Full abstraction also fails for the convex powerdomain—already at the level of the ground type powerdomain. We repair this low level failure by adding (besides parallel conditional) an exists-operator, which tests all paths of a nondeterministic computation in parallel. But even with this operator we do not obtain full abstraction for all types, and there is some evidence that adding further (reasonable) operators does not help.

Supported by the Deutsche Forschungsgemeinschaft, SFB 124, Teilprojekt C1

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. E. Astesiano and G. Costa. Nondeterminism and fully abstract models. RAIRO, 14(4):323–347, 1980.

    Google Scholar 

  2. C. A. Gunter. Relating total and partial correctness interpretations of non-deterministic programs. In 17th Annual ACM Symposium on Principles of Programming Languages, pages 306–319, 1990.

    Google Scholar 

  3. C. A. Gunter and D. S. Scott. Semantic domains. In J. van Leeuven, editor, Handbook of Theoretical Computer Science, chapter 12, pages 635–674. Elsevier Science Publishers, 1990.

    Google Scholar 

  4. R. Heckmann. Power Domain Constructions. PhD thesis, Universität des Saarlandes, Saarbrücken, 1990.

    Google Scholar 

  5. E. Moggi. Notions of computation and monads. Information and Computation, 93:55–92, 1991.

    Google Scholar 

  6. G. D. Plotkin. Call-by-name, call-by-value and the λ-calculus. Theoretical Computer Science, 1:125–159, 1975.

    Google Scholar 

  7. G. D. Plotkin. LCF considered as a programming language. Theoretical Computer Science, 5:223–256, 1977.

    Google Scholar 

  8. K. Sieber. Relating full abstraction results for different programming languages. In K. Nori and C. V. Madhavan, editors, 10th Conference on Foundations of Software Technology and Theoretical Computer Science, Springer LNCS 472, pages 373–387, Bangalore, India, 1990.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. FB 14 Informatik, Universität des Saarlandes, W-6600, Saarbrücken, Germany

    Kurt Sieber

Authors
  1. Kurt Sieber
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Marc Bezem Jan Friso Groote

Rights and permissions

Reprints and permissions

Copyright information

© 1993 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Sieber, K. (1993). Call-by-value and nondeterminism. In: Bezem, M., Groote, J.F. (eds) Typed Lambda Calculi and Applications. TLCA 1993. Lecture Notes in Computer Science, vol 664. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0037119

Download citation

  • DOI: https://doi.org/10.1007/BFb0037119

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-56517-8

  • Online ISBN: 978-3-540-47586-6

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation