×

Dynamic game semantics. (English) Zbl 1495.68128

Summary: 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.

MSC:

68Q55 Semantics in the theory of computing
03G30 Categorical logic, topoi
18C50 Categorical semantics of formal languages
68N15 Theory of programming languages
68Q01 General topics in the theory of computing
PDFBibTeX XMLCite
Full Text: DOI arXiv

References:

[1] Abramsky, S. (1997). Semantics of interaction: An introduction to game semantics. In: Semantics and Logics of Computation, Publications of the Newton Institute, 1-31. · Zbl 0938.91500
[2] Abramsky, S., Jagadeesan, R. and Malacaria, P. (2000). Full abstraction for PCF. Information and Computation163 (2) 409-470. · Zbl 1006.68028
[3] Abramsky, S. and Jung, A. (1994). Domain theory. In: Handbook of Logic in Computer Science, Oxford University Press, New York.
[4] Abramsky, S. and Mccusker, G. (1999). Game semantics. In: Computational Logic, Springer, Berlin, Heidelberg, 1-55. · Zbl 0961.68080
[5] 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.
[6] Amadio, R. M. and Curien, P.-L. (1998). Domains and Lambda-Calculi, vol. 46, Cambridge, Cambridge University Press. · Zbl 0962.03001
[7] Barendregt, H. P. (1984). The Lambda Calculus, vol. 3, Amsterdam, North-Holland. · Zbl 0558.03006
[8] Church, A. (1940). A formulation of the simple theory of types. The Journal of Symbolic Logic5 (02) 56-68. · JFM 66.1192.06
[9] Clairambault, P. and Harmer, R. (2010). Totality in arena games. Annals of Pure and Applied Logic161 (5) 673-689. · Zbl 1225.03029
[10] Curien, P.-L. (2006). Notes on game semantics. From the author’s web page.
[11] Curien, P.-L. (2007). Definability and full abstraction. Electronic Notes in Theoretical Computer Science172301-310.
[12] 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.
[13] Danos, V. and Regnier, L. (2004). Head linear reduction. Unpublished.
[14] Dimovski, A., Ghica, D. R. and Lazić, R. (2005). Data-Abstraction refinement: A game semantic approach. In: International Static Analysis Symposium, Springer, 102-117. · Zbl 1141.68366
[15] Ehrhard, T. and Regnier, L. (2003). The differential lambda-calculus. Theoretical Computer Science309 (1) 1-41. · Zbl 1070.68020
[16] 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. · Zbl 1088.06001
[17] Girard, J.-Y. (1987). Linear logic. Theoretical Computer Science50 (1) 1-101. · Zbl 0625.03037
[18] Girard, J.-Y. (1989). Geometry of interaction I: Interpretation of system F. Studies in Logic and the Foundations of Mathematics127221-260.
[19] Girard, J.-Y. (1990). Geometry of interaction II: Deadlock-Free algorithms. In: COLOG-88, Springer, 76-93. · Zbl 0716.03047
[20] 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. · Zbl 0828.03027
[21] Girard, J.-Y. (2003). Geometry of interaction IV: The feedback equation. In: Logic Colloquium, vol. 3, Citeseer, 76-117. · Zbl 1105.03064
[22] Girard, J.-Y. (2011). Geometry of interaction V: Logic in the hyperfinite factor. Theoretical Computer Science412 (20) 1860-1883. · Zbl 1230.03093
[23] Girard, J.-Y. (2013). Geometry of interaction VI: A blueprint for transcendental syntax. preprint.
[24] Girard, J.-Y., Taylor, P. and Lafont, Y. (1989). Proofs and Types, vol. 7, Cambridge, Cambridge University Press. · Zbl 0671.68002
[25] Greenland, W. E. (2005). Game Semantics for Region Analysis. Phd thesis, University of Oxford. · Zbl 1099.62129
[26] Gunter, C. A. (1992). Semantics of Programming Languages: Structures and Techniques, Cambridge, MA, MIT press. · Zbl 0823.68059
[27] Hankin, C. (1994). Lambda Calculi: A Guide for computer scientists (Vol. 3), USA, Oxford University Press. · Zbl 0833.68070
[28] Harmer, R. (2004). Innocent game semantics. In: Lecture Notes, 2007.
[29] Hilken, B. P. (1996). Towards a proof theory of rewriting: The simply typed 2λ-calculus. Theoretical Computer Science170 (1-2) 407-444. · Zbl 0874.03017
[30] Hyland, J. M. E. and Ong, C.-H. (2000). On full abstraction for PCF: I, II, and III. Information and Computation163 (2) 285-408. · Zbl 1006.68027
[31] Hyland, M. (1997). Game semantics. In: Semantics and Logics of Computation, vol. 14, New York, Cambridge University Press, 131. · Zbl 0919.68084
[32] Jacobs, B. (1999). Categorical Logic and Type Theory, vol. 141, Amsterdam, Elsevier. · Zbl 0911.03001
[33] Lambek, J. and Scott, P. J. (1988). Introduction to Higher-Order Categorical Logic, vol. 7, USA, Cambridge University Press. · Zbl 0642.03002
[34] Laurent, O. (2004). Polarized games. Annals of Pure and Applied Logic130 (1-3) 79-123. · Zbl 1055.03020
[35] Longley, J. and Normann, D. (2015). Higher-Order Computability, Heidelberg, Springer. · Zbl 1471.03002
[36] Mccusker, G. (1998). Games and Full Abstraction for a Functional Metalanguage with Recursive Types, London, Springer Science & Business Media. · Zbl 0917.68192
[37] 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. · Zbl 1171.68515
[38] Moggi, E. (1991). Notions of computation and monads. Information and Computation93 (1) 55-92. · Zbl 0723.68073
[39] 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.
[40] Ouaknine, J. (1997). A Two-Dimensional Extension of Lambek’s Categorical Proof Theory. Phd thesis, McGill University, Montréal.
[41] Pitts, A. M. (2001). Categorical Logic. In: Handbook of Logic in Computer Science, New York, Oxford University Press, 39-123.
[42] Plotkin, G. D. (1977). LCF considered as a programming language. Theoretical Computer Science5 (3) 223-255. · Zbl 0369.68006
[43] Rose, K. H. (1996). Explicit Substitution: Tutorial & Survey. Computer Science Department.
[44] Scott, D. (1976). Data types as lattices. Siam Journal on Computing5 (3) 522-587. · Zbl 0337.02018
[45] Scott, D. S. (1993). A type-theoretical alternative to ISWIM, CUCH, OWHY. Theoretical Computer Science121 (1) 411-440. · Zbl 0942.68522
[46] 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.
[47] Sørensen, M. H. and Urzyczyn, P. (2006). Lectures on the Curry-Howard Isomorphism, vol. 149, Amsterdam, Elsevier. · Zbl 1183.03004
[48] Winskel, G. (1993). The Formal Semantics of Programming Languages: An Introduction, Cambridge, MA, MIT Press. · Zbl 0919.68082
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.