License: 
Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CALCO.2017.13
URN: urn:nbn:de:0030-drops-80454
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2017/8045/
Gowers, William John ;
Laird, James
Sequoidal Categories and Transfinite Games: A Coalgebraic Approach to Stateful Objects in Game Semantics
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.
BibTeX - Entry
@InProceedings{gowers_et_al:LIPIcs:2017:8045,
author = {William John Gowers and James Laird},
title = {{Sequoidal Categories and Transfinite Games: A Coalgebraic Approach to Stateful Objects in Game Semantics}},
booktitle = {7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017)},
pages = {13:1--13:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-033-0},
ISSN = {1868-8969},
year = {2017},
volume = {72},
editor = {Filippo Bonchi and Barbara K{\"o}nig},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2017/8045},
URN = {urn:nbn:de:0030-drops-80454},
doi = {10.4230/LIPIcs.CALCO.2017.13},
annote = {Keywords: Game Semantics, Stateful Languages, Transfinite Games, Sequoid Operator}
}
|
Keywords: |
|
Game Semantics, Stateful Languages, Transfinite Games, Sequoid Operator |
|
Collection: |
|
7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017) |
|
Issue Date: |
|
2017 |
|
Date of publication: |
|
17.11.2017 |
