Document Open Access Logo

Sequoidal Categories and Transfinite Games: A Coalgebraic Approach to Stateful Objects in Game Semantics

Authors William John Gowers, James Laird

PDF
Thumbnail PDF

File

LIPIcs.CALCO.2017.13.pdf
  • Filesize: 0.62 MB
  • 17 pages

Document Identifiers

Author Details

William John Gowers
James Laird

Cite AsGet BibTex

William John Gowers and James Laird. Sequoidal Categories and Transfinite Games: A Coalgebraic Approach to Stateful Objects in Game Semantics. In 7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 72, pp. 13:1-13:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
https://doi.org/10.4230/LIPIcs.CALCO.2017.13

Abstract

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.
Keywords
  • Game Semantics
  • Stateful Languages
  • Transfinite Games
  • Sequoid Operator

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. 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.
  2. 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.
  3. 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.
  4. 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.
  5. 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.
  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.
  7. 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.
  8. 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.
  9. Pierre Clairambault. A remark on jim laird’s games category for general references, 2008. Google Scholar
  10. 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.
  11. Martin Hyland. Game semantics. Semantics and logics of computation, 14:131, 1997. Google Scholar
  12. Neeman Itay. The Determinacy of Long Games. De Gruyter CY, 2008. URL: http://www.degruyter.com/view/product/178683.
  13. Bart Jacobs. Introduction to Coalgebra: Towards Mathematics of States and Observation, volume 59 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2016. Google Scholar
  14. 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.
  15. Yves Lafont. Logiques, catégories et machines. PhD thesis, Université Paris 7, 1988. Google Scholar
  16. J. Laird. A categorical semantics of higher-order store. In Proceedings of CTCS '02, number 69 in ENTCS. Elsevier, 2002. Google Scholar
  17. 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.
  18. 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.
  19. James Laird. Functional programs as coroutines: A semantic analysis. Logical methods in computer science. To appear. Google Scholar
  20. Joachim Lambek. A fixpoint theorem for complete categories. Mathematische Zeitschrift, 103(2):151-161, 1968. URL: http://dx.doi.org/10.1007/BF01110627.
  21. 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.
  22. 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. Google Scholar
  23. 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.
  24. Jan Mycielski. On the axiom of determinateness. Fundamenta Mathematicae, 53(2):205-224, 1964. URL: http://eudml.org/doc/213736.
  25. 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.
  26. Andrea Schalk. What is a categorical model for linear logic?, October 2004. URL: http://www.cs.man.ac.uk/~schalk/notes/llmodel.pdf.
  27. 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.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact