Nerdsniped myself by finding a thought in journals from early this year trying to understand specifically the notion of the **sum** of games in the sense of Conway-Berlekamp-Guy-style combinatorial game theory --- in the context of focused linear logic. This is something that I hadn't previously seen treated in (what embarrassingly little literature I have read about) game semantics for linear logic. These certainly seemed gamey enough in the sense of possessing the quantifier-alternation that comes out of the alternation of focusing phases. But tensor, or dually par in a classical setting, the things that you'd think might mean "plop these two games down next to each other and play them jointly" doesn't capture what addition of surreal numbers does. *If* it's the synchronous player's turn, then for that turn you choose one of them to play in, to focus on. If on the other hand it's the asynchronous player's turn, one of them gets nondeterministically selected to be played in.
So I tried to come up with some fiddly token-passing translation (of course) to understand it through, because that's the one hammer I have.
I ended up with a very strange sort of... tri-polar? syntax for the source language. I have
positive props P ::= ↓G | P ⊕ P | 0
negative props N ::= ↑G | N & N | ⊤
games G ::= {N|P} | G + G
The notation `{N|P}` is meant to echo the ONAG notation of left and right moves. For the fiddly translation, conjure up parametrically (i.e. imagine you are invoking ∀R or ∃L to get them) a plain old set-theoretic set S, and a distinguished point `x ∈` S of it. The translation has three phases:
`[P, a, b]` outputs a positive proposition in linear logic
`[N, a, b]` outputs a negative proposition in linear logic
`[G, a, b]` outputs a positive proposition in linear logic and both a and b are subsets of S. The translation is:
[P1 ⊕ P2, a, b] = [P1, a, b] ⊕ [P2, a, b]
[0, a, b] = 0
[N1 & N2, a, b] = [N1, a, b] & [N2, a, b]
[⊤, a, b] = ⊤
[↓G, a, b] = (x ∈ b) ⊗ [G, a, b]
[↑G, a, b] = ↑((x ∉ b) ⊗ [G, a, b])
[G1 + G2, a, b] = ∃c1,c2.(a = c1 ∩ c2) ⊗ [G1, c1, b] ⊗ [G2, c2, b]
[{N|P}, a, b] = ↓(((x ∈ a) ⊸ [N, a, b]) & ((x ∉ a) ⊸ ↑[P, a, b]))
and you read off "Left player wins G assuming Left starts" by the provability of
`∃a.[↓G, a, a] ⊦ 0` and "Left player wins G assuming Right starts" by the provability of
`∃a.[↑G, a, a] ⊦ 0` The propositions x ∈ a and x ∉ a are passed around as linear tokens in the context signalling that it's left's (∈) or right's (∉) turn to play, and the subset a that we're concerned about the point x being in or not gives the address of the current part of the expression tree that the player is thinking about moving in. Doing proof search starting from ∃a.[↓(G1 + G2), a, a] ⊦ 0 we get to the state
`(x ∈ a), ∃c1,c2.(a = c1 ∩ c2) ⊗ [G1, c1, a] ⊗ [G2, c2, a] ⊦ 0` and thence to
`(x ∈ c1 ∩ c2), [G1, c1, c1 ∩ c2] ⊗ [G2, c2, c1 ∩ c2] ⊦ 0` which is equivalent to
`(x ∈ c1) & (x ∈ c2), [G1, c1, c1 ∩ c2], [G2, c2, c1 ∩ c2] ⊦ 0` so the synchronous player, whose turn it is, has to make a choice whether to play in [G1, c1, c1 ∩ c2], which will consume (x ∈ c1) and eventually yield (x ∉ c1 ∩ c2), or to play in [G2, c2, c1 ∩ c2], which will consume (x ∈ c2) and eventually yield (x ∉ c1 ∩ c2). But then note that (x ∉ c1 ∩ c2) is equivalent to (x ∉ c1) ⊕ (x ∉ c2) --- the *asynchronous* player makes a nondeterministic choice among the two subgames to play in, as they should.
With this setup I can show through an easy induction that the zero game **0** = {⊤|0} (I'm being careful to distinguish the zero game **0** where both players have no options from the logical 0 which is specifically about the asynchronous player having no options) actually is a unit for addition, i.e. `G ⊣⊢ {⊤|0} + G`, by which I mean `[G, a, a] ⊣⊢ [{⊤|0} + G, a, a]`, but two sad things happen:
- This proof seems to break if I try to add multiplicatives to the source language
- I don't get equivalence of the zero game with the nim game consisting of two heaps of size one, written
`{*|*}` in ONAG notation, and `{{{⊤|0}|{⊤|0}}|{{⊤|0}|{⊤|0}}}` in my language here. The logical treatment seems to think that it's "better" that you can make at least one move in `{*|*}`, where as you don't even have a move in **0**, so bisimulation fails.
However, if we write **1** = {**0**|0}, then the logic can tell that two representations of **2** are equivalent: `{`**1**|0} ⊣⊢ {**0** & **1**|0} (in ONAG notation this would have been written `{`**1**|} = {**0**,**1**|}) |