Hostname: page-component-cd9895bd7-jn8rn Total loading time: 0 Render date: 2024-12-23T16:31:31.687Z Has data issue: false hasContentIssue false
  • English
  • Français

Dynamic game semantics

Published online by Cambridge University Press:  18 December 2020

Norihiro Yamada Open the ORCID record for Norihiro Yamada [Opens in a new window]  and
Samson Abramsky Open the ORCID record for Samson Abramsky [Opens in a new window]
Norihiro Yamada*
Affiliation:
The University of Minnesota, Minneapolis, USA
Samson Abramsky
Affiliation:
The University of Oxford, Oxford, UK
*
*Corresponding author. Email: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

The present work achieves a mathematical, in particular syntax-independent, formulation of dynamics and intensionality of computation in terms of games and strategies. Specifically, we give game semantics of a higher-order programming language that distinguishes programmes with the same value yet different algorithms (or intensionality) and the hiding operation on strategies that precisely corresponds to the (small-step) operational semantics (or dynamics) of the language. Categorically, our games and strategies give rise to a cartesian closed bicategory, and our game semantics forms an instance of a bicategorical generalisation of the standard interpretation of functional programming languages in cartesian closed categories. This work is intended to be a step towards a mathematical foundation of intensional and dynamic aspects of logic and computation; it should be applicable to a wide range of logics and computations.

Keywords

Game semanticscategorical logicintensionality of computation
Type
Paper
Information
Mathematical Structures in Computer Science , Volume 30 , Issue 8 , September 2020 , pp. 892 - 951
Check for updates
Copyright
© The Author(s), 2020. Published by Cambridge University Press

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Abramsky, S. (1997). Semantics of interaction: An introduction to game semantics. In: Semantics and Logics of Computation, Publications of the Newton Institute, 1–31.Google Scholar
Abramsky, S., Jagadeesan, R. and Malacaria, P. (2000). Full abstraction for PCF. Information and Computation 163 (2) 409–470.CrossRefGoogle Scholar
Abramsky, S. and Jung, A. (1994). Domain theory. In: Handbook of Logic in Computer Science, Oxford University Press, New York.Google Scholar
Abramsky, S. and McCusker, G. (1999). Game semantics. In: Computational Logic, Springer, Berlin, Heidelberg, 1–55.Google Scholar
Abramsky, S. and Melliès, P.-A. (1999). Concurrent games and full completeness. In: Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science, IEEE Computer Society, 431.Google Scholar
Amadio, R. M. and Curien, P.-L. (1998). Domains and Lambda-Calculi, vol. 46, Cambridge, Cambridge University Press.CrossRefGoogle Scholar
Barendregt, H. P. (1984). The Lambda Calculus, vol. 3, Amsterdam, North-Holland.Google Scholar
Church, A. (1940). A formulation of the simple theory of types. The Journal of Symbolic Logic 5 (02) 56–68.CrossRefGoogle Scholar
Clairambault, P. and Harmer, R. (2010). Totality in arena games. Annals of Pure and Applied Logic 161 (5) 673–689.CrossRefGoogle Scholar
Curien, P.-L. (2006). Notes on game semantics. From the author’s web page.Google Scholar
Curien, P.-L. (2007). Definability and full abstraction. Electronic Notes in Theoretical Computer Science 172 301–310.CrossRefGoogle Scholar
Danos, V., Herbelin, H. and Regnier, L. (1996). Game semantics and abstract machines. In: Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science, IEEE Computer Society, 394.Google Scholar
Danos, V. and Regnier, L. (2004). Head linear reduction. Unpublished.Google Scholar
Dimovski, A., Ghica, D. R. and Lazić, R. (2005). Data-Abstraction refinement: A game semantic approach. In: International Static Analysis Symposium, Springer, 102–117.CrossRefGoogle Scholar
Ehrhard, T. and Regnier, L. (2003). The differential lambda-calculus. Theoretical Computer Science 309 (1) 1–41.CrossRefGoogle Scholar
Gierz, G., Hofmann, K. H., Keimel, K., Lawson, J. D., Mislove, M. and Scott, D. S. (2003). Continuous Lattices and Domains, (Encyclopedia of Mathematics and its Applications, pp. I-Iv). vol. 93, Cambridge, Cambridge University Press.CrossRefGoogle Scholar
Girard, J.-Y. (1987). Linear logic. Theoretical Computer Science 50 (1) 1–101.CrossRefGoogle Scholar
Girard, J.-Y. (1989). Geometry of interaction I: Interpretation of system F. Studies in Logic and the Foundations of Mathematics 127 221–260.CrossRefGoogle Scholar
Girard, J.-Y. (1990). Geometry of interaction II: Deadlock-Free algorithms. In: COLOG-88, Springer, 76–93.CrossRefGoogle Scholar
Girard, J.-Y. (1995). Geometry of interaction III : Accommodating the additives. In: Girard, Lafont and Regnier, (eds.) Advances in Linear Logic, 329–389, Cambridge, Cambridge University Press.CrossRefGoogle Scholar
Girard, J.-Y. (2003). Geometry of interaction IV: The feedback equation. In: Logic Colloquium, vol. 3, Citeseer, 76–117.Google Scholar
Girard, J.-Y. (2011). Geometry of interaction V: Logic in the hyperfinite factor. Theoretical Computer Science 412 (20) 1860–1883.CrossRefGoogle Scholar
Girard, J.-Y. (2013). Geometry of interaction VI: A blueprint for transcendental syntax. preprint.Google Scholar
Girard, J.-Y., Taylor, P. and Lafont, Y. (1989). Proofs and Types, vol. 7, Cambridge, Cambridge University Press.Google Scholar
Greenland, W. E. (2005). Game Semantics for Region Analysis. Phd thesis, University of Oxford.Google Scholar
Gunter, C. A. (1992). Semantics of Programming Languages: Structures and Techniques, Cambridge, MA, MIT press.Google Scholar
Hankin, C. (1994). Lambda Calculi: A Guide for computer scientists (Vol. 3), USA, Oxford University Press.Google Scholar
Harmer, R. (2004). Innocent game semantics. In: Lecture Notes, 2007.Google Scholar
Hilken, B. P. (1996). Towards a proof theory of rewriting: The simply typed 2λ-calculus. Theoretical Computer Science 170 (1–2) 407–444.CrossRefGoogle Scholar
Hyland, J. M. E. and Ong, C.-H. (2000). On full abstraction for PCF: I, II, and III. Information and Computation 163 (2) 285–408.CrossRefGoogle Scholar
Hyland, M. (1997). Game semantics. In: Semantics and Logics of Computation, vol. 14, New York, Cambridge University Press, 131.Google Scholar
Jacobs, B. (1999). Categorical Logic and Type Theory, vol. 141, Amsterdam, Elsevier.Google Scholar
Lambek, J. and Scott, P. J. (1988). Introduction to Higher-Order Categorical Logic, vol. 7, USA, Cambridge University Press.Google Scholar
Laurent, O. (2004). Polarized games. Annals of Pure and Applied Logic 130 (1–3) 79–123.CrossRefGoogle Scholar
Longley, J. and Normann, D. (2015). Higher-Order Computability, Heidelberg, Springer.CrossRefGoogle Scholar
McCusker, G. (1998). Games and Full Abstraction for a Functional Metalanguage with Recursive Types, London, Springer Science & Business Media.CrossRefGoogle Scholar
Mellies, P.-A. (2005). Axiomatic rewriting theory I: A diagrammatic standardization theorem. In: Processes, Terms and Cycles: Steps on the Road to Infinity, Springer, 554–638.CrossRefGoogle Scholar
Moggi, E. (1991). Notions of computation and monads. Information and Computation 93 (1) 55–92.CrossRefGoogle Scholar
Ong, C.-H. (2006). On model-checking trees generated by higher-order recursion schemes. In: 21st Annual IEEE Symposium on Logic in Computer Science (LICS’06), IEEE, 81–90.CrossRefGoogle Scholar
Ouaknine, J. (1997). A Two-Dimensional Extension of Lambek’s Categorical Proof Theory. Phd thesis, McGill University, Montréal.Google Scholar
Pitts, A. M. (2001). Categorical Logic. In: Handbook of Logic in Computer Science, New York, Oxford University Press, 39–123.Google Scholar
Plotkin, G. D. (1977). LCF considered as a programming language. Theoretical Computer Science 5 (3) 223–255.CrossRefGoogle Scholar
Rose, K. H. (1996). Explicit Substitution: Tutorial & Survey. Computer Science Department.Google Scholar
Scott, D. (1976). Data types as lattices. Siam Journal on Computing 5 (3) 522–587.CrossRefGoogle Scholar
Scott, D. S. (1993). A type-theoretical alternative to ISWIM, CUCH, OWHY. Theoretical Computer Science 121 (1) 411–440.CrossRefGoogle Scholar
Seely, R. A. (1987). Modelling computations: A 2-categorical framework. In: Proceedings of the 2nd Annual IEEE Symposium on Logic in Computer Science, IEEE Computer Society, 65–71.Google Scholar
Sørensen, M. H. and Urzyczyn, P. (2006). Lectures on the Curry-Howard Isomorphism, vol. 149, Amsterdam, Elsevier.Google Scholar
Winskel, G. (1993). The Formal Semantics of Programming Languages: An Introduction, Cambridge, MA, MIT Press.CrossRefGoogle Scholar