Skip to main content
SpringerLink
Log in

Game theoretic analysis of call-by-value computation

  • Session 4: Semantics I
  • Conference paper
  • First Online:
Book cover Automata, Languages and Programming (ICALP 1997)

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

Included in the following conference series:

Abstract

We present a general semantic universe of call-by-value computation based on elements of game semantics, and validate its appropriateness as a semantic universe by the full abstraction result for call-by-value PCF, a generic typed programming language with call-by-value evaluation. The key idea is to consider the distinction between call-by-name and call-by-value as that of the structure of information flow, which determines the basic form of games. In this way call-by-name computation and call-by-value computation arise as two independent instances of sequential functional computation with distinct algebraic structures. We elucidate the type structures of the universe following the standard categorical framework developed in the context of domain theory. Mutual relationship between the presented category of games and the corresponding call-by-name universe is also clarified.

Supported in part by EPSRC Fellowships and JSPS Research Fellowships.

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. Abelson, H., Sussman, G.J., Structure and Interpretation of Computer Program, MIT Press, 1985.

    Google Scholar 

  2. Abramsky, S. and Jagadeesan, R., Games and Full Completeness for Multiplicative Linear Logic, Journal of Symbolic Logic, 59(2), pp. 543–574, 1994.

    Google Scholar 

  3. Abramsky, S., Jagadeesan, R. and Malacaria, P., Full Abstraction for PCF, 1994. To appear.

    Google Scholar 

  4. Abramsky, S. and McCusker, G., Linearity, Sharing and State: a fully abstract game semantics for Idealized Algol with active expressions, ENTCS, Vol.3, North Holland, 1996.

    Google Scholar 

  5. Abramsky, S. and McCusker, G., Call-by-value games, a typescript, 12p, Apr. 1997.

    Google Scholar 

  6. Berry, G. and Curien, P. L., Sequential algorithms on concrete data structures. TCS Vol.20, pp.265–321, North-Holland, 1982.

    Google Scholar 

  7. Blass, A., A game semantics for linear logic, Annuals of Pure and Applied Logic, 56:183–220, 1992.

    Google Scholar 

  8. Curien, P. L., Sequentiality and full abstraction. In Proc. of Application of Categories in Computer Science, LNM 177, pp.86–94, Cambridge Press, 1995.

    Google Scholar 

  9. Danos, V. and Regnier, L., Games and abstract machines. LICS'96, IEEE, 1994.

    Google Scholar 

  10. Felshcer, W., Dialogue games as a foundation for intuitionistic logic, Handbook of Philosophical logic, Vol.3, pp.341–372, D. Reidel Publishing Company, 1986.

    Google Scholar 

  11. Fiore, M., Axiomatic Domain Theory in Category of Partial Maps, PhD thesis. ECS-LFCS-94-307, Univ. of Edinburgh, 1994.

    Google Scholar 

  12. Fiore, M. and Plotkin, G., An Axiomatisation of Computationally Adequate Domain Theoretic Models of FPC. LICS'94, pp.92–102, IEEE, 1994.

    Google Scholar 

  13. Freyd, P., Algebraically Complete Categories, In Proc. of Como. Category Theory Conference, LNM 1488, pp.95–104, Springer Verlag, 1991.

    Google Scholar 

  14. Girard, J.-Y., Linear Logic, TCS, Vol.50, pp.1–102, North-Holland, 1987.

    Google Scholar 

  15. Gunter, C., Semantics of Programming Languages: Structures and Techniques, MIT Press, 1992.

    Google Scholar 

  16. Harmer. R., Malacaria, P., Linear foundations of game semantics, a typescript, Sep. 1996.

    Google Scholar 

  17. Honda. K., Yoshida. N., Name-Passing Games: a functional universe, a typescript. 35p, Nov. 1996.

    Google Scholar 

  18. Honda, K. and Yoshida, N., Game-theoretic Analysis of Call-by-value Computation (full version of this paper), ftp-able at ftp.dcs.ed.ac.uk/export/kohei/cbvfull.ps.gz, Feb, 1997.

    Google Scholar 

  19. Hyland, M. and Ong, L., On Full Abstraction for PCF: I, II and III, 130 pages, ftp-able at theory.doc.ic.ac.uk/papers/Ong, 1994.

    Google Scholar 

  20. Hyland. M. and Ong, L., Pi-calculus, dialogue games and PCF, FPCA'93, ACM. 1995.

    Google Scholar 

  21. Laird, J., Full abstraction for functional languages with control, LICS'97, IEEE, 1997.

    Google Scholar 

  22. Kahn, G. and Plotkin, D., Domaines Concrets. INRIA Report 336, 1978.

    Google Scholar 

  23. Longo, G. and Moggi, E., Cartesian closed categories of enumarations for effective type-structures, LNCS 173, Springer-Varlag, 1984.

    Google Scholar 

  24. McCusker, G., Games and Full Abstraction for FPC. LICS'96, IEEE, 1996.

    Google Scholar 

  25. Milner, R., Fully abstract models of typed lambda calculi. TCS, Vol.4, 1–22, North-Holland, 1977.

    Google Scholar 

  26. Milner, R., A Calculus of Communicating Systems, LNCS 76, Springer-Verlag, 1980.

    Google Scholar 

  27. Milner, R., Functions as Processes. MSCS, 2(2), pp. 119–146, 1992.

    Google Scholar 

  28. Milner, R., Sorts and Types of π-Calculus, a manuscript, 43pp, 1990.

    Google Scholar 

  29. Milner, R., Polyadic π-Calculus: a tutorial. Proceedings of the International Summer School on Logic Algebra of Specification, Marktoberdorf, 1992.

    Google Scholar 

  30. Milner, R., Tofte, M. and Harper, R., The Definition of Standard ML, MIT Press, 1990.

    Google Scholar 

  31. Moggi, E., Partial morphisms in categories of effective objects, Info.&Comp., 76:250–277, 1988.

    Google Scholar 

  32. Moggi, E., Notions of Computations and Monads. Info.&Comp., 93(1):55–92, 1991.

    Google Scholar 

  33. Nickau. M., Hereditarily Sequential Functionals, LNCS 813, pp.253–264, Springer-Verlag, 1994.

    Google Scholar 

  34. Ong, L., Correspondence between Operational Semantics and Denotational Semantics, Handbook of Logic in Computer Science, Vol.4, pp.269–356, Oxford University Press, 1995.

    Google Scholar 

  35. Plotkin, G., LCF considered as a programming language, TCS, 5:223–255, North-Holland, 1975.

    Google Scholar 

  36. Plotkin, G., Lecture on Predomains and Partial Functions, Notes for a course given at the Center for the Study of Language and Information, Stanford, 1985.

    Google Scholar 

  37. Power, J., Robinson, E., Premonoidal Categories and Notions of Computation, To appear in MSCS.

    Google Scholar 

  38. Riecke, J., and Sandholm,A. Relational Account of Call-by-value Sequentiality, LICS'97, 1997.

    Google Scholar 

  39. Robinson, E. and Rosolini, P., Categories of Partial Maps, Info.&Comp., 79:95–130, 1988.

    Google Scholar 

  40. Sieber, K., Relating Full Abstraction Results for Different Programming Languages, FST/TCS'10, pp. 373–387, LNCS 472, Springer-Verlag, 1990.

    Google Scholar 

  41. Winskel, G., Synchronization Trees, TCS, Vol.34, pp. 33–82, North-Holland, 1985.

    Google Scholar 

  42. Winskel, G., The Formal Semantics of Programming Languages, MIT Press, 1993.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. LFCS, Department of Computer Science, University of Edinburgh, UK

    Kohei Honda & Nobuko Yoshida

Authors
  1. Kohei Honda
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Nobuko Yoshida
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Pierpaolo Degano Roberto Gorrieri Alberto Marchetti-Spaccamela

Rights and permissions

Reprints and permissions

Copyright information

© 1997 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Honda, K., Yoshida, N. (1997). Game theoretic analysis of call-by-value computation. In: Degano, P., Gorrieri, R., Marchetti-Spaccamela, A. (eds) Automata, Languages and Programming. ICALP 1997. Lecture Notes in Computer Science, vol 1256. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-63165-8_180

Download citation

  • DOI: https://doi.org/10.1007/3-540-63165-8_180

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-63165-1

  • Online ISBN: 978-3-540-69194-5

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation