Skip to main content
SpringerLink
Log in

Definability of Total Objects in PCF and Related Calculi

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

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

Included in the following conference series:

  • 471 Accesses

Abstract

We let PCF be Plotkin’s [8] calculus based on Scott’s 10, 11 LCF, and we consider the standard case with base types for the natural numbers and for the Booleans. We consider the standard interpretation using algebraic domains. Plotkin [8] showed that a finite object in general will not be definable, and isolated two nondeterministic constants PAR and ∃ ω such that each computable object is definable in PCF + PAR + ∃ ω .

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

  1. Escardó, M. H., PCF extended with real numbers: a domain-theoretic approach to higher-order exact number computation, Thesis, University of London, Imperial College of Science, Technology and medicine (1996).

    Google Scholar 

  2. Escardó, M. H., PCF extended with real numbers, Theoretical Computer Science 162(1) pp. 79–115 (1996).

    Article  MATH  MathSciNet  Google Scholar 

  3. Niggl, K.-H., M ω considered as a programming language, Annals of Pure and Applied Logic 99, pp. 73–92 (1999)

    Article  MATH  MathSciNet  Google Scholar 

  4. Normann, D., Computability over the partial continuous functionals, Journal of Symbolic Logic 65, pp. 1133–1142, (2000)

    Article  MATH  MathSciNet  Google Scholar 

  5. Normann, D., The Cook-Berger Problem. A Guide to the solution, In Spreen, D. (ed.): Electronic Notes in Theoretical Computer Science. 2000-10; 35: 9

    Google Scholar 

  6. Normann, D., The continuous functionals of finite types over the reals, To appear in Keimel, Zhang, Liu and Chen (eds.) Domains and Processes Proceedings of the 1st International Symposium on Domain Theory, Luwer Academic Publishers

    Google Scholar 

  7. Normann, D., Exact real number computations relative to hereditarily total functionals, To appear in Theoretical Computer Science.

    Google Scholar 

  8. Plotkin, G., LCF considered as a programming language, Theoretical Computer Science 5 (1977) pp. 223–255.

    Article  MathSciNet  Google Scholar 

  9. Rördam, C., A comparison of the simply typed lambda calculi M ω and λPA, Cand. Scient. Thesis, Oslo (2000)

    Google Scholar 

  10. Scott, D. S., A theory of computable functionals of higher type, Unpublished notes, University of Oxford, Oxford (1969).

    Google Scholar 

  11. Scott, D. S., A type-theoretical alternative to ISWIM, CUCH, OWHY, Theoretical Computer Science 121 pp. 411–440 (1993).

    Article  MATH  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Mathematics, University of Oslo, USA

    Dag Normann

Authors
  1. Dag Normann
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Oxford University Computing Laboratory, Wolfson Building, Parks Road, Oxford, OX1 3QD, USA

    Samson Abramsky

Rights and permissions

Reprints and permissions

Copyright information

© 2001 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Normann, D. (2001). Definability of Total Objects in PCF and Related Calculi. In: Abramsky, S. (eds) Typed Lambda Calculi and Applications. TLCA 2001. Lecture Notes in Computer Science, vol 2044. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45413-6_3

Download citation

  • DOI: https://doi.org/10.1007/3-540-45413-6_3

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-41960-0

  • Online ISBN: 978-3-540-45413-7

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation