Games, Arenas, and Strategies

Proof. Induction on $s$. The first clause appends a $P$-move whose justifier lies in $\mathrm{pv}(s)$ by the visibility condition. The second restarts the view at an initial move, which needs no pointer. The third appends an $O$-move whose justifier is $m$, the last move of $\mathrm{pv}(sm)$, so the pointer targets a retained move. No clause deletes a move that is the target of a retained pointer, since deletion occurs only in the third clause and only for the block $t$, whose moves are not targets of the appended pointer. ◻

Proof. The labelling of $A\Rightarrow B$ exchanges $O$ and $P$ on the $A$-component, and that of $B\Rightarrow C$ exchanges them on the $B$-component; so a single $B$-move receives opposite labels in the two restrictions, which is the first claim. Inside a block the two strategies therefore alternate: after a $B$-move by one of them, the other must answer, and neither can terminate the block by playing in $B$. A block is left by a move outside $B$, which by definition 157.3 must be justified outside $B$. Counting from the $A\Rightarrow B$ side, a block begins with a $P$-move of $\sigma$ and ends with an $O$-move of $\sigma$, so its length is odd. ◻

Proof. Plays. Deleting a $B$-block of odd length exchanges parity exactly once, so by lemma 157.8 the visible moves of $u\upharpoonright A,C$ alternate and the sequence begins with an $O$-move. Well-bracketing: a deleted block is itself well-bracketed, so the stack of pending questions of the visible play is unchanged across it, and a composed pointer still targets the most recent unanswered visible question. Visibility: an induction on $u$ shows that $\mathrm{pv}(u\upharpoonright A,C)$ is the image of $\mathrm{pv}(u)$ under deletion, using lemma 157.5; hence a justifier visible in $\mathrm{pv}(u)$ remains visible after deletion.

Even-prefix closure. If $u\upharpoonright A,C=smn$, the prefix of $u$ ending at the last move restricting to $s$ is again an interaction sequence, and its two restrictions are even-length prefixes of members of $\sigma$ and $\tau$, hence members.

Determinism. Let $u,u^{\prime }\in \sigma \Vert \tau$ restrict to $smn$ and $sm{n}^{\prime }$, and let $v$ be their longest common prefix. By lemma 157.8 exactly one of the two strategies is to move after $v$, and that strategy is deterministic, so $u$ and $u^{\prime }$ agree one move further. Iterating contradicts maximality of $v$ unless the two restrictions coincide, whence $n=n^{\prime }$ with the same pointer. ◻

Proof. Identity laws. Let $\sigma :A\Rightarrow B$. In an interaction of ${\mathrm{id}}_A$ with $\sigma$, whenever ${\mathrm{id}}_A$ is to move it copies the last move across, so the interaction sequence is determined by $\sigma$ and is exactly the image of a play of $\sigma$ under duplicating $A$-moves. Restricting to the outer $A$ and to $B$ returns that play, so $\sigma \circ {\mathrm{id}}_A=\sigma$; the other unit law is symmetric.

Associativity. For $\sigma :A\Rightarrow B$, $\tau :B\Rightarrow C$ and $\upsilon :C\Rightarrow D$ consider the sequences over $M_A+M_B+M_C+M_D$ whose three consecutive two-component restrictions lie in $\sigma$, $\tau$ and $\upsilon$. Both $(\upsilon \circ \tau )\circ \sigma$ and $\upsilon \circ (\tau \circ \sigma )$ arise from this set by deleting $B$ and $C$ in the two possible orders, and deletion of disjoint sets of moves commutes and composes pointers associatively. It remains to see that every element of either composite arises from a four-component sequence: given witnesses $u$ for the outer composition and $v$ for the inner one, they agree on the moves they share by determinism of the strategies involved, and by lemma 157.8 no move is scheduled twice, so they amalgamate. ◻

Proof. For copycat, the $P$-view determines the last $O$-move and its justifier, which is all the copying rule consults; the copied answer answers the copy of the question that was answered on the other side, so bracketing holds.

For composition, prove by induction on interaction sequences that $\mathrm{pv}(u)$ is obtained from $\mathrm{pv}(u\upharpoonright A,C)$ by inserting at each position a $B$-block that is determined by ${\mathrm{f}}_{\sigma }$ and ${\mathrm{f}}_{\tau }$ alone. The base case is empty; the inductive step is the case analysis of lemma 157.8, in which the strategy about to move consults only its own $P$-view, available by the induction hypothesis. It follows that two plays of $\tau \circ \sigma$ with equal $P$-views have equal interaction $P$-views and hence equal continuations, which is innocence. Well-bracketing was shown in proposition 157.9. ◻

Proof. Proposition 157.13 gives closure under composition and contains the identities; the laws are inherited from theorem 157.11. ◻

Proof. An initial move of $A\times B$ lies in exactly one summand, and by definition 157.4 every later move is hereditarily justified by it; so a play of $C\Rightarrow A\times B$ has all its $A\times B$-moves in one summand, and the set of such plays splits as a disjoint union. Define $⟨\sigma ,\tau ⟩$ to be $\sigma$ on the plays whose initial move is in $A$ and $\tau$ on those whose initial move is in $B$; determinism and even-prefix closure are inherited summandwise, and innocence holds because the $P$-view of a play determines its initial move. The two equations follow from the identity law of theorem 157.11 applied inside each summand, and uniqueness holds because the splitting is forced. Terminality of $\mathbf{1}$ is the observation that $\mathbf{1}\Rightarrow$ nothing may be played after the unique answer, so exactly one strategy exists. ◻

Proof. The two arenas $(C\times A)\Rightarrow B$ and $C\Rightarrow (A\Rightarrow B)$ have the same moves, namely $M_A+M_B+M_C$, and the same labels: on the left the $O/P$ roles are exchanged on $C$ and on $A$, and on the right they are exchanged on $C$ and, inside $A\Rightarrow B$, exchanged again on $A$ — which is one exchange in total, the same as on the left. The enabling relations differ only in that on the right an initial move of $A$ is enabled by an initial move of $B$, whereas on the left it is enabled by an initial move of $B$ through the pairing; in both cases the hereditary justifier of every $A$-move is an initial $B$-move. Hence the two sets of justified sequences coincide, and the conditions of definition 157.4 are conditions on labels and pointers only, so the plays coincide. Take $\mathrm{\Lambda }$ to be the identity on sets of plays. It preserves determinism, prefix closure, $P$-views — hence innocence — and the pending-question stack — hence bracketing. Naturality in $C$ is the statement that composition with a strategy $C^{\prime }\Rightarrow C$ is computed by the same interaction on both sides, which holds because the move sets agree. ◻

Proof. A union of a directed family of even-prefix-closed sets is even-prefix closed. Determinism is preserved: two continuations of the same play lie in a common member of the family by directedness, hence agree. Innocence and bracketing are conditions on individual plays and on pairs of plays with equal views, and both are again settled inside a common member. Continuity of composition: an element of $\tau \circ (\bigcup _i{\sigma }_i)$ is witnessed by a single interaction sequence, which is finite, so all the $\sigma$-plays it uses lie in one ${\sigma }_i$; the converse inclusion is monotonicity. ◻

Proof. Each reduction rule is one of: a $\beta$-step, handled by proposition 157.16 together with the identity law; a constant step, handled by unfolding the view functions of definition 157.17 and observing that the two sides have the same view function; or the unfolding of $\mathsf{fix}$, which holds because $\bigcup _n{\mathrm{\Phi }}^n(\mathrm{\varnothing })$ is a fixed point of the continuous $\mathrm{\Phi }$ by lemma 157.18. Compatibility with contexts is functoriality of the interpretation, which is theorem 157.11. ◻

Proof. $(\Leftarrow )$ is proposition 157.20 together with $[[\underset{―}{n}]]=\{qn\}$, computed from definition 157.17.

$(\Rightarrow )$ is proved by a logical relation between strategies and terms. For each type $\sigma$ define a relation ${⊲}_{\sigma }$ between innocent strategies on $[[\sigma ]]$ and closed terms of type $\sigma$:

• $\rho {⊲}_{\iota }M$ iff $qn\in \rho$ implies $M\Downarrow \underset{―}{n}$, and similarly at $o$;

• $\rho {⊲}_{\sigma \to \tau }M$ iff $\mathrm{ev}\circ ⟨\rho ,{\rho }^{\prime }⟩{⊲}_{\tau }MN$ whenever ${\rho }^{\prime }{⊲}_{\sigma }N$.

Each ${⊲}_{\sigma }$ is closed under directed unions in its first argument: at $\iota$ because a play in the union lies in a member, and at higher types because $\mathrm{ev}$ is continuous by lemma 157.18; and $\mathrm{\varnothing }{⊲}_{\sigma }M$ always, again by induction on $\sigma$. The fundamental lemma states that for $x_1:{\sigma }_1,\dots ,x_k:{\sigma }_k⊢M:\tau$ and closed $N_i$ with ${\rho }_i{⊲}_{{\sigma }_i}{N}_i$, $$[[M]]\circ ⟨{\rho }_1,\dots ,{\rho }_k⟩{⊲}_{\tau }M[N_1/x_1,\dots ,N_k/x_k].$$ It is proved by induction on $M$. Variables and abstraction use proposition 157.15, proposition 157.16; application is the defining clause of ${⊲}_{\sigma \to \tau }$; the constants are checked directly from their view functions, the conditional using the two operational rules for $\mathsf{if}$; and $\mathsf{fix}$ uses closure under directed unions together with $\mathrm{\varnothing }{⊲}_{\sigma }M$ and induction on the approximants of definition 157.19. Instantiating the fundamental lemma at a closed term of type $\iota$ gives $[[M]]{⊲}_{\iota }M$, which is the required implication. The final claim follows: $[[M]]\ne \mathrm{\varnothing }$ forces some $qn\in [[M]]$, since a nonempty strategy on $\iota$ contains a play of length two. ◻