Category Theory
Zulip Server
Archive

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.


Stream: deprecated: logic

Topic: 3-player game semantics?


view this post on Zulip Haskell (Jan 05 2022 at 14:09):

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?

view this post on Zulip Tom Hirschowitz (Jan 05 2022 at 14:39):

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?

view this post on Zulip Sam Speight (Jan 05 2022 at 17:20):

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.

view this post on Zulip Sam Speight (Jan 05 2022 at 17:25):

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.

view this post on Zulip Sam Speight (Jan 05 2022 at 17:28):

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?

view this post on Zulip Morgan Rogers (he/him) (Jan 05 2022 at 17:29):

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.

view this post on Zulip Sam Speight (Jan 05 2022 at 17:32):

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.

view this post on Zulip Morgan Rogers (he/him) (Jan 05 2022 at 17:37):

The bra-ket expression that physicists manipulate, like xAy\langle x \mid A \mid y \rangle spring to mind, as a syntax with 3 parts. It's not a direct link to logic, but OP seemed curious about general instances.

view this post on Zulip Morgan Rogers (he/him) (Jan 05 2022 at 17:39):

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

view this post on Zulip Sam Speight (Jan 05 2022 at 17:58):

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.

view this post on Zulip Sam Speight (Jan 05 2022 at 18:03):

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..

view this post on Zulip Alex Gryzlov (Jan 05 2022 at 18:16):

You also get "3-way sequents" in focused sequent calculi like μμ~: https://ix.cs.uoregon.edu/~pdownen/publications/sequent-intro.pdf

view this post on Zulip Sam Speight (Jan 05 2022 at 18:17):

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.

view this post on Zulip Haskell (Jan 06 2022 at 08:04):

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).

view this post on Zulip Matteo Capucci (he/him) (Jan 06 2022 at 09:01):

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'

view this post on Zulip Alex Gryzlov (Jan 06 2022 at 14:26):

btw there's a dedicated https://categorytheory.zulipchat.com/#narrow/stream/233273-theory.3A-game.20semantics stream on this server

view this post on Zulip Tom Hirschowitz (Jan 11 2022 at 08:08):

@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 ABCA \to B \to C, there are three boards (AA, BB, and CC), and

Alternatively, depending on the considered variant of game semantics, there could be two external players, one playing as Player on AA, the other playing as Opponent on CC.

view this post on Zulip Chris Barrett (Jan 28 2022 at 08:39):

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.

view this post on Zulip Haskell (Feb 05 2022 at 14:35):

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.