Sequoidal Categories and Transfinite Games: A Coalgebraic Approach to Stateful Objects in Game Semantics
The non-commutative sequoid operator (/) on games was introduced to capture algebraically the presence of state in history-sensitive strategies in game semantics, by imposing a causality relation on the tensor product of games. Coalgebras for the functor A (/) _ - i.e., morphisms from S to A (/) S --- may be viewed as state transformers: if A (/) _ has a final coalgebra, !A, then the anamorphism of such a state transformer encapsulates its explicit state, so that it is shared only between successive invocations.
We study the conditions under which a final coalgebra !A for A (/) _ is the carrier of a cofree commutative comonoid on A. That is, it is a model of the exponential of linear logic in which we can construct imperative objects such as reference cells coalgebraically, in a game semantics setting. We show that if the tensor decomposes into the sequoid, the final coalgebra !A may be endowed with the structure of the cofree commutative comonoid if there is a natural isomorphism from !(A × B)to !A (x) !B. This condition is always satisfied if !A is the bifree algebra for A (/) _, but in general it is necessary to impose it, as we establish by giving an example of a sequoidally decomposable category of games in which plays will be allowed to have transfinite length. In this category, the final coalgebra for the functor A (/)_ is not the cofree commutative comonoid over A: we illustrate this by explicitly contrasting the final sequence for the functor A (/) _ with the chain of symmetric tensor powers used in the construction of the cofree commutative comonoid as a limit by Melliès, Tabareau and Tasson.
Game Semantics
Stateful Languages
Transfinite Games
Sequoid Operator
13:1-13:17
Regular Paper
William John
Gowers
William John Gowers
James
Laird
James Laird
10.4230/LIPIcs.CALCO.2017.13
Samson Abramsky and Radha Jagadeesan. Games and full completeness for multiplicative linear logic. The Journal of Symbolic Logic, 59(2):543-574, 1994. URL: http://arxiv.org/abs/1311.6057.
http://arxiv.org/abs/1311.6057
Samson Abramsky and Guy McCusker. Full abstraction for Idealized Algol with passive expressions. Theor. Comput. Sci., 227(1-2):3-42, September 1999. URL: http://dx.doi.org/10.1016/S0304-3975(99)00047-X.
http://dx.doi.org/10.1016/S0304-3975(99)00047-X
S. Abramsky and G. McCusker. Call-by-value games. In M. Neilsen and W. Thomas, editors, Proceedings of CSL '97, pages 1-17. Springer-Verlag, 1998. URL: http://dx.doi.org/10.1007/BFb0028004.
http://dx.doi.org/10.1007/BFb0028004
S. Abramsky, K. Honda and G. McCusker. A fully abstract games semantics for general references. In Proceedings of LICS '98. IEEE Press, 1998. URL: http://dx.doi.org/10.1109/LICS.1998.705669.
http://dx.doi.org/10.1109/LICS.1998.705669
Stefano Berardi and Ugo de'Liguoro. Total functionals and well-founded strategies. In Jean-Yves Girard, editor, Typed Lambda Calculi and Applications: 4th International Conference, TLCA'99 L'Aquila, Italy, April 7-9, 1999 Proceedings, pages 54-68. Springer Berlin Heidelberg, Berlin, Heidelberg, 1999. URL: http://dx.doi.org/10.1007/3-540-48959-2_6.
http://dx.doi.org/10.1007/3-540-48959-2_6
G. M. Bierman. What is a categorical model of Intuitionistic Linear Logic?, pages 78-93. Springer Berlin Heidelberg, Berlin, Heidelberg, 1995. URL: http://dx.doi.org/10.1007/BFb0014046.
http://dx.doi.org/10.1007/BFb0014046
Andreas Blass. Equivalence of two strong forms of determinacy. Proceedings of the American Mathematical Society, 52(1):373-376, 1975. URL: http://www.jstor.org/stable/2040166.
http://www.jstor.org/stable/2040166
Martin Churchill, Jim Laird, and Guy McCusker. Imperative programs as proofs via game semantics. CoRR, abs/1307.2004, 2013. URL: http://arxiv.org/abs/1307.2004.
http://arxiv.org/abs/1307.2004
Pierre Clairambault. A remark on jim laird’s games category for general references, 2008.
William John Gowers and James Laird. Sequoidal categories and transfinite games: A coalgebraic approach to stateful objects in game semantics. CoRR, abs/1706.00035, 2017. URL: http://arxiv.org/abs/1706.00035.
http://arxiv.org/abs/1706.00035
Martin Hyland. Game semantics. Semantics and logics of computation, 14:131, 1997.
Neeman Itay. The Determinacy of Long Games. De Gruyter CY, 2008. URL: http://www.degruyter.com/view/product/178683.
http://www.degruyter.com/view/product/178683
Bart Jacobs. Introduction to Coalgebra: Towards Mathematics of States and Observation, volume 59 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2016.
G. Janelidze and G.M. Kelly. A note on actions of a monoidal category. Theory and Applications of Categories [electronic only], 9:61-91, 2001. URL: http://eudml.org/doc/122510.
http://eudml.org/doc/122510
Yves Lafont. Logiques, catégories et machines. PhD thesis, Université Paris 7, 1988.
J. Laird. A categorical semantics of higher-order store. In Proceedings of CTCS '02, number 69 in ENTCS. Elsevier, 2002.
J. Laird. Locally boolean domains. Theoretical Computer Science, 342(1):132 - 148, 2005. URL: http://dx.doi.org/10.1016/j.tcs.2005.06.007.
http://dx.doi.org/10.1016/j.tcs.2005.06.007
J. Laird. Sequential algorithms for unbounded nondeterminism. Electronic Notes in Theoretical Computer Science, 319:271 - 287, 2015. URL: http://dx.doi.org/10.1016/j.entcs.2015.12.017.
http://dx.doi.org/10.1016/j.entcs.2015.12.017
James Laird. Functional programs as coroutines: A semantic analysis. Logical methods in computer science. To appear.
Joachim Lambek. A fixpoint theorem for complete categories. Mathematische Zeitschrift, 103(2):151-161, 1968. URL: http://dx.doi.org/10.1007/BF01110627.
http://dx.doi.org/10.1007/BF01110627
Paul Blain Levy. Infinite trace equivalence. Annals of Pure and Applied Logic, 151(2):170 - 198, 2008. URL: http://dx.doi.org/10.1016/j.apal.2007.10.007.
http://dx.doi.org/10.1016/j.apal.2007.10.007
G. McCusker. A fully abstract relational model of Syntactic Control of Interference. In Proceedings of Computer Science Logic '02, number 2471 in LNCS. Springer, 2002.
Paul-André Melliès, Nicolas Tabareau, and Christine Tasson. An Explicit Formula for the Free Exponential Modality of Linear Logic, pages 247-260. Springer Berlin Heidelberg, Berlin, Heidelberg, 2009. URL: http://dx.doi.org/10.1007/978-3-642-02930-1_21.
http://dx.doi.org/10.1007/978-3-642-02930-1_21
Jan Mycielski. On the axiom of determinateness. Fundamenta Mathematicae, 53(2):205-224, 1964. URL: http://eudml.org/doc/213736.
http://eudml.org/doc/213736
A. W. Roscoe. Unbounded non-determinism in CSP. Journal of Logic and Computation, 3(2):131, 1993. URL: http://dx.doi.org/10.1093/logcom/3.2.131.
http://dx.doi.org/10.1093/logcom/3.2.131
Andrea Schalk. What is a categorical model for linear logic?, October 2004. URL: http://www.cs.man.ac.uk/~schalk/notes/llmodel.pdf.
http://www.cs.man.ac.uk/~schalk/notes/llmodel.pdf
James Worrell. On the final sequence of a finitary set functor. Theoretical Computer Science, 338(1):184 - 199, 2005. URL: http://dx.doi.org/10.1016/j.tcs.2004.12.009.
http://dx.doi.org/10.1016/j.tcs.2004.12.009
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode