Skip to main content
SpringerLink
Log in

Full abstraction and the Context Lemma (preliminary report)

  • Invited Paper
  • Conference paper
  • First Online:
Theoretical Aspects of Computer Software (TACS 1991)

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

Included in the following conference series:

Abstract

A general notion of rewriting system of the kind used for evaluating simply typed λ-terms in Scott's PCF is defined. Any simply typed λ-calculus with PCF-like rewriting semantics is shown necessarily to satisfy Milner's Context Lemma. A simple argument demonstrates that any denotational semantics which is adequate for PCF and in which certain simple Boolean functionals exist, cannot be fully abstract for any extension of PCF satisyfing the Context Lemma. An immediate corollary is that Berry's stable domains cannot be fully abstract for any extension of PCF definable by PCF-like rules. Thus, the idea of adding a combinator to PCF analogous to the “parallel-or” combinator which establishes full abstraction for the familiar cpo model cannot be generalized for models such as stable domains.

Supported in part by ARO grant DAAL03-89-G-0071.

Supported in part by ONR grant N00014-89-J-1988 and NSF grant 8819761-CCR.

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.

Similar content being viewed by others

References

  1. S. Abramsky. The lazy lambda calculus. In D. L. Turner, editor, Research Topics in Functional Programming. Addison-Wesley Publishing Co., 1989.

    Google Scholar 

  2. S. Abramsky. Domain theory in logical form. Ann. Pure Appl. Logic, 51:1–77, 1991.

    Google Scholar 

  3. G. Berry. Séquentialité de l'evaluation formelle des lambda-expressions. In B. Robinet, editor, Program Transformations, 3eme Colloque International sur la programmation, pages 67–80, 1978.

    Google Scholar 

  4. G. Berry. Stable models of typed lambda-calculi. In G. Ausiello and C. Böhm, editors, Automata, Languages and Programming: Fifth Colloquium, volume 62 of Lecture Notes in Computer Science, pages 72–89. Springer-Verlag, July 1978.

    Google Scholar 

  5. G. Berry and P.-L. Curien. Sequential algorithms on concrete data structures. Theor. Comput. Sci., 20(3):265–321, July 1982.

    Google Scholar 

  6. G. Berry and P.-L. Curien. Theory and practice of sequential algorithms: the kernel of the programming language CDS. In M. Nivat and J. C. Reynolds, editors, Algebraic Methods in Semantics, chapter 2, pages 35–87. Cambridge Univ. Press, 1985.

    Google Scholar 

  7. G. Berry, P.-L. Curien, and J.-J. Lévy. Full abstraction for sequential languages: the state of the art. In M. Nivat and J. C. Reynolds, editors, Algebraic Methods in Semantics, chapter 3, pages 89–132. Cambridge Univ. Press, 1985.

    Google Scholar 

  8. B. Bloom. Can LCF be topped? Flat lattice models of typed lambda calculus (preliminary report). In Third Annual Symposium on Logic in Computer Science, pages 282–295. IEEE, 1988.

    Google Scholar 

  9. B. Bloom. Can LCF be topped? Flat lattice models of typed λ-calculus. Information and Computation, 87(1/2):263–300, July/Aug. 1990.

    Google Scholar 

  10. B. Bloom, S. Istrail, and A. R. Meyer. Bisimulation can't be traced (preliminary report). In Conference Record of the Fifteenth Annual ACM Symposium on Principles of Programming Languages, pages 229–239, 1988. Also appears as MIT Technical Memo MIT/LCS/TM-345; submitted for journal publication.

    Google Scholar 

  11. A. Bucciarelli and T. Ehrard. Sequentiality and strong stability. In Proceedings, Sixth Annual IEEE Symposium on Logic in Computer Science, 1991. to appear.

    Google Scholar 

  12. P.-L. Curien. Categorical Combinators, Sequential Algorithms and Functional Programming. John Wiley and Sons, 1986.

    Google Scholar 

  13. J.-Y. Girard. The system F of variable types, fifteen years later. Theor. Comput. Sci., 45:152–192, 1986.

    Google Scholar 

  14. D. J. Howe. Equality in lazy computation systems. In Proceedings, Fourth Annual Symposium on Logic in Computer Science, pages 198–203. IEEE, 1989.

    Google Scholar 

  15. G. Huet and J.-J. Lévy. Computations in nonambiguous term rewriting systems. Technical Report 359, INRIA, Rocquencourt, France, 1979.

    Google Scholar 

  16. T. Jim and A. R. Meyer. Communication in the types electronic forum (types@theory.lcs.mit.edu). June 17th, 1989.

    Google Scholar 

  17. G. Kahn and D. B. MacQueen. Coroutines and networks of parallel processes. In B. Gilchrist, editor, Information Processing '77, pages 993–998. North-Holland Publishing Co., 1977.

    Google Scholar 

  18. I. Mason and C. Talcott. Programming, transforming, and proving with function abstractions and memories. In G. Ausiello, M. Dezani-Ciancaglini, and S. R. D. Rocca, editors, Automata, Languages and Programming: 16th International Colloquium, volume 372 of Lecture Notes in Computer Science. Springer-Verlag, 1989.

    Google Scholar 

  19. A. R. Meyer. What is a model of the lambda calculus? Information and Control, 52(1):87–122, Jan. 1982.

    Article  Google Scholar 

  20. A. R. Meyer. Semantical paradigms: Notes for an invited lecture, with two appendices by Stavros Cosmadakis. In Third Annual Symposium on Logic in Computer Science, pages 236–253. IEEE, 1988.

    Google Scholar 

  21. R. Milner. Fully abstract models of the typed lambda calculus. Theor. Comput. Sci., 4:1–22, 1977.

    Google Scholar 

  22. K. Mulmuley. Full Abstraction and Semantic Equivalence. ACM Doctoral Dissertation Award 1986. MIT Press, 1987.

    Google Scholar 

  23. C.-H. L. Ong. The Lazy Lambda Calculus: An Investigation into the Foundations of Functional Programming. PhD thesis, Imperial College, University of London, 1988.

    Google Scholar 

  24. G. D. Plotkin. LCF considered as a programming language. Theor. Comput. Sci., 5(3):223–256, Dec. 1977.

    Article  Google Scholar 

  25. V. Sazonov. Expressibility of functions in D. Scott's LCF language. Algebra i Logika, 15:308–330, 1976. (Russian).

    Google Scholar 

  26. D. S. Scott. A type theoretical alternative to CUCH, ISWIM, OWHY. Manuscript, Oxford Univ., 1969.

    Google Scholar 

  27. D. S. Scott. Continuous lattices. In F. W. Lawvere, editor, Toposes, Algebraic Geometry and Logic, volume 274 of Lecture Notes in Mathematics, pages 97–136. Springer-Verlag, 1972.

    Google Scholar 

  28. D. S. Scott. Data types as lattices. SIAM J. Comput., 5:522–587, 1976.

    Google Scholar 

  29. D. S. Scott. Logic and programming languages. Commun. ACM, 20:634–645, 1977.

    Google Scholar 

  30. S. Smith. From operational to denotational semantics. In Mathematical Foundations of Programming Semantics, 1991. To appear.

    Google Scholar 

  31. A. Stoughton. Fully Abstract Models of Programming Languages. Research Notes in Theoretical Computer Science. Pitman/Wiley, 1988. Revision of Ph.D. thesis, Dept. of Computer Science, Univ. Edinburgh, Report No. CST-40-86, 1986.

    Google Scholar 

  32. C. Strachey. Fundamental concepts in programming languages. Lecture Notes, Int'l. Summer School in Computer Programming, Copenhagen., 1967.

    Google Scholar 

  33. C. Talcott. Programming and proving with function and control abstractions. Technical Report STAN-CS-89-1288, Stanford Univ., 1988.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. MIT Laboratory for Computer Science, USA

    Trevor Jim & Albert R. Meyer

Authors
  1. Trevor Jim
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Albert R. Meyer
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Takayasu Ito Albert R. Meyer

Rights and permissions

Reprints and permissions

Copyright information

© 1991 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Jim, T., Meyer, A.R. (1991). Full abstraction and the Context Lemma (preliminary report). In: Ito, T., Meyer, A.R. (eds) Theoretical Aspects of Computer Software. TACS 1991. Lecture Notes in Computer Science, vol 526. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-54415-1_44

Download citation

  • DOI: https://doi.org/10.1007/3-540-54415-1_44

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-54415-9

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

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation