In the paper Coalgebraic Games and Strategies F. Honsell, M. Lenisa, and R. Redamalla use the functor $F_A$(X) = ${\mathscr{P}_{<κ}}$(A×X) to define games coalgebraically. This is a functor from the category of $Set^* \to Set^*$ where $Set^*$ is the category of sets satisfying the antifoundation axioms.

They state that the final $F_A$ coalgebra is ($G_A$,id) and that a game is to be understood as an element of $G_A$, but I don't know where the final coalgebra construction for $F_A$ is explained in detail. Why would id be the coalgebraic function?

They write

The elements of the final coalgebra $G_A$ are the minimal graphs up-to bisimilarity.

To add a bit more context as to how this relates to games:

We consider a general notion of 2-player game of perfect information, where the two players are called Left (L) and Right (R). A game x is identified with its initial position; at any position, there are moves for L and R, taking to new positions of the game. By abstracting from superficial features of positions, games can be viewed as elements of the final coalgebra for the functor F$_A$(X) = $\mathscr{P}_{<κ}$(A×X), where A is a parametric set of atoms which encode information on moves and positions, i.e. move names, and the player who has moved, and $\mathscr{P}_{<κ}$ is the set of all subsets of cardinality < κ. The coalgebra structure captures, for any position, the moves of the players and the corresponding next positions.

as for the meaning of $\mathscr{P}_{<κ}$ this is explained in a later article "Multigames and strategies, coalgebraically"

$\mathscr{P}_{<κ}$is the set of all subsets of cardinality < κ, where κ can be ω, if only finitely branching games are considered, or it can be an inaccessible cardinal, if we are interested in more general games.

  • 1
    $\begingroup$ $\kappa=\omega$ in this case, I guess? $\endgroup$ – Asaf Karagila Jan 4 at 21:26
  • $\begingroup$ I think it is actually finite in this case. I added a bit more info above. $\endgroup$ – Henry Story Jan 4 at 21:39
  • 2
    $\begingroup$ I'm confused. You said "finite power set", namely the set of all finite subsets. Then how could $\kappa$ be finite? $\endgroup$ – Asaf Karagila Jan 4 at 21:40
  • $\begingroup$ I added an explanation of ${\mathscr{P}_{<κ}}$ taken from another article. It can be smaller the w or larger, depending on what game you want. $\endgroup$ – Henry Story Jan 4 at 23:40
  • 2
    $\begingroup$ They are using/assuming a strong form of anti-foundation which allows them to pretend they are iterating the operation $X\rightarrow \mathcal{P}(A\times X)$. In reality what I think they intend is for the objects of $G_A$ to be the sets (witnessed to exist by this strong form of anti-foundation) whose membership relation codes the iterates of some labeled transitional system. $\endgroup$ – Not Mike Jan 5 at 11:00

Your Answer

By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

Browse other questions tagged or ask your own question.