You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
The usual way to interpret forall or exists or even (A -> B) is "you give me an A, I'll give you a B". I've only ever seen games between two players.
Is there a logic that can make productive use of 3-player (or more) games? Or alternatively, a proof that adding more than 2-players reduces to the 2 case?
Taken very loosely, I guess composition of strategies in game semantics may be understood as reducing any 3-player interaction to some 2-player one?
In Semantics of Interaction, Abramsky says:
Why the number 2? The key feature of games, by comparison with the many extant models of computation (labelled transition systems, event structures, etc. etc.) is that they provide an explicit representation of the environment, and hence model interaction in an intrinsic fashion. (By contrast, interaction is modelled in, say, labelled transition systems using some additional structure, typically a “synchronization algebra” on the labels.) One-person games would degenerate to transition systems; it seems that multi-party interaction can be adequately modeled by two-person games, in much the same way that functions with multiple arguments can be reduced to one-place functions and tupling.
In terms of logic/type theory, I guess this has to do with the fact that we have the things to the left of the turnstile and the things to the right of the turnstile, ie. the turnstile separates things into two parts: the environment and the system, the hypotheses (context) and the conclusion, or whatever you want to call them.
I suppose this doesn't rule out 3-player games being useful for something, but I don't know what.
@Tom Hirschowitz composition understood this way is a particular kind of 3-player game, right? One in which the third player is "in the middle" of the other two. So it is not like all three of them are involved in a single game, each taking a turn going round in a circle. Is it this more "equal-footing" 3-player game you had in mind, @Haskell?
Sam Speight said:
In terms of logic/type theory, I guess this has to do with the fact that we have the things to the left of the turnstile and the things to the right of the turnstile, ie. the turnstile separates things into two parts: the environment and the system, the hypotheses (context) and the conclusion, or whatever you want to call them.
There's nothing preventing other shapes of expression, though! 2 is just one of the simplest cases.
Morgan Rogers (he/him) said:
Sam Speight said:
In terms of logic/type theory, I guess this has to do with the fact that we have the things to the left of the turnstile and the things to the right of the turnstile, ie. the turnstile separates things into two parts: the environment and the system, the hypotheses (context) and the conclusion, or whatever you want to call them.
There's nothing preventing other shapes of expression, though! 2 is just one of the simplest cases.
Sure! But what kind of thing are you thinking of? I can't think of any examples off the top of my head.
The bra-ket expression that physicists manipulate, like spring to mind, as a syntax with 3 parts. It's not a direct link to logic, but OP seemed curious about general instances.
There's also the evident caveat that most formal logic and math is quite 1-dimensional in its presentation; a syntax for a symmetric "3-player logic" wouldn't sit very naturally in 1-d
Interesting. I'm finding it hard to break out of that "two things separated by a turnstile" or "1-d" paradigm. Generally I'm used to thinking of things as morphisms in a category, and there we fall into the same paradigm. Like arrows go from something to something - that's two things. Then multicategories reduce to this paradigm by tupling, as in the Abramsky quote.
But I'm curious as to what kind of computational process (if any) could be modeled by an "equal-footing" 3-player game - which is the kind of game I took the OP to be asking about. So P1 moves first, then P2, then P3, then back to P1, etc..
You also get "3-way sequents" in focused sequent calculi like μμ~: https://ix.cs.uoregon.edu/~pdownen/publications/sequent-intro.pdf
Sam Speight said:
Interesting. I'm finding it hard to break out of that "two things separated by a turnstile" or "1-d" paradigm. Generally I'm used to thinking of things as morphisms in a category, and there we fall into the same paradigm. Like arrows go from something to something - that's two things. Then multicategories reduce to this paradigm by tupling, as in the Abramsky quote.
Maybe a better way of putting this is in your 1-d terms: an arrow is 1-d; information flows in one direction.
My intuition of 2-player was also something like the 'Cartesian boundary' as in Abramsky (ie. there's just you and an environment in an adversarial context).
In that same setting, if a part of the environment is also adversarial against another part of the environment, maybe then modeling it as 3-player would be natural. Lumping "everything that isn't you" into a single 'Environment' would be less useful (again, unless we have a reduction).
I guess this 2 is the same 2 as in 'how many ends of an arrow in a category' and 'how many variances are there for a functor'
btw there's a dedicated https://categorytheory.zulipchat.com/#narrow/stream/233273-theory.3A-game.20semantics stream on this server
@Sam Speight I've never been too sure about how to interpret composition of strategies as a 3-player game. I'd rather say that in a composition of strategies , there are three boards (, , and ), and
Player 1 plays on (as Opponent) and (as Player),
Player 2 plays on (as Opponent) and (as Player), and
there is a third, external player, called Opponent, who plays on (as Player) and (as Opponent).
Alternatively, depending on the considered variant of game semantics, there could be two external players, one playing as Player on , the other playing as Opponent on .
I could imagine it might be natural to model certain self-dual phenomenon in terms of a third, neutral, player. For example, perhaps probabilistic or non-deterministic choice might be decisions made by such a neutral player.
Running with 2 being the answer to "how many ends of an arrow"...
I recall (with little detail) that k-cospans reduce to 2-cospans when using them to model morphisms in open systems (see @John Baez 's talk in ICRA 2021), by taking coproducts appropriately.
So maybe that would have something to say about k-player games reducing to 2-player games.