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 '19 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 '19 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 '19 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 '19 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 '19 at 11:00

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.