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: Dialectica

Topic: Dialectica and games

Valeria de Paiva (May 04 2022 at 20:44):

@Jérémie Koenig talked a little about the games in programming that he's most interested in. His slides on "Grounding Game Semantics in Categorical Algebra" from last year show more about how computing effects and games can interact (one of the many possible computing ways we can see this interaction). His way goes via polynomials, the theme of @Nelson Niu next week.

EDIT:
Other connections of Dialectica with games can be seen in

• Y. Lafont & T. Streicher, Games Semantics for Linear Logic, in Logic in Computer Science (LICS 91), p. 43-50, IEEE Computer Society Press (1991)

• Blass' paper Questions and Answers

• Jules Hedges "Dialectica and Games with Bidding"

• Compositional game theory Neil Ghani, Jules Hedges, Viktor Winschel, Philipp Zahn, https://arxiv.org/abs/1603.04641

Jérémie Koenig (May 27 2022 at 09:58):

A Dialectica object $A = (\alpha : U \times X \rightarrow 2)$ is a simultaneous two-player constant-sum game with payoffs in $\{0,1\}$:

• $U$ is the set of strategies available to the first player (proponent)
• $X$ is the set of strategies available to the second player (opponent)
• $\alpha(u, x)$ gives the payoff matrix

Some simple Dialectica homsets can be interpreted as:

• $I \multimap A$ winning strategies for the first player
• $\bot \multimap A$ arbitrary strategies for the first player
• $A \multimap \bot$ winning strategies for the second player
• $A \multimap I$ arbitrary strategies for the second player

The basic constructions match the usual game semantics of linear logic:

• In $A \mathbin{\&} B$ the opponent chooses which game is played
• In $A \oplus B$ the proponent chooses which game is played
• In $A \otimes B$ both games are played. The proponent must win both to win the overall game.

Question 1 Does this all work as expected, and what is the game-theoretic interpretation of the more complex constructions?
In particular the two versions of $[-,-]$ will give us a more general interpretation of morphisms in $\mathbf{DC}$ and $\mathbf{GC}$. This and constructions such as the $\oslash$ tensor product of $GC$ introduce sequentiality.

From there, we can take our exploration in two directions. The first one is traditional economic games.

Question 2 Using a more general lineale than $2$, can we do some classical game theory within DC or GC?
An example is to use $\mathbb{R}$ with addition, so that the payoff for $A \otimes B$ is the sum of the payoff in each game.

The second direction is game semantics: the use of games and strategies to characterize the behavior of program components. Here the potential distinguishing feature of Dialectica is the simultaneous aspect of the corresponsing games. This means it may be possible to use it to model concurrency without the complexity of event structures or coherence spaces. It could also overcome the awkwardness that often exists between game semantics and linear logic. However this kind of application requires partial definition and fixed points.

Question 3 What are some $\mathbf{DCPO}$-enriched Dialectica categories? What are $D\mathbf{DCPO}$ and $G\mathbf{DCPO}$ like?

We could then explore the connections between Dialectica and existing approaches to game semantics.

Question 4 Can we embed existing versions of game semantics into some Dialectica categories?

@Jan Rooduijn @Colin Bloomfield

Colin Bloomfield (May 27 2022 at 16:13):

Is a two player constant-sum game with payoffs in {0,1}, a game in which in all outcomes one player has outcome 0 (loses) and the other has outcome 1 (wins)? I was a little unsure what simultaneous means here: would a simultaneous game be like a footrace instead of a game of chess?

Are there any references on games you suggest I read in preparation? I found "A game semantics for linear logic" by Blass and thought it might be relevant. Also, thank you for proposing questions, they all look very interesting!

James Deikun (May 27 2022 at 16:28):

"Simultaneous" means neither player gets to know what move the other one picked before picking their own move.

Jérémie Koenig (May 27 2022 at 18:35):

Colin Bloomfield said:

Is a two player constant-sum game with payoffs in {0,1}, a game in which in all outcomes one player has outcome 0 (loses) and the other has outcome 1 (wins)?

Yes that is correct!

Are there any references on games you suggest I read in preparation? I found "A game semantics for linear logic" by Blass and thought it might be relevant.

Yes that paper is a good read and very relevant! In some ways it is the starting point for game semantics as used in programming languages. Beyond that the game semantics literature is quite vast and rich so it's difficult to point to any one thing, but for a light read I like to point to this high-level articulation of some of the principles:

• From CSP to Game Semantics, Abramsky 2010
  https://link.springer.com/chapter/10.1007/978-1-84882-912-1_2

My ACT'21 paper also covers some technical basics on game semantics and DCPOs (in a way that's not too deep in the weeds of the combinatorial structure of the λ-calculus etc..) in case that's useful:

• Grounding Game Semantics in Categorical Algebra (especially §3)
  https://www.cl.cam.ac.uk/events/act2021/papers/ACT_2021_paper_71.pdf

Other than that, this work by Glynn Winskel looks interesting because it looks like we could use it as a "map" of where Dialectica fits compared to various other models of interaction:

• Making Concurrency Functional, Winskel 2022
  https://arxiv.org/abs/2202.13910, https://www.youtube.com/watch?v=ywHNG6DYAGg
  

And of course there are the references which Valeria posted at the top of this topic, although to be honest I have not yet worked my way through all of them.

Valeria de Paiva (May 28 2022 at 16:13):

@Jérémie Koenig thanks for posting this here. I had already added your paper (I think the right one) and Winskel's paper (and talk) to our Google drive. maybe you want to add Abramsky's paper and the original Blass paper.

It would be good if you could put the Abramsky paper on the Google drive, as I am only finding it paying lots...

Jérémie Koenig (Jun 01 2022 at 21:09):

Since our internet is spotty, using Overleaf is tricky, but I have created a Github repository with our write-up so far:
https://github.com/jeremie-koenig/dialectica-games
I have also uploaded a copy of the PDF in our Google Drive.

Valeria de Paiva (Jun 01 2022 at 21:28):

Thanks, Jeremie! I hadn't expected the internet to be spotty!

Jeremie, have a look, if you can (with spotty internet everything gets more complicated) at "Building Models of Linear Logic" (with Andrea Schalk), Proc. AMAST-99, LNCS 1548, 1999. (there is also a TCS version, but the conference one is shorter, I'm putting a version in our Google Drive.)

Jérémie Koenig (Jun 02 2022 at 01:37):

Valeria de Paiva said:

"Building Models of Linear Logic" (with Andrea Schalk), Proc. AMAST-99, LNCS 1548, 1999.

This looks very interesting. I need to dig in more seriously tomorrow but it already prompted some thoughts after a perfunctory skim.

For example I suspect there is a similar relationship

• between Poly (ΣΠ1) and coherence spaces
• between ΣΠ2 and the "coherence games" we defined

and it might be possible to generalize that relationship to ΣΠL using variations on the presentation of coherence spaces in that paper.

Valeria de Paiva (Jun 02 2022 at 01:38):

cool @Jérémie Koenig !

I would prefer us to do Dial(Pos), Dial(CPO), Dial(DCPO), but I understand that you guys want the dependent types. This means we have to understand Tamara von Glehn's thesis, I believe

Jérémie Koenig (Jun 02 2022 at 01:51):

I'm not personally that committed to dependent types, and we could do essentially the same thing with $M_1 Set$, $M_2 Set$, $M_L Set$. It will be easier to vary the underlying category which is definitely part of what I'd like to do (Question 1). But so far the dependency hasn't made a big difference in the Dialectica -> coherence space translation, so we thought we might as well go for it.

Jérémie Koenig (Jun 02 2022 at 02:03):

Just to write it down somewhere, I was also thinking:
If $(U \xleftarrow{\alpha} X)$ has $U$ strategies, $X$ counter-strategies, $\alpha$ winning condition, this suggest a functor in the other direction, from coherence games to Dialectica. For a coherence game $A$ we take:

• U := the (general, possibly maximal) cliques for $A$
• X := the (general, possibly maximal) cliques for $A^\bot$
• \alpha(x, y) is whether $x \cap y$ (which should have at most, possibly exactly, one element) is a winning play / self-coherent token.

Here by "general clique" I mean $\forall a b \in x \mathbin{.} a \neq b \Rightarrow a \mathrel\text{coh} b$

Valeria de Paiva (Jun 02 2022 at 02:07):

@Jérémie Koenig sorry Jeremie, I'm not that proficient with the cliques, but this is interesting too.

Jérémie Koenig (Jun 02 2022 at 02:22):

^ I think what I said above comes out of our discussion of process spaces with @Charlotte Aten on Day 1 and how they compare to coherence spaces.

In case it's useful, the way I understand it, if we think of a coherence space as a game, with the tokens as plays, then a clique is a strategy for the game. So the correspondence with game semantics is:

• coherence space <-> game
• token (element of the web) <-> play
• clique <-> strategy
• pairwise coherence constraint of cliques <-> determinism constraint of strategies.

See also the correspondence here: 20220530_173145.jpg

So when you have a clique in $A$ (a system strategy) and a clique in the dual game $A^\bot$ (so an environment strategy), the one token they have in common will be the play that results from playing them against each other.

Jérémie Koenig (Jun 02 2022 at 02:29):

And in that context the maximal cliques are just the maximally defined strategies (so that we have a set of strategies/counter-stragies rather than a poset/DCPPO), which ensures that this common play does exist. Of course ideally we would want to account for the order structure on the Dialectica side to have a 1-to-1 correspondence.

But I guess the motto is:

• Dialectica <-> "normal form game" counterpart to
• Coherence spaces <-> "extensional form game"

Valeria de Paiva (Jun 02 2022 at 02:49):

@Jérémie Koenig I am sorry I need to think, I don't understand it.

Valeria de Paiva (Jun 02 2022 at 17:30):

hi @John Baez , I hope this is not inside practice: chemistry by mistake!

Jan Rooduijn (Jun 02 2022 at 19:24):

We've had some setbacks in the project.

• We thought that the functor $E : \Sigma \Pi \mathbb{2} \rightarrow \mathbf{CoG}$ was faithful. Unfortunately that is not the case, not even when restricted to a functor $D: \Sigma \Pi \mathbb{1} \rightarrow \mathbf{Coh}$. The reason is that if $q[j] = \emptyset$ for some $j$, then the information $f(i) = j$ is lost when applying $D$ to $(F, f)$.
• We even hoped that the $E$ would be full when the morphisms of $$\mathbf{CoG}$ are restricted to maximal relations. This is also not the case. A counterexample is given by the object $(p, P)$ with $p[1] = {i}$, $p[i] = {a}$ and $P(i, a) = \bot$.

Jeremy is now going to try to repair this by further tweaking $\mathbf{CoG}$. I'm going to look at relations with Joyal's category of Conway games.

Valeria de Paiva (Jun 02 2022 at 19:27):

hi @Jan Rooduijn , nice to hear from you!
setbacks are part of the process! do not worry, carry on trying variants.

Because I'm a pest, I will say again that instead of thinking of PiSigma2 (actuallly don't you mean SigmaPi2?) why not think of GSets=LDial? I'm sure we can make a nice category of games Dial_2 (Coh) or LDial(Coh)...
I just don't know if this works for Jeremie's goals

John Baez (Jun 02 2022 at 20:01):

Valeria de Paiva said:

hi John Baez , I hope this is not inside practice: chemistry by mistake!

John Baez (Jun 02 2022 at 20:02):

I don't know what you're referring to , @Valeria de Paiva.

Valeria de Paiva (Jun 02 2022 at 20:05):

hi @John Baez I think you deleted our stream and recreated it yesterday, at least this is how it looked from here. might be somethign to do with the spotty internet.

John Baez (Jun 02 2022 at 20:33):

No, I did some other silly thing and undid it. Sorry!

I marked this topic as "resolved". This happens when you accidentally click the little gray check mark to the right of the name of a topic.

Jérémie Koenig (Jun 02 2022 at 20:45):

Valeria de Paiva said:

I will say again that instead of thinking of PiSigma2 (actuallly don't you mean SigmaPi2?) why not think of GSets=LDial? I'm sure we can make a nice category of games Dial_2 (Coh) or LDial(Coh)...
I just don't know if this works for Jeremie's goals

This is definitely an interesting thing to explore, it is not completely clear if/how that would fit in with our angle so far of Dialectica <-> Coh read as Normal form <-> Extensive form games. (I agree we shouldn't bring in the extra complexity of ΣΠ2 on top of all that.)

Jan Rooduijn (Jun 02 2022 at 22:41):

Valeria de Paiva said:

hi Jan Rooduijn , nice to hear from you!
setbacks are part of the process! do not worry, carry on trying variants.

Because I'm a pest, I will say again that instead of thinking of PiSigma2 (actuallly don't you mean SigmaPi2?) why not think of GSets=LDial? I'm sure we can make a nice category of games Dial_2 (Coh) or LDial(Coh)...
I just don't know if this works for Jeremie's goals

Thanks, I indeed meant $\Sigma \Pi 2$ and I agree that it is a good idea to first look at the non-dependent version. We're discussing your other suggestions.

Colin Bloomfield (Jun 14 2022 at 20:43):

We have discussed how coherence games provide a general model of games. A (scored) coherence game is a pair (|A|, ^) where |A| is a set of "tokens" and ^ is a symmetric binary relation on |A|. The set |A| is to represent plays of the game, and ^ is a relation which holds between distinct plays u,v in |A|, whenever they form a coherent strategy for Player 1 (Alice) and ^ holds between a play u and itself whenever it is winning for Alice. (A strategy for Alice is a collection of plays, where from the same position in any two different plays Alice always makes the same move. Strategies need not be complete, i.e. always tell you what move to make. Thus the emptyset and any singleton consisting of a single play are always strategies for Alice.)

As outlined I don't see how to use coherence games to model concurrency. Consider a simple game where Alice and player 2 (Bob), each choose a number 1 or 2. If they both choose the same number then Alice wins, and if they choose different numbers Bob wins. This game can either be played simultaneously (both players choose numbers and simultaneously reveal them) or sequentially (Alice chooses and number and then Bob can choose a number based off of Alice's choice). Clearly in the simultaneous game, if Alice is a random number generator Bob cannot be guaranteed to win and in the second game Bob can always win by choosing the number Alice didn't choose. However, the coherence game model of both games is identical, because a strategy for Alice in both games is determined by choosing a single number, and the winning conditions for Alice are also the same.

I haven't been able to think of a different way to use coherence games to account for the difference between the two games described above. The only thing I can think of is to add an additional symmetric binary relation ~ on |A| so that when u,v are distinct plays, u ~ v whenever u and v form a coherent strategy for Bob, and u~u whenever u is a winning play for Bob. Plays of either the simultaneous or sequential game can be represented as order pairs (x,y) where x,y are in {1,2} and x represents Alice's number and y, Bob's number. thus |A| = { (x,y) : x,y \in {1,2} } and ...

the simultaneous game has relations:
(x,y) ^ (w,z) iff (x = w and (y \neq z or x = y))
(x,y) ~ (w,z) iff (y = z and (x \neq w or x \neq y))

And the sequential game has relations:
^ is the same as in the simultaneous game.
(x,y) ~ (w,z) iff (x \neq w or ( (x,y) = (w,z) and x \neq y ) ).

It is probably easier to just draw a graph whose vertices are the plays and have two colored edges for the relations and work out the two game graphs. In the first one there are two maximal player 2 strategies: Bob can either choose 1 or choose 2. In the second game, Bob has 4 maximal strategies: he can stubbornly choose 1 or 2 independent of what Alice does, he can foolishly copy what Alice does or he can wisely choose what Alice didn't.

Valeria de Paiva (Jun 15 2022 at 22:37):

Just saw your message @Colin Bloomfield Don't know if I can help with it. I am sure that you can read the linear logic connectives of Coh as a way of doing concurrency, as Coh is the prototypical model of LL. but this is probably not what you want, as this way we don't model strategies.
You can do Dial(Coh) and this is another model of LL, not described in the literature, but maybe has the same problem of not modelling strategies?
I haven't read Winskel's paper properly, but doesn't he do the kind of modelling you want? if not, why not?

Nelson Niu (Jun 16 2022 at 04:11):

@Colin Bloomfield I think the way of resolving the dilemma of your game is that while the simultaneous and sequential games are different from Bob’s point of view, they’re actually the same from Alice’s point of view, no? For her, it can’t really affect her strategy whether Bob goes at the same time as or after her or not, which is why when you make the coherence game for her for either version, there’s no difference.

But if you make the coherence game for Bob in the two different versions, you actually do get different coherence games, I think. Because in the sequential version, ^ does hold for (Alice picks 1, Bob picks 1) and (Alice picks 2, Bob picks 2): they form a coherent strategy because they don’t conflict, for even though Bob is making different moves, they are being made from different situations (Alice just picked 1 vs. Alice just picked 2). Whereas in the simultaneous version, ^ does not hold for (Alice picks 1, Bob picks 1) and (Alice picks 2, Bob picks 2), because with no information about what Alice is doing, Bob is in the exact same situation when it’s his turn to pick in both plays—and yet he makes different moves, so these plays are not coherent.

So I think what counts as “the same position” when defining ^ is the key to encoding concurrency here: something like “move A occurs ‘before’ move B iff when modeled from B’s POV, altering both move A and move B still yields a coherent play wrt ^”

Nelson Niu (Jun 16 2022 at 04:13):

Actually maybe this is already what you’re saying with your fix! It’s just that it’s possible to have things look exactly the same from Alice’s POV while entirely different from Bob’s POV, and the difference is whether you want to just build different coherence games for each player, like I’m doing above, or somehow encode both players’ POVs in the “same” coherence game, like you did

Colin Bloomfield (Jun 16 2022 at 08:38):

Nelson Niu said:

Actually maybe this is already what you’re saying with your fix! It’s just that it’s possible to have things look exactly the same from Alice’s POV while entirely different from Bob’s POV, and the difference is whether you want to just build different coherence games for each player, like I’m doing above, or somehow encode both players’ POVs in the “same” coherence game, like you did

Thanks for thinking about my question/confusion. :) It sounds like you agree that viewing coherence games as I outlined (which may not be the only view) one cannot distinguish between all of the games: Alice plays first, they play simultaneously and Bob plays first. I wonder if another solution is to have tokens not only represent complete plays, but also partial plays? Then the two games outlined before can be distinguished by the fact that the sequential game will have additional tokens, partial plays where Alice has made a move and Bob hasn't yet responded. Still I kind of like the symmetry of having a coherence relation for Alice and for Bob and not having to deal with partial plays. Also it seems a natural notion of morphism between these 2-coherence games is to have a relation which preserves the first coherence relation and reflects the second one. Anyway before I think about this more, I agree with Valeria that I should learn about how the LL connectives of Coh provide a way of doing concurrency as well as look more closely at Winkel's paper.

Added: I am recalling now that I think the games model by Coh do not have scoring, and including partial play tokens for such games is fine. However, with scoring, things get more complicated if one wants to preserve the nice structure of taking the dual game.

Jérémie Koenig (Sep 09 2022 at 23:57):

@Jan Rooduijn I think the games you define in the draft can be presented inductively as:

$G ::= \sum_{i \in I} G_i \mid \prod_{i \in I} G_i \mid \text{win} \mid \text{lose}$

Because those have quite a loose polarization structure, perhaps they correspond more to $G\mathbf{Set}$ than $D\mathbf{Set}$. I think this is also one reason for the issue you note with identity strategies.

Perhaps it would be useful to consider games with more constrained schedules:

• Proponent always starts
• The players alternate after each move

One way to do that is to use the grammar:

$H ::= \bigoplus_i \lnot H_i \mid \text{win}$

Here is an embedding of the $H$'s into the $G$'s which explains what I mean by the expressions above.
First, I'll define what it means to swap the players in a game, which is what "$\lnot$" should be read as:

$\text{flip}\big(\sum_i G_i \big) := \prod_i \text{flip}(G_i)$
$\text{flip}\big(\prod_i G_i \big) := \sum_i \text{flip}(G_i)$
$\text{flip}(\text{win}) := \text{lose}$
$\text{flip}(\text{lose}) := \text{win}$

Then we can $H \mapsto G$ as follows:

$\llbracket \bigoplus_i \lnot H_i \rrbracket := \sum_i \text{flip}( \llbracket H_i \rrbracket )$
$\llbracket \text{win} \rrbracket := \text{win}$

Jan Rooduijn (Sep 12 2022 at 13:50):

Jérémie Koenig said:

Jan Rooduijn I think the games you define in the draft can be presented inductively as:

$G ::= \sum_{i \in I} G_i \mid \prod_{i \in I} G_i \mid \text{win} \mid \text{lose}$

Because those have quite a loose polarization structure, perhaps they correspond more to $G\mathbf{Set}$ than $D\mathbf{Set}$. I think this is also one reason for the issue you note with identity strategies.

Perhaps it would be useful to consider games with more constrained schedules:

• Proponent always starts
• The players alternate after each move

One way to do that is to use the grammar:

$H ::= \bigoplus_i \lnot H_i \mid \text{win}$

Here is an embedding of the $H$'s into the $G$'s which explains what I mean by the expressions above.
First, I'll define what it means to swap the players in a game, which is what "$\lnot$" should be read as:

$\text{flip}\big(\sum_i G_i \big) := \prod_i \text{flip}(G_i)$
$\text{flip}\big(\prod_i G_i \big) := \sum_i \text{flip}(G_i)$
$\text{flip}(\text{win}) := \text{lose}$
$\text{flip}(\text{lose}) := \text{win}$

Then we can $H \mapsto G$ as follows:

$\llbracket \bigoplus_i \lnot H_i \rrbracket := \sum_i \text{flip}( \llbracket H_i \rrbracket )$
$\llbracket \text{win} \rrbracket := \text{win}$

Thanks, I understand what you mean. I do think it might be easier to show that these games form a category, but I don't see why they are more similar to $D\mathbf{Set}$? Don't the morphisms in $D\mathbf{Set}$, as we interpret them, have the property that the opponent starts rather than the proponent?

By the way, I think there may not be an issue with the identity morphisms after all and I added something about that to the draft.

Jérémie Koenig (Sep 13 2022 at 18:07):

Yes, the morphisms $A \rightarrow B \in D\mathbf{Set}$ start with an opponent move in $A$, but here the game $A$ in itself appears in a negative position, ie. from the point of view of the game $A$ alone this will be a proponent move.
What might happen is that the game $[A, B]$ we use to define morphisms would start with a trivial proponent move, so that the opening move in $A$ would be the second move in the composite game.

Colin Bloomfield (Oct 30 2022 at 18:49):

As a consequence of Valeria's thesis, $ D(Set) $ provides sound semantics for intuitionistic linear logic with the "of course" modality. Thus the logic with categorical semantics in D(Set) is at least as strong as ILL with "!". I was wondering if there is a known sequent calculus for the logic defined semantically by $ D(Set) $? Also, is it known if one can get complete semantics for ILL with "!" via some collection Dialectica categories?

Valeria de Paiva (Nov 15 2022 at 23:10):

hi, so sorry for the big delay, @Colin Bloomfield !

the logic with categorical semantics in D(Set) is at least as strong as ILL with "!".

well, ILL+! is equiprovable with IPL, right? so any sequent calculus for propositional Intuitionistic logic would work -- at the provability level.

but I don't get what you want to say with

if there is a known sequent calculus for the logic defined semantically by $ D(Set) $?

it seems to me that the usual sequent calculus for ILL is what you want?

Colin Bloomfield (Nov 28 2022 at 08:20):

No worries; thank you for your reply! For a category C, let P(C) be the poset you get from thinning C then taking the skeleton. For D(Set), (and D(C) more generally), it seems P respects the operations on D(Set) interpreting the connectives of ILL and probably ! as well? So it seems the logic defined by D(Set) categorically is the same as the one defined (algebraically) by P(D(Set)). I believe the algebra P(D(Set)) is a four-element chain which is actually equal to D(P(Set)) = D(2). If we denote the elements by 0 < A < E < 1, in the game perspective, each represents a terminal game: in 0, it is the proponent's move, and the proponent can't move and so loses, in A the opponent is immediately declared winner, in E the proponent is immediately declared the winner, and in 1 it is opponent's move, and the opponent can't move and so loses. I thought the logic defined by D(Set) might then be stronger than ILL + ! because it seems to be defined by a single four-element algebra. Actually, since D(2) is idempotent, it seems it validates $ a \vdash a \otimes a $, which is not valid in ILL?