# Making Concurrency Functional

Glynn Winskel  Huawei Research Centre, Edinburgh, UK University of
Strathclyde, Glasgow, UK

###### Abstract.

The article bridges between two major paradigms in computation, the
functional, at basis computation from input to output, and the interactive,
where computation reacts to its environment while underway. Central to any
compositional theory of interaction is the dichotomy between a system and its
environment. Concurrent games and strategies address the dichotomy in fine
detail, very locally, in a distributed fashion, through distinctions between
Player moves (events of the system) and Opponent moves (those of the
environment). A functional approach has to handle the dichotomy more
ingeniously, via its blunter distinction between input and output. This has
led to a variety of functional approaches, specialised to particular
interactive demands. Through concurrent games we can see what separates and
connects the differing paradigms, and show how:

$\bullet$ to lift functions to strategies; the “Scott order” of concurrent
games turns functional dependency to causal dependency.

$\bullet$ several paradigms of functional programming and logic arise
naturally as subcategories of concurrent games, including stable domain
theory; nondeterministic dataflow; geometry of interaction; dialectica
interpretation; lenses and optics; their extensions to containers in dependent
lenses and optics.

$\bullet$ to transfer enrichments of strategies (e.g. to probabilistic,
quantum or real-number computation) to functional cases.

event structures, stable families, games, concurrent strategies, domain
theory, stable functions, nondeterministic dataflow, dialectica categories,
containers, geometry of interaction, lenses, dependent lenses, optics,
dependent optics, combs, functional programming.

††copyright: none††journalyear: ††doi:

##  1\. Introduction

The view of computation as functions is at the foundation of computer science:
the Church-Turing thesis expresses the coincidence of different notions of
computable function; programming with higher-order functions is now taken for
granted. In contrast the view of computation as interaction is more recent and
less settled, and often obscured by adherence to one syntax or another,
perhaps each with its own mechanism of interaction. Whereas the basic
mechanism of interaction of functions is clear—ultimately by function
composition—a functional approach can struggle with quite the right way to
approach computation which isn’t simply from input to output. The literature
includes approaches via lenses, optics, combs, containers, dependent lenses,
dependent optics, open games and learners (Oles, 1982; Foster et al., 2007;
Pickering et al., 2017; Chiribella et al., 2008; Abbott et al., 2005; Ghani et
al., 2018; Fong et al., 2019). The difficulty is compounded by enrichments to,
say, probabilistic, quantum or real-number computation.

Undeniably there are many ingenious successes, especially through
modifications of functions and their types. But fundamentally the functional
view of computation originates in another computing era, unlike that today
where interaction, unwanted or designed, is often the rule rather than the
exception. By adopting a model which addresses interaction from the outset we
can hope to understand and explore better the space of possibilities in
computation, functional or otherwise. Our model is that of
distributed/concurrent games and strategies: games represent types or
constraints while strategies represent programs or computational processes,
with interaction via the composition of strategies (Rideau and Winskel, 2011).
Through it we can show how many functional paradigms arise automatically by
specialising games. This gives one reading of the title. But reasoning about
interaction is technically challenging. So there’s another reading too: that
of taming concurrent computation, making it practicable by providing
functional abstractions where possible.

After the basics on event structures, the tools of stable families, and
concurrent strategies, the new contribution comes in two parts which can
roughly be described as: how to describe strategies by functions; and how to
describe functions by strategies. The first, rather technical part, Section 5,
introduces a powerful method for lifting a very broad class of functions to
strategies, turning functional into causal dependency. It makes essential use
of stable families and the Scott order intrinsic to a concurrent game. The
second part, Section 6, concerns how causal dependency determines functional
dependency, and shows how many paradigms discovered in making functions
interactive arise as subcategories of concurrent games.

##  2\. Event structures

An event structure (Winskel, 1986) comprises $(E,\leq,{\rm Con})$, consisting
of a set $E$ of events which are partially ordered by $\leq$, the causal
dependency relation, and a nonempty consistency relation ${\rm Con}$
consisting of finite subsets of $E$. The relation $e^{\prime}\leq e$ expresses
that event $e$ causally depends on the previous occurrence of event
$e^{\prime}$; the consistency relation, those events which may occur together.
We insist that the partial order is finitary, i.e.

  * •

$[e]\coloneqq{\\{e^{\prime}\ |\ e^{\prime}\leq e\\}}\hbox{ is finite for all
}e\in E$ ,

and that consistency satisfies

  * •

${\\{e\\}}\in{\rm Con}\hbox{ for all }e\in E$ ,

  * •

$Y\subseteq X\in{\rm Con}\hbox{ implies }Y\in{\rm Con},\ \hbox{ and}$

  * •

$X\in{\rm Con}\ \&\ e\leq e^{\prime}\in X\hbox{ implies }X\cup{\\{e\\}}\in{\rm
Con}$ .

There is an accompanying notion of state or history. A configuration is a,
possibly infinite, subset $x\subseteq E$ which is:

  * •

consistent, $X\subseteq x\ \&\ X\hbox{ is finite}\hbox{ implies }X\in{\rm
Con}$ ; and

  * •

down-closed,  $e^{\prime}\leq e\in x\hbox{ implies }e^{\prime}\in x$ .

Two events $e,e^{\prime}$ are called concurrent if the set
${\\{e,e^{\prime}\\}}$ is in ${\rm Con}$ and neither event is causally
dependent on the other; then we write $e\mathbin{{\it co}}e^{\prime}$. In
games the relation of immediate dependency $e\rightarrowtriangle e^{\prime}$,
meaning $e$ and $e^{\prime}$ are distinct with $e\leq e^{\prime}$ and no event
in between, plays a very important role. We write $[X]$ for the down-closure
of a subset of events $X$. Write $\>\\!{\mathscr{C}}(E)$ for the
configurations of $E$ and $\>\\!{\mathscr{C}}(E)^{o}$ for its finite
configurations. (Sometimes we shall need to distinguish the precise event
structure to which a relation is associated and write, for instance,
$\leq_{E}$, $\rightarrowtriangle_{E}$ or $\mathbin{{\it co}}_{E}$.)

Let $E$ and $E^{\prime}$ be event structures. A map of event structures
$f:E\to E^{\prime}$ is a partial function on events $f:E\rightharpoonup
E^{\prime}$ such that for all $x\in\>\\!{\mathscr{C}}(E)$ its direct image
$fx\in\>\\!{\mathscr{C}}(E^{\prime})$ and

$\hbox{if }e,e^{\prime}\in x\hbox{ and }f(e)=f(e^{\prime})\hbox{ (with both
defined)},\hbox{ then }e=e^{\prime}\,.$

Maps of event structures compose as partial functions. Notice that for a total
map $f$, i.e. when the function $f$ is total, the condition on maps says it is
locally injective, in the sense that w.r.t. any configuration $x$ of the
domain the restriction of $f$ to a function from $x$ is injective; the
restriction of total $f$ to a function from $x$ to $fx$ is thus bijective.

Although a map $f:E\to E^{\prime}$ of event structures does not generally
preserve causal dependency, it does reflect causal dependency locally:
whenever $e,e^{\prime}\in x$, a configuration of $E$, and $f(e)$ and
$f(e^{\prime})$ are both defined with $f(e^{\prime})\leq f(e)$, then
$e^{\prime}\leq e$. Consequently, $f$ preserves the concurrency relation: if
$e\mathbin{{\it co}}e^{\prime}$ in $E$ then $f(e)\mathbin{{\it
co}}f(e^{\prime})$, when defined.

A total map of event structures is rigid when it preserves causal dependency.
Rigid maps induce discrete fibrations:

###### Proposition 2.1.

A total map $f:E\to E^{\prime}$ of event structures is rigid iff for all
$x\in{\mathscr{C}}(E)$ and $y\in{\mathscr{C}}(E^{\prime})$,

$y\subseteq fx\implies\exists z\in{\mathscr{C}}(E).\ z\subseteq x\hbox{ and
}fz=y\ .$

The configuration $z$ is necessarily unique by local injectivity.

##  3\. Stable families

In a “prime” event structure, defined above, an event $e$ has a unique causal
history, the prime configuration $[e]$. Constructions directly on such event
structures can be unwieldy, as often an event is more immediately associated
with several mutually inconsistent causal histories. In this case the broader
model of stable families is apt, especially so, as any stable family yields an
event structure (Winskel, 1982, 1986).

A subset $X$ of a family of sets ${\mathscr{F}}$ is compatible if there is an
element of ${\mathscr{F}}$ which includes all elements of $X$; we say $X$ is
finitely compatible if every finite subset of $X$ is compatible.
A stable family is a non-empty family of sets ${\mathscr{F}}$ which is
$\bullet$ Complete: $\forall Z\subseteq{\mathscr{F}}.\ \hbox{if }Z\hbox{ is
finitely compatible, }\bigcup Z\in{\mathscr{F}}$ ;
$\bullet$ Stable: $\forall Z\subseteq{\mathscr{F}}.\ Z\not=\emptyset\ \&\
Z\hbox{ is compatible }\implies\bigcap Z\in{\mathscr{F}}$;
$\bullet$ Finitary: $\forall x\in{\mathscr{F}},e\in x\exists
x_{0}\in{\mathscr{F}}.\ x_{0}\hbox{ is finite }\ \&\ e\in x_{0}\subseteq x$;
$\bullet$ Coincidence-free: For all $x\in{\mathscr{F}}$, $e,e^{\prime}\in x$
with $e\not=e^{\prime}$,

$\exists x_{0}\in{\mathscr{F}}.\ x_{0}\subseteq x\ \&\ (e\in x_{0}\iff
e^{\prime}\notin x_{0})\,.$

We call elements of ${\mathscr{F}}$ its configurations, $\bigcup{\mathscr{F}}$
its events and write ${\mathscr{F}}^{o}$ for its finite configurations.

A map $f:{\mathscr{F}}\to{\mathscr{G}}$ between stable families
${\mathscr{F}}$ and ${\mathscr{G}}$ is a partial function $f$ from the events
of ${\mathscr{F}}$ to those of ${\mathscr{G}}$ such that for all
$x\in{\mathscr{F}}$ its direct image $fx\in{\mathscr{G}}$ and if
$e,e^{\prime}\in x$ and $f(e)=f(e^{\prime})$ then $e=e^{\prime}$. The choice
of map ensures an inclusion functor from the category of event structures to
that of stable families. The inclusion functor has a right adjoint $\Pr$
giving a coreflection (an adjunction with unit an isomorphism). The
construction $\Pr({\mathscr{F}})$ essentially replaces the original events of
a stable family ${\mathscr{F}}$ by the minimal, prime configurations at which
they occur. Let $x$ be a configuration of a stable family ${\mathscr{F}}$.
Define the prime configuration of $e$ in $x$ by

$[e]_{x}\coloneqq\hbox{$\bigcap$}{\\{y\in{\mathscr{F}}\ |\ e\in y\ \&\
y\subseteq x\\}}\ .$

By coincidence-freeness, the function $\it
top:\>\\!{\mathscr{C}}(\Pr({{\mathscr{F}}}))\to{\mathscr{F}}$ which takes a
prime configuration $[e]_{x}$ to $e$ is well-defined; it is the counit of the
adjunction (Winskel, 1982, 1986).

###### Proposition 3.1.

Let ${\mathscr{F}}$ be a stable family. Then,
$\Pr({\mathscr{F}})\coloneqq(P,{\rm Con},\leq)$ is an event structure where

$\displaystyle{{}P={\\{[e]_{x}\ |\ e\in x\ \&\ x\in{\mathscr{F}}\\}}\ ,}$
---
$\displaystyle{{}Z\in{\rm Con}\hbox{ iff }Z\subseteq P\ \&\
\hbox{$\bigcup$}Z\in{\mathscr{F}}\ \hbox{ and},}$
$\displaystyle{{}p\leq p^{\prime}\hbox{ iff }p,p^{\prime}\in P\ \&\ p\subseteq
p^{\prime}\,.}$

There is an order isomorphism
$\theta:(\>\\!{\mathscr{C}}(\Pr({\mathscr{F}})),\subseteq)\cong({\mathscr{F}},\subseteq)$
where $\theta(y)\coloneqq\it top\,y=\bigcup y$ for
$y\in\>\\!{\mathscr{C}}(\Pr({{\mathscr{F}}}))$; its mutual inverse is
$\varphi$ where $\varphi(x)={\\{[e]_{x}\ |\ e\in x\\}}$ for
$x\in{\mathscr{F}}$.

The partial orders represented by configurations under inclusion are the same
whether for event structures or stable families. They are Gérard Berry’s dI-
domains (Berry, 1978; Winskel, 1982, 1986).

###  3.1. Hiding—the defined part of a map

Let $(E,\leq,{\rm Con})$ be an event structure. Let $V\subseteq E$ be a subset
of ‘visible’ events. Define the projection on $V$, by
$E{\mathbin{\downarrow}}V\coloneqq(V,\leq_{V},{\rm Con}_{V})$, where
$v\leq_{V}v^{\prime}\hbox{ iff }v\leq v^{\prime}\ \&\ v,v^{\prime}\in V$ and
$X\in{\rm Con}_{V}\hbox{ iff }X\in{\rm Con}\ \&\ X\subseteq V$. The operation
hides all events outside $V$. It is associated with a partial-total
factorization system. Consider a partial map of event structures
$f:E\rightharpoonup E^{\prime}$. Let

$V\coloneqq{\\{e\in E\ |\ f(e)\hbox{ is defined}\\}}\,.$

Then $f$ clearly factors into the composition

$\textstyle{E\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{f_{0}}$$\textstyle{E{\mathbin{\downarrow}}V\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{f_{1}}$$\textstyle{E^{\prime}}$

of $f_{0}$, a partial map of event structures taking $e\in E$ to itself if
$e\in V$ and undefined otherwise, and $f_{1}$, a total map of event structures
acting like $f$ on $V$. Note that any
$x\in\>\\!{\mathscr{C}}(E{\mathbin{\downarrow}}V)$ is the image under $f_{0}$
of a minimum configuration, viz. $[x]_{E}\in\>\\!{\mathscr{C}}(E)$. We call
$f_{0}$ a projection and $f_{1}$ the defined part of the map $f$.

###  3.2. Pullbacks

The coreflection from event structures to stable families is a considerable
aid in constructing limits in the former from limits in the latter. The
pullback of total maps of event structures is essential in composing
strategies. We can define it via the pullback of stable families, obtained as
a stable family of secured bijections. Let $\sigma:S\to B$ and $\tau:T\to B$
be total maps of event structures. There is a composite bijection

$\theta:x\cong\sigma x=\tau y\cong y\,,$

between $x\in\>\\!{\mathscr{C}}(S)$ and $y\in\>\\!{\mathscr{C}}(T)$ such that
$\sigma x=\tau y$; because $\sigma$ and $\tau$ are total they induce
bijections between configurations and their image. The bijection is secured
when the transitive relation generated on $\theta$ by
$(s,t)\leq(s^{\prime},t^{\prime})$ if $s\leq_{S}s^{\prime}$ or
$t\leq_{T}t^{\prime}$ is a finitary partial order.

###### Theorem 3.2.

Let $\sigma:S\to B$, $\tau:T\to B$ be total maps of event structures. The
family $\mathscr{R}$ of secured bijections between
$x\in\>\\!{\mathscr{C}}(S)^{o}$ and $y\in\>\\!{\mathscr{C}}(T)^{o}$ such that
$\sigma x=\tau y$ is a stable family. The functions
$\pi_{1}:\Pr({\mathscr{R}})\to S$, $\pi_{2}:\Pr({\mathscr{R}})\to T$, taking a
secured bijection with top to, respectively, the left and right components of
its top, are maps of event structures. $\Pr({\mathscr{R}})$ with $\pi_{1}$,
$\pi_{2}$ is the pullback of $\sigma$, $\tau$ in the category of event
structures.

W.r.t. $\sigma:S\to B$ and $\tau:T\to B$, define $x\wedge y$ to be the
configuration of their pullback which corresponds via this isomorphism to a
secured bijection between $x\in\>\\!{\mathscr{C}}(S)$ and
$y\in\>\\!{\mathscr{C}}(T)$, necessarily with $\sigma x=\tau y$; any
configuration of the pullback takes the form $x\wedge y$ for unique $x$ and
$y$.

##  4\. Concurrent games and strategies

The driving idea is to replace the traditional role of game trees by that of
event structures. Both games and strategies will be represented by event
structures with polarity, which comprise $(A,{\it pol}_{A})$ where $A$ is an
event structure and a polarity function ${\it pol}_{A}:A\to\\{+,-,0\\}$
ascribing a polarity + (Player) or $-$ (Opponent) or 0 (neutral) to its
events. The events correspond to (occurrences of) moves. It will be
technically useful to allow events of neutral polarity; they arise, for
example, in a play between a strategy and a counterstrategy. Maps are those of
event structures which preserve polarity. A game is represented by an event
structure with polarities restricted to + or $-$, with no neutral events.

###### Definition 4.1.

In an event structure with polarity, with configurations $x$ and $y$, write
$x\subseteq^{-}y$ to mean inclusion in which all the intervening events are
Opponent moves. Write $x\subseteq^{+}y$ for inclusion in which the intervening
events are neutral or Player moves. For a subset of events $X$ we write
$X^{+}$ and $X^{-}$ for its restriction to Player and Opponent moves,
respectively. The Scott order will play a central role: between
$x,y\in\>\\!{\mathscr{C}}(A)$, where $A$ is a game, it is characterised by
$y\sqsubseteq_{A}x\iff y^{-}\supseteq x^{-}\ \&\ y^{+}\subseteq x^{+}\,.$

There are two fundamentally important operations on games. One is that of
forming the dual game. On a game $A$ this amounts to reversing the polarities
of events to produce the dual $A^{\perp}$. The other operation, a simple
parallel composition $A{\mathbin{\parallel}}B$, is achieved on games $A$ and
$B$ by simply juxtaposing them, ensuring a finite subset of events is
consistent if its overlaps with the two games are individually consistent; any
configuration $x$ of $A{\mathbin{\parallel}}B$ decomposes into
$x_{A}{\mathbin{\parallel}}x_{B}$ where $x_{A}$ and $x_{B}$ are configurations
of $A$ and $B$ respectively.

A strategy in a game $A$ is a total map $\sigma:S\to A$ of event structures
with polarity such that

(i) if $\sigma x\subseteq^{-}y$, where $x\in\>\\!{\mathscr{C}}(S)$ and
$y\in\>\\!{\mathscr{C}}(A)$, there is a unique
$x^{\prime}\in\>\\!{\mathscr{C}}(S)$ with $x\subseteq x^{\prime}$ and $\sigma
x^{\prime}=y$;

(ii) if $s\rightarrowtriangle_{S}s^{\prime}$ & (${\it pol}(s)=+$ or ${\it
pol}(s^{\prime})=-$ ) , $\sigma(s)\rightarrowtriangle_{A}\sigma(s^{\prime})$.

The conditions prevent Player from constraining Opponent’s behaviour beyond
the constraints of the game. Condition (i) is receptivity, ensuring that the
strategy is open to all moves of Opponent permitted by the game. Condition
(ii), called innocence in (Faggian and Piccolo, 2009), ensures that the only
additional immediate causal dependencies a strategy can enforce beyond those
of the game are those in which a Player move awaits moves of Opponent. A map
$f:\sigma\Rightarrow\sigma^{\prime}$ of strategies $\sigma:S\to A$ and
$\sigma^{\prime}:S^{\prime}\to A$ is a map $f:S\to S^{\prime}$ such that
$\sigma=\sigma^{\prime}f$; this determines when strategies are isomorphic.

Following (Conway, 2000; Joyal, 1997), a strategy from a game $A$ to a game
$B$ is a strategy in the game $A^{\perp}{\mathbin{\parallel}}B$. The
conditions of receptivity and innocence precisely ensure that the copycat
strategy behaves as identity w.r.t. composition, presented below (Rideau and
Winskel, 2011).

###  4.1. Copycat

Let $A$ be a game. The copycat strategy $\ c\\!c\,_{A}:{\rm C\\!\\!C}_{A}\to
A^{\perp}{\mathbin{\parallel}}A$ is an instance of a strategy from $A$ to $A$.
The event structure ${\rm C\\!\\!C}_{A}$ is based on the idea that Player
moves in one component of the game $A^{\perp}{\mathbin{\parallel}}A$ always
copy corresponding moves of Opponent in the other component. For $c\in
A^{\perp}{\mathbin{\parallel}}A$ we use $\bar{c}$ to mean the corresponding
copy of $c$, of opposite polarity, in the alternative component. The event
structure ${\rm C\\!\\!C}_{A}$ comprises $A^{\perp}{\mathbin{\parallel}}A$
with extra causal dependencies $\bar{c}\leq c$ for all events $c$ with ${\it
pol}_{A^{\perp}{\mathbin{\parallel}}A}(c)=+$; with the original causal
dependency they generate a partial order; a finite subset is consistent in
${\rm C\\!\\!C}_{A}$ iff its down-closure w.r.t. $\leq$ is consistent in
$A^{\perp}{\mathbin{\parallel}}A$. The map $\ c\\!c\,_{A}$ acts as the
identity function. In characterising the configurations of ${\rm
C\\!\\!C}_{A}$ we recall the Scott order of Defn 4.1.

###### Lemma 4.2.

Let $A$ be a game. Let $x\in\>\\!{\mathscr{C}}(A^{\perp})$ and
$y\in\>\\!{\mathscr{C}}(A)$,
$x{\mathbin{\parallel}}y\in\>\\!{\mathscr{C}}({\rm C\\!\\!C}_{A})\ \hbox{ iff
}\ y\sqsubseteq_{A}x\,.$

###  4.2. Composition

Two strategies $\sigma:S\to A^{\perp}{\mathbin{\parallel}}B$ and $\tau:T\to
B^{\perp}{\mathbin{\parallel}}C$ compose via pullback and hiding, summarised
below.

---
$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces T\oast
S\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\pi_{1}}$$\scriptstyle{\tau\oast\sigma}$$\scriptstyle{\pi_{2}}$$\textstyle{T{{\odot}}S\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\tau{{\odot}}\sigma}$$\textstyle{S{\mathbin{\parallel}}C\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\sigma{\mathbin{\parallel}}C}$$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces
A{\mathbin{\parallel}}T}$$\scriptstyle{A{\mathbin{\parallel}}\tau}$$\textstyle{A{\mathbin{\parallel}}B{\mathbin{\parallel}}C\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{A{\mathbin{\parallel}}C}$

Ignoring polarities, by forming the pullback of $\sigma{\mathbin{\parallel}}C$
and $A{\mathbin{\parallel}}\tau$ we obtain the synchronisation of
complementary moves of $S$ and $T$ over the common game $B$; subject to the
causal constraints of $S$ and $T$, the effect is to instantiate the Opponent
moves of $T$ in $B^{\perp}$ by the corresponding Player moves of $S$ in $B$,
and vice versa. Reinstating polarities we obtain the interaction of $\sigma$
and $\tau$

$\tau\oast\sigma:T\oast S\to
A^{\perp}{\mathbin{\parallel}}B^{0}{\mathbin{\parallel}}C\,,$

where we assign neutral polarities to all moves in or over $B$. Neutral moves
over the common part $B^{0}$ remain unhidden. The map
$A^{\perp}{\mathbin{\parallel}}B^{0}{\mathbin{\parallel}}C\rightharpoonup
A^{\perp}{\mathbin{\parallel}}C$ is undefined on $B^{0}$ and otherwise mimics
the identity. Pre-composing this map with $\tau\oast\sigma$ we obtain a
partial map $T\oast S\rightharpoonup A^{\perp}{\mathbin{\parallel}}C$; it is
undefined on precisely the neutral events of $T\oast S$. The defined parts of
its partial-total factorization yields

$\tau{{\odot}}\sigma:T{{\odot}}S\to A^{\perp}{\mathbin{\parallel}}C\,;$

this is the composition of $\sigma$ and $\tau$.

For $x\in\>\\!{\mathscr{C}}(S)$ and $y\in\>\\!{\mathscr{C}}(T)$, let $\sigma
x=x_{A}{\mathbin{\parallel}}x_{B}$ and $\tau
y=y_{B}{\mathbin{\parallel}}y_{C}$ where $x_{A}\in\>\\!{\mathscr{C}}(A)$,
$x_{B},y_{B}\in\>\\!{\mathscr{C}}(B)$, $y_{C}\in\>\\!{\mathscr{C}}(C)$. Define
$y\oast x=(x{\mathbin{\parallel}}y_{C})\wedge(x_{A}{\mathbin{\parallel}}y)$.
This is a partial operation only defined if the $\wedge$-expression is. It
glues configurations $x$ and $y$ together at their common overlap over $B$, if
$x_{B}=y_{B}$ and a finitary partial order of causal dependency results. Any
configuration of $T\oast S$ has the form $y\oast x$, for unique
$x\in\>\\!{\mathscr{C}}(S),y\in\>\\!{\mathscr{C}}(T)$.

###  4.3. A bicategory of strategies

We obtain a bicategory ${\mathbf{Strat}}$ for which the objects are games, the
arrows $\sigma:A\\!\\!\\!\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
3.0pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
9.4444pt\raise 0.0pt\hbox{\hbox{\kern
0.0pt\raise-1.75pt\hbox{$\scriptstyle{\\!+\\!}$}}}}}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
18.0pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
18.0pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{}$}}}}}}}\ignorespaces}}}}\ignorespaces\\!\\!\\!B$ are
strategies $\sigma:S\to A^{\perp}{\mathbin{\parallel}}B$; with 2-cells
$f:\sigma\Rightarrow\sigma^{\prime}$ maps of strategies. The vertical
composition of 2-cells is the usual composition of maps. Horizontal
composition is the composition of strategies ${{\odot}}$ (which extends to a
functor via the universality of pullback and partial-total factorisation). We
can restrict the 2-cells to be rigid maps and still obtain a bicategory. The
bicategory of strategies is compact-closed, though with the addition of
winning conditions—Section 4.4—this weakens to $*$-autonomous.

A strategy $\sigma:S\to A$ is deterministic if $S$ is deterministic, viz.

$\forall X\subseteq_{\rm fin}S.\ [X]^{-}\in{\rm Con}_{S}\implies X\in{\rm
Con}_{S}\,,$

where $[X]^{-}\coloneqq{\\{s^{\prime}\in S\ |\ \exists s\in X.\ {\it
pol}_{S}(s^{\prime})=-\ \&\ s^{\prime}\leq s\\}}$. So, a strategy is
deterministic if consistent behaviour of Opponent is answered by consistent
behaviour of Player. Copycat $\ c\\!c\,_{A}$ is deterministic iff the game $A$
is race-free, i.e. if $x\subseteq^{-}y$ and $x\subseteq^{+}z$ in
$\>\\!{\mathscr{C}}(A)$ then $y\cup z\in\>\\!{\mathscr{C}}(A)$. The bicategory
of strategies restricts to a bicategory of deterministic strategies between
race-free games.

There are several ways to reformulate strategies. Deterministic strategies
coincide with the receptive ingenuous strategies of Melliès and Mimram based
on asynchronous transition systems (Melliès and Mimram, 2007; Winskel, 2012a).
Via the Scott order, we can see strategies as a refinement of profunctors: a
strategy in a game $A$ induces a discrete fibration, so presheaf, on
$(\>\\!{\mathscr{C}}(A)^{o},\sqsubseteq_{A})$, a construction which extends to
strategies between games (Winskel, 2013b).

###  4.4. Winning conditions

Winning conditions of a game $A$ specify a subset of its configurations $W$,
an outcome in which is a win for Player. Informally, a strategy (for Player)
is winning if it always prescribes moves for Player to end up in a winning
configuration, no matter what the activity or inactivity of Opponent.

Formally, a game with winning conditions $(A,W_{A})$ comprises a concurrent
game $A$ with winning conditions $W_{A}\subseteq\>\\!{\mathscr{C}}(A)$. A
strategy $\sigma:S\to A$ is winning if $\sigma x$ is in $W_{A}$ for all
+-maximal configurations $x$ of $S$; in general, a configuration is +-maximal
if no additional Player, or neutral, moves can occur from it. That $\sigma$ is
winning can be shown equivalent to: all plays of $\sigma$ against any
counterstrategy of Opponent result in a win for Player (Clairambault et al.,
2012; Winskel, 2016).

As the dual of a game with winning conditions $(A,W_{A})$ we again reverse the
roles of Player and Opponent, and take its winning conditions to be the set-
complement of $W_{A}$, i.e.
$(A,W_{A})^{\perp}=(A^{\perp},\>\\!{\mathscr{C}}(A)\setminus W_{A})$.

In a parallel composition of games with winning conditions, we deem a
configuration winning if its component in either game is winning:
$(A,W_{A}){\mathbin{\parallel}}(B,W_{B})\coloneqq(A{\mathbin{\parallel}}B,W)$
where $W={\\{x\in\>\\!{\mathscr{C}}(A{\mathbin{\parallel}}B)\ |\ x_{A}\in
W_{A}\hbox{ or }x_{B}\in W_{B}\\}}$.

With these extensions, we take a winning strategy from a game $(A,W_{A})$ to a
game $(B,W_{B})$, to be a winning strategy in the game
$A^{\perp}{\mathbin{\parallel}}B$. When games are race-free, copycat will be a
winning strategy. The composition of winning strategies is winning
(Clairambault et al., 2012; Winskel, 2016). In the proof the following lemma
is critical:

###### Lemma 4.3.

For strategies $\sigma:S\to A^{\perp}{\mathbin{\parallel}}B$, $\tau:T\to
B^{\perp}{\mathbin{\parallel}}C$, $y\oast x\in\>\\!{\mathscr{C}}(T\oast S)$ is
+-maximal iff $x$ and $y$ are +-maximal.

One can extend winning conditions to payoff functions (Clairambault and
Winskel, 2013) or to allow draws, where neither player wins (Winskel, 2012b).

###  4.5. Imperfect information

In a game of imperfect information some moves are masked, or inaccessible, and
strategies with dependencies on unseen moves are ruled out. One can extend
games with imperfect information in a way that respects the operations of
concurrent games and strategies (Winskel, 2012b). Each move of a game is
assigned a level in a global order of access levels; moves of the game or its
strategies can only causally depend on moves at equal or lower levels.

In more detail, a fixed preorder of access levels $(\Lambda,\preceq)$ is pre-
supposed. A $\Lambda$-game, comprises a game $A$ with a level function
$l:A\to\Lambda$ such that if $a\leq_{A}a^{\prime}$ then $l(a)\preceq
l(a^{\prime})$ for all moves $a,a^{\prime}$ in $A$. A $\Lambda$-strategy in
the $\Lambda$-game is a strategy $\sigma:S\to A$ for which if
$s\leq_{S}s^{\prime}$ then $l\sigma(s)\preceq l\sigma(s^{\prime})$ for all
$s,s^{\prime}$ in $S$. The access levels of moves in a game are left
undisturbed in forming the dual and parallel composition of $\Lambda$-games.
As before a $\Lambda$-strategy from a $\Lambda$-game $A$ to a $\Lambda$-game
$B$ is a $\Lambda$-strategy in the game $A^{\perp}{\mathbin{\parallel}}B$. It
can be shown that $\Lambda$-strategies compose (Winskel, 2012b).

###  4.6. A language for strategies

We recall briefly the language for strategies introduced in (Castellan et al.,
2014b). Games $A,B,C,\cdots$ play the role of types. Operations on games
include forming the dual $A^{\perp}$, simple parallel composition
$A{\mathbin{\parallel}}B$, a sum $\Sigma_{i\in I}A_{i}$ as well as
recursively-defined games.

Terms, denoting strategies, have typing judgements

$x_{1}:A_{1},\cdots,x_{m}:A_{m}\vdash\ t\ \dashv
y_{1}:B_{1},\cdots,y_{n}:B_{n}\ ,$

where all the variables are distinct, interpreted as a strategy from
$\vec{A}=A_{1}{\mathbin{\parallel}}\cdots{\mathbin{\parallel}}A_{m}$ to
$\vec{B}=B_{1}{\mathbin{\parallel}}\cdots{\mathbin{\parallel}}B_{n}$. We can
think of the term $t$ as a box with input and output wires for the variables
$\vec{x}$ and $\vec{y}$.

The term $t$ denotes a strategy
$\sigma:S\to\vec{A}^{\perp}{\mathbin{\parallel}}\vec{B}$. It does so by
describing witnesses, configurations of $S$, to a relation between
configurations $\vec{x}$ of $\vec{A}$ and $\vec{y}$ of $\vec{B}$. For example,
the term
$x:A\vdash y\sqsubseteq_{A}x\dashv y:A$
denotes the copycat strategy on a game $A$; it describes configurations of
copycat, ${\rm C\\!\\!C}_{A}$, as witnesses, viz. those configurations
$x{\mathbin{\parallel}}y$ of ${\rm C\\!\\!C}_{A}$ for which
$y\sqsubseteq_{A}x$ in the Scott order. There are other operations, such as
sum $\mathop{[\\!]}$ and pullback $\wedge$ on strategies of the same type.

Duality is caught by the rules

${{\hbox{{$\Gamma,x:A\vdash t\dashv\Delta$}}\over{\hbox{{$\Gamma\vdash t\dashv
x:{A}^{\perp},\Delta$}}}}}\qquad{{\hbox{{$\Gamma\vdash t\dashv
x:A,\Delta$}}\over{\hbox{{$\Gamma,x:{A}^{\perp}\vdash t\dashv\Delta$}}}}}$

and composition of strategies by

${{\hbox{{${\Gamma\vdash t\dashv\Delta\qquad\Delta\vdash u\dashv{\rm
H}}$}}\over{\hbox{{$\Gamma\vdash\exists\Delta.\,[\,t\mathrel{{\mathbin{\parallel}}}u\,]\dashv{\rm
H}$}}}}}$

which, in the picture of strategies as boxes, joins the output wires of one
strategy to input wires of the other. Simple parallel composition of
strategies arises when $\Delta$ is empty.

##  5\. From functions to strategies

The language for strategies in (Castellan et al., 2014b) included a judgement

$x:A\vdash g(y)\sqsubseteq_{C}f(x)\dashv y:B$

for building strategies out of expressions $f(x)$ and $g(y)$ denoting “affine
functions.” It breaks down into a composition

$x:A\vdash\exists
z:C.\,[\,g(y)\sqsubseteq_{C}z\mathrel{{\mathbin{\parallel}}}z\sqsubseteq_{C}f(x)\,]\dashv
y:B\,.$

Here we present a considerably broader class of affine-stable functions $f$
and “co-affine-stable” functions $g$ with which to define strategies in this
manner. It hinges on the Scott order to convert functional dependency to
causal dependency.

###  5.1. Affine-stable maps and their strategies

###### Definition 5.1.

An affine-stable map between games from $A$ to $B$, is a function
$f:\>\\!{\mathscr{C}}(A)\to\>\\!{\mathscr{C}}(B)$ which is
$\bullet$ polarity-respecting: for $x,y\in\>\\!{\mathscr{C}}(A)$,

$x\subseteq^{-}y\Rightarrow f(x)\subseteq^{-}f(y)\ \hbox{ and }\
x\subseteq^{+}y\Rightarrow f(x)\subseteq^{+}f(y)\,;$

$\bullet$ +-continuous: for $x\in\>\\!{\mathscr{C}}(A)$,

$b\in f(x)\ \&\ {\it pol}_{B}(b)=+\Rightarrow\exists
x_{0}\in\>\\!{\mathscr{C}}(A)^{o}.\ x_{0}\subseteq x\ \&\ b\in f(x_{0})\,;$

$\bullet$ $-$-image finite: for all finite configurations
$x\in\>\\!{\mathscr{C}}(A)^{o}$ the set $f(x)^{-}$ is finite;
$\bullet$ affine: for all compatible families ${\\{x_{i}\ |\ i\in I\\}}$ in
$\>\\!{\mathscr{C}}(A)$,

$\hbox{$\bigcup$}_{i\in I}f(x_{i})\subseteq^{+}f(\hbox{$\bigcup$}_{i\in
I}x_{i})\,$

—when $I$ is empty this amounts to $\emptyset\subseteq^{+}f(\emptyset)$; and
$\bullet$ stable: for all compatible families ${\\{x_{i}\ |\ i\in
I\\}}\neq\emptyset$ in $\>\\!{\mathscr{C}}(A)$,

$f(\hbox{$\bigcap$}_{i\in I}x_{i})\subseteq^{-}\hbox{$\bigcap$}_{i\in
I}f(x_{i})\,.$

When all the moves of games $A$ and $B$ are those of Player, the definition
reduces to that of stable function. If all moves are those of Opponent, it
becomes that of demand maps—see Section 6.2 (Winskel, 2011). Affine-stable
maps include maps of event structures with polarity, including partial maps
between games, and the affine maps of (Castellan et al., 2014b). They are the
most general maps out of which we can construct a strategy as follows:

###### Theorem 5.2.

Let $f:\>\\!{\mathscr{C}}(A)\to\>\\!{\mathscr{C}}(B)$ be an affine-stable map
between games $A$ and $B$. Then

${\mathscr{F}}\coloneqq{\\{x{\mathbin{\parallel}}y\in\>\\!{\mathscr{C}}(A^{\perp}{\mathbin{\parallel}}B)\
|\ y\sqsubseteq_{B}f(x)\\}}$

is a stable family. The map $\it top:\Pr({\mathscr{F}})\to
A^{\perp}{\mathbin{\parallel}}B$ is a strategy
$f_{!}:A\\!\\!\\!\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
3.0pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
9.4444pt\raise 0.0pt\hbox{\hbox{\kern
0.0pt\raise-1.75pt\hbox{$\scriptstyle{\\!+\\!}$}}}}}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
18.0pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
18.0pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{}$}}}}}}}\ignorespaces}}}}\ignorespaces\\!\\!\\!B$. The
strategy $f_{!}$ is deterministic if $A$ and $B$ are race-free and $f$
reflects $-$-compatibility, i.e. $x\subseteq^{-}x_{1}$ and
$x\subseteq^{-}x_{2}$ in $\>\\!{\mathscr{C}}(A)$ and $fx_{1}\cup
fx_{2}\in\>\\!{\mathscr{C}}(B)$ implies $x_{1}\cup
x_{2}\in\>\\!{\mathscr{C}}(A)$.

For $f$ an affine-stable map from $A$ to $B$ we can write $f_{!}$ as

$x:A\vdash y\sqsubseteq_{B}f(x)\dashv y:B\,.$

Through suitable $f$ we can create strategies from structural maps, injections
and projections as strategies, for conditional and case statements and,
generally, much of the causal wiring that is often explained informally in
diagrammatic reasoning. If $\sigma$ is a strategy in $A$ then
$f_{!}{{\odot}}\sigma$ is its “pushforward” to a strategy in $B$. Some basic
examples:

###### Example 5.3.

(Projectors) Let $f:A{\mathbin{\parallel}}B\to B$ be the function undefined on
game $A$ but acting as identity on game $B$. Let $\sigma$ be a strategy in the
game $A{\mathbin{\parallel}}B$. The strategy $f_{!}{{\odot}}\sigma$ is its
projection to a strategy in $B$. $\Box$

###### Example 5.4.

(Duplicators) Let $A$ be a game. Consider the function $d_{A}:x\mapsto
x{\mathbin{\parallel}}x$ from $\>\\!{\mathscr{C}}(A)$ to
$\>\\!{\mathscr{C}}(A{\mathbin{\parallel}}A)$. It is easily checked to be
affine-stable. Hence there is a duplicator strategy
$\delta_{A}={d_{A}}_{!}:A\\!\\!\\!\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
3.0pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
9.4444pt\raise 0.0pt\hbox{\hbox{\kern
0.0pt\raise-1.75pt\hbox{$\scriptstyle{\\!+\\!}$}}}}}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
18.0pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
18.0pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{}$}}}}}}}\ignorespaces}}}}\ignorespaces\\!\\!\\!A{\mathbin{\parallel}}A$.
(The strategy $\delta_{A}$ is not natural in $A$ as ${\mathbin{\parallel}}$ is
not a product, except in subcategories.) $\Box$

###### Example 5.5.

(Detectors) Let $A$ be a game. Let $X\in{\rm Con}_{A}$ with $X\subseteq
A^{+}$. Let ${\boxplus}$ be a single “detector” event, of +ve polarity. Let

$d_{X}:\>\\!{\mathscr{C}}(A)\to\>\\!{\mathscr{C}}({\boxplus})$

be the function such that

$d_{X}(x)=\begin{cases}{\boxplus}&\hbox{ if }X\subseteq x\,,\\\
\emptyset&\hbox{ otherwise. }\end{cases}$

The function $d_{X}$ is affine-stable. There is a detector strategy

${d_{X}}_{!}:A\\!\\!\\!\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
3.0pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
9.4444pt\raise 0.0pt\hbox{\hbox{\kern
0.0pt\raise-1.75pt\hbox{$\scriptstyle{\\!+\\!}$}}}}}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
18.0pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
18.0pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{}$}}}}}}}\ignorespaces}}}}\ignorespaces\\!\\!\\!{\boxplus}\,.$

The strategy simply adjoins extra causal dependencies
$a\rightarrowtriangle{\boxplus}$ from $a\in X$. It detects the presence of
$X$. In a similar way, one can extend detectors to detect the occurrence of
one of a family $\langle X_{i}\rangle_{i\in I}$ of $X_{i}\in{\rm Con}_{A}$
provided $X_{i}\cup X_{j}\in{\rm Con}_{A}\implies i=j$ for $i,j\in I$. $\Box$

###### Example 5.6.

(Blockers) Let $A$ be a game and $Y\subseteq A^{-}$. Let

$h_{Y}:\>\\!{\mathscr{C}}(A)\to\>\\!{\mathscr{C}}({\boxminus})$

be the function which acts so

$h_{Y}(x)=\begin{cases}{\boxminus}&\hbox{ if }x\cap Y\neq\emptyset\,,\\\
\emptyset&\hbox{ otherwise.}\end{cases}$

$h_{Y}$ is a map of event structures so affine-stable. The blocker strategy
${h_{Y}}_{!}$ adjoins causal dependencies ${\boxminus}\rightarrowtriangle a$
from ${\boxminus}$ to each $a\in Y$. The absence of move ${\boxminus}$ blocks
all moves $Y$. $\Box$

###### Theorem 5.7.

The operation $(\\_)_{!}$ is a (pseudo) functor from the category of affine-
stable maps to concurrent strategies ${\mathbf{Strat}}$.

###  5.2. co-Affine-stability

We examine the dual, or co-notion, to affine-stability. An affine-stable map
$f$ from $A^{\perp}$ to $B^{\perp}$ yields a strategy
$f_{!}:A^{\perp}\\!\\!\\!\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
3.0pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
9.4444pt\raise 0.0pt\hbox{\hbox{\kern
0.0pt\raise-1.75pt\hbox{$\scriptstyle{\\!+\\!}$}}}}}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
18.0pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
18.0pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{}$}}}}}}}\ignorespaces}}}}\ignorespaces\\!\\!\\!B^{\perp}$,
so by duality a strategy $f^{*}:B\\!\\!\\!\lx@xy@svg{\hbox{\raise
0.0pt\hbox{\kern
3.0pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
9.4444pt\raise 0.0pt\hbox{\hbox{\kern
0.0pt\raise-1.75pt\hbox{$\scriptstyle{\\!+\\!}$}}}}}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
18.0pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
18.0pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{}$}}}}}}}\ignorespaces}}}}\ignorespaces\\!\\!\\!A$. We
obtain the dual to Theorems 5.2,5.7 as a corollary:

###### Corollary 5.8.

Let $g:\>\\!{\mathscr{C}}(A)\to\>\\!{\mathscr{C}}(B)$ be such that
$g:\>\\!{\mathscr{C}}(A^{\perp})\to\>\\!{\mathscr{C}}(B^{\perp})$ is affine-
stable, then

${\mathscr{G}}\coloneqq{\\{y{\mathbin{\parallel}}x\in\>\\!{\mathscr{C}}(B^{\perp}{\mathbin{\parallel}}A)\
|\ g(x)\sqsubseteq_{B}y\\}}$

is a stable family. The map $\it top:\Pr({\mathscr{G}})\to
B^{\perp}{\mathbin{\parallel}}A$ is a strategy
$g^{*}:B\\!\\!\\!\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
3.0pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
9.4444pt\raise 0.0pt\hbox{\hbox{\kern
0.0pt\raise-1.75pt\hbox{$\scriptstyle{\\!+\\!}$}}}}}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
18.0pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
18.0pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{}$}}}}}}}\ignorespaces}}}}\ignorespaces\\!\\!\\!A$. The
strategy $g^{*}$ is deterministic if $A$ is race-free and $g$ reflects
$+$-compatibility. The operation $(\\_)^{*}$ is a contravariant (pseudo)
functor from the category of affine-stable maps to ${\mathbf{Strat}}$.

For $g$ an affine-stable map from $A^{\perp}$ to $B^{\perp}$ we can write
$g^{*}$ as

$y:B\vdash g(y)\sqsubseteq_{B}x\dashv x:A\,.$

For a strategy $\sigma$ in game $B$ the operation $g^{*}{{\odot}}\sigma$
yields the strategy in $A$ got as the pullback of $\sigma$ along $g$. In
particular, if $A$ prefixed game $B$ by some initial move,
$g^{*}{{\odot}}\sigma$ would be a prefix operation on strategies.

###  5.3. An adjunction

An affine-stable map $f$ from $A$ to $B$ is not generally an affine-stable map
from $A^{\perp}$ to $B^{\perp}$. The next definition, of an additive-stable
map $f$ from $A$ to $B$, bluntens affine-stability to ensure $f$ is also a
additive-stable map from $A^{\perp}$ to $B^{\perp}$; and hence is associated
with both a strategy $f_{!}:A\\!\\!\\!\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
3.0pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
9.4444pt\raise 0.0pt\hbox{\hbox{\kern
0.0pt\raise-1.75pt\hbox{$\scriptstyle{\\!+\\!}$}}}}}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
18.0pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
18.0pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{}$}}}}}}}\ignorespaces}}}}\ignorespaces\\!\\!\\!B$ and
a converse strategy $f^{*}:B\\!\\!\\!\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
3.0pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
9.4444pt\raise 0.0pt\hbox{\hbox{\kern
0.0pt\raise-1.75pt\hbox{$\scriptstyle{\\!+\\!}$}}}}}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
18.0pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
18.0pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{}$}}}}}}}\ignorespaces}}}}\ignorespaces\\!\\!\\!A$.
Together they form an adjunction.

###### Definition 5.9.

A additive-stable map between event structures with polarity, from $A$ to $B$,
is a function $f:\>\\!{\mathscr{C}}(A)\to\>\\!{\mathscr{C}}(B)$ which is
$\bullet$ polarity-respecting: for $x,y\in\>\\!{\mathscr{C}}(A)$,

$x\subseteq^{-}y\Rightarrow f(x)\subseteq^{-}f(y)\ \hbox{ and }\
x\subseteq^{+}y\Rightarrow f(x)\subseteq^{+}f(y)\,;$

$\bullet$ image finite: if $x\in\>\\!{\mathscr{C}}(A)^{o}$ then
$f(x)\in\>\\!{\mathscr{C}}(B)^{o}$;
$\bullet$ additive: for all compatible families ${\\{x_{i}\ |\ i\in I\\}}$ in
$\>\\!{\mathscr{C}}(A)$,

$\hbox{$\bigcup$}_{i\in I}f(x_{i})=f(\hbox{$\bigcup$}_{i\in I}x_{i})\,;$

$\bullet$ stable: for all compatible families ${\\{x_{i}\ |\ i\in
I\\}}\neq\emptyset$ in $\>\\!{\mathscr{C}}(A)$,

$f(\hbox{$\bigcap$}_{i\in I}x_{i})=\hbox{$\bigcap$}_{i\in I}f(x_{i})\,.$

The usual maps of games are additive-stable, including those which are
partial, as are Girard’s linear maps. Additive-stability is indifferent to a
switch of polarities:

###### Proposition 5.10.

An additive-stable function $f$ from $A$ to $B$ is an additive-stable function
$f$ from $A^{\perp}$ to $B^{\perp}$ and vice versa.

Given an additive-stable function $f$ from $A$ to $B$ we obtain a strategy
$f_{!}:A\\!\\!\\!\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
3.0pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
9.4444pt\raise 0.0pt\hbox{\hbox{\kern
0.0pt\raise-1.75pt\hbox{$\scriptstyle{\\!+\\!}$}}}}}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
18.0pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
18.0pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{}$}}}}}}}\ignorespaces}}}}\ignorespaces\\!\\!\\!B$ and,
via $f$ from $A^{\perp}$ to $B^{\perp}$,
$f^{*}:B\\!\\!\\!\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
3.0pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
9.4444pt\raise 0.0pt\hbox{\hbox{\kern
0.0pt\raise-1.75pt\hbox{$\scriptstyle{\\!+\\!}$}}}}}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
18.0pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
18.0pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{}$}}}}}}}\ignorespaces}}}}\ignorespaces\\!\\!\\!A$.

###### Theorem 5.11.

Let $f$ be an additive-stable function from $A$ to $B$ between event
structures with polarity. The strategies $f_{!}$ and $f^{*}$ form an
adjunction $f_{!}\dashv f^{*}$ in the bicategory ${\mathbf{Strat}}$.

${\mathbf{Strat}}$ forms a pseudo double category (Johnson and Yau, 2020;
Paquet, 2020). In Section 6.3.1 we apply Theorem 5.11 to relate deterministic
strategies in general, to those of Geometry of Interaction. The adjunction in
${\mathbf{Strat}}$ of Theorem 5.11 yields a traditional adjunction:

###### Corollary 5.12.

Let $f$ be an additive-stable function from game $A$ to game $B$. Let
${\mathbf{Strat}}_{A}$ be the category of strategies in the game $A$, and
${\mathbf{Strat}}_{B}$ that in $B$. Then there are functors
$f_{!}{{\odot}}(\\_):{\mathbf{Strat}}_{A}\to{\mathbf{Strat}}_{B}$ and
$f^{*}{{\odot}}(\\_):{\mathbf{Strat}}_{B}\to{\mathbf{Strat}}_{A}$ with
$f_{!}{{\odot}}(\\_)$ left adjoint to $f^{*}{{\odot}}(\\_)$.

##  6\. From strategies to functions

We recover familiar notions on games from those based on event structures. A
game is tree-like when any two events are either inconsistent or causally
dependent. When race-free, at any finite configuration, the next moves, if
there are any, are either purely those of Player, or purely those of Opponent;
so positions either belong to Player or Opponent. Then, at each Player
position a deterministic strategy either chooses a unique move or to stay put.
In contrast to many presentations of games, in a concurrent strategy Player
isn’t forced to make a move, though that can be encouraged through suitable
winning conditions. A counterstrategy, as a strategy in the dual game, picks
moves for Opponent at their configurations. The interaction $\tau\oast\sigma$
of a deterministic strategy $\sigma$ with a deterministic counterstrategy
$\tau$ determines a finite or infinite branch in the tree of configurations,
which in the presence of winning conditions will be a win for one of the
players.

On tree-like games we recover familiar notions. More surprising is that by
exploiting the richer structure of concurrent games we can recover other
familiar paradigms, not traditionally tied to games, or if so only somewhat
informally. We start by rediscovering Berry’s stable domain theory, of which
Jean-Yves Girard’s qualitative domains and coherence spaces are special cases.
The other examples, from dataflow, logic and functional programming, concern
ways of handling interaction within a functional approach. We shall restrict
to race-free games, so guaranteeing that deterministic strategies have an
identity w.r.t. composition, given by copycat.

###  6.1. Stable functions

Consider games in which all moves are Player moves. Consider a strategy
$\sigma$ from from one such purely Player game $A$ to another $B$. This is a
map $\sigma:S\to A^{\perp}{\mathbin{\parallel}}B$ which is receptive and
innocent. Notice that in $A^{\perp}{\mathbin{\parallel}}B$ all the Opponent
moves are in $A^{\perp}$ and all the Player moves are in $B$. By receptivity
any configuration of $A$ can be input. The only new immediate causal
connections, beyond those in $A^{\perp}$ and $B$, that can be introduced in a
strategy are those from Opponent moves of $A^{\perp}$ to a Player move in $B$.
Beyond the causal dependencies of the games, a strategy $\sigma$ can only make
a Player move in $B$ causally depend on a finite subset of moves in
$A^{\perp}$.

When $\sigma$ is deterministic, all conflicts are inherited from conflicts
between Opponent moves. Then the strategy $\sigma$ gives rise to a stable
function from the configurations of $A$ to the configurations of $B$.
Conversely, such a stable function $f$ yields a deterministic strategy
$f_{!}:A\\!\\!\\!\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
3.0pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
9.4444pt\raise 0.0pt\hbox{\hbox{\kern
0.0pt\raise-1.75pt\hbox{$\scriptstyle{\\!+\\!}$}}}}}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
18.0pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
18.0pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{}$}}}}}}}\ignorespaces}}}}\ignorespaces\\!\\!\\!B$, by
Theorem 5.2.

###### Theorem 6.1.

The category of dI-domains and stable functions, enriched by the stable order,
is equivalent to the bicategory of deterministic strategies between purely
Player games with rigid 2-cells.

The category of dI-domains and stable functions is well-known to be cartesian-
closed; its function space and product are realised by constructions $[A\to
B]$ and $A{\mathbin{\parallel}}B$ on event structures. When the games are
further restricted to have trivial causal dependency we recover Girard’s
qualitative domains and, with conflict determined in a binary fashion, his
coherence spaces. Girard’s models for polymorphism there generalise to dI-
domains, with dependent types $\Pi_{x:A}B(x)$ and $\Sigma_{x:A}B(x)$ on event
structures (Winskel, 1986; Coquand et al., 1987, 1989)—see Appendices A.1,
A.2.

###  6.2. Stable spans

When between games in which all the moves are Player moves, a general,
nondeterministic, strategy corresponds to a stable span, a form of many-valued
stable function which has been discovered, and rediscovered, in giving
semantics to higher-order processes and nondeterministic dataflow (Nygaard,
2003; Winskel, 2011; Saunders-Evans and Winskel, 2007); the trace of
strategies, derived from their compact closure, specialises to the feedback
operation of dataflow. Recall a stable span comprises

$\textstyle{{E}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{{\it
dem}}$$\scriptstyle{{\it out}}$$\textstyle{{A}}$$\textstyle{{B\,,}}$

with event structure $E$ relating input given by an event structure $A$ and
output by an event structure $B$. The map ${\it out}:E\to B$ is a rigid map.
The map ${\it dem}:E\to A$, associated to input, is of a different character.
It is a demand map, i.e., a function from $\>\\!{\mathscr{C}}(E)$ to
$\>\\!{\mathscr{C}}(A)$ which preserves unions and finite configurations;
${\it dem}(x)$ is the minimum input for $x$ to occur and is the union of the
demands of its events. The occurrence of an event $e$ in $E$ demands minimum
input ${\it dem}([e])$ and is observed as the output event ${\it out}(e)$.
Spans from $A$ to $B$ are related by the usual 2-cells, here (necessarily)
rigid maps $r$ making the diagram below commute:

$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces
E^{\prime}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{{\it
dem}^{\prime}}$$\scriptstyle{r}$$\scriptstyle{{\it
out}^{\prime}}$$\textstyle{A}$$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces
E\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{{\it
dem}}$$\scriptstyle{{\it out}}$$\textstyle{B}$

Stable spans compose via the usual pullback construction of spans, as both
demand and output maps extend to functions between configurations. A stable
span $E$ corresponds to a (special) profunctor

$\tilde{E}(x,y)={\\{w\in\>\\!{\mathscr{C}}(E)^{o}\ |\ {\it dem}(w)\subseteq x\
\&\ {\it out}\,w=y\\}}\,,$

between the partial-order categories $\>\\!{\mathscr{C}}(A)^{o}$ and
$\>\\!{\mathscr{C}}(B)^{o}$ —a correspondence that respects composition.
Recalling the view of profunctors as Kleisli maps w.r.t. the presheaf
construction (Fiore et al., 2018), we borrow from Moggi (Moggi, 1989) and
describe the composition of stable spans $F:A\\!\\!\\!\lx@xy@svg{\hbox{\raise
0.0pt\hbox{\kern
3.0pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
9.4444pt\raise 0.0pt\hbox{\hbox{\kern
0.0pt\raise-1.75pt\hbox{$\scriptstyle{\\!+\\!}$}}}}}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
18.0pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
18.0pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{}$}}}}}}}\ignorespaces}}}}\ignorespaces\\!\\!\\!B$,
$G:B\\!\\!\\!\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
3.0pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
9.4444pt\raise 0.0pt\hbox{\hbox{\kern
0.0pt\raise-1.75pt\hbox{$\scriptstyle{\\!+\\!}$}}}}}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
18.0pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
18.0pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{}$}}}}}}}\ignorespaces}}}}\ignorespaces\\!\\!\\!C$ as

$G{{\odot}}F(x)=\hbox{ {\rm let }}y\Leftarrow F(x)\hbox{ {\rm in} }G(y)\,$

—which, via the correspondence with profunctors, stands for the coend
$\int^{y\in\>\\!{\mathscr{C}}(B)^{o}}\tilde{F}(x,y)\times\tilde{G}(y,\\_)$. In
using let-notation we can take account of the shape of the configuration $y$
in the definition of $G$, in effect an informal pattern matching.

Stable spans are monoidal closed (Nygaard, 2003; Nygaard and Winskel, 2002):
w.r.t. an event structure $A$, the functor $(\\_{\mathbin{\parallel}}A)$ has a
right adjoint, the function space $[A\multimap\\_]$. The construction
$[A\multimap B]$ is recalled in Appendix B along with a more general dependent
product $\Pi^{s}_{x:A}B(x)$ for stable spans: the type of stable spans which
on input $x:A$ yield output $y:B(x)$ nondeterministically.

Let $A$ and $B$ be purely Player games. A strategy $\sigma:S\to
A^{\perp}{\mathbin{\parallel}}B$ gives rise to a stable span

$\textstyle{A}$$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces{E}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{{\it
dem}}$$\scriptstyle{{\it out}}$$\textstyle{{B\,,}}$

where $E=S^{+}$, and ${\it out}$ gives the image of its events in $B$ and
${\it dem}$ those events in $A$ on which they casually depend. Conversely
given a stable span, as above, we obtain a strategy as the composition ${\it
out}_{!}{{\odot}}{\it dem}^{*}$, by the results of Section 5; as regarding $E$
and $A$ as purely Player games, both ${\it out}$ and ${\it
dem}:\>\\!{\mathscr{C}}(E^{\perp})\to\>\\!{\mathscr{C}}(A^{\perp})$ are
affine-stable. In the strategy ${\it out}_{!}{{\odot}}{\it dem}^{*}:S\to
A^{\perp}{\mathbin{\parallel}}B$ so obtained, $S$ comprises the disjoint union
of $A$ and $E$ with the additional causal dependencies of $e\in E$ on $a\in
A^{\perp}$ prescribed by ${\it dem}$.

###### Theorem 6.2.

The bicategory of stable spans is equivalent to the bicategory of strategies
between purely Player games with rigid 2-cells.

We show that in a similar way, we obtain geometry of interaction, dialectica
categories, containers, lenses, open games and learners, optics and dependent
optics by moving to slightly more complicated subcategories of games,
sometimes with winning conditions and imperfect information.

###  6.3. Geometry of Interaction

Let’s now consider slightly more complex games. A GoI game comprises a
parallel composition $A:=A_{1}{\mathbin{\parallel}}A_{2}$ of a purely Player
game $A_{1}$ with a purely Opponent game $A_{2}$. Consider a strategy $\sigma$
from a GoI game $A:=A_{1}{\mathbin{\parallel}}A_{2}$ to a GoI game
$B:=B_{1}{\mathbin{\parallel}}B_{2}$. Rearranging the parallel compositions,

$A^{\perp}{\mathbin{\parallel}}B=A_{1}^{\perp}{\mathbin{\parallel}}A_{2}^{\perp}{\mathbin{\parallel}}B_{1}{\mathbin{\parallel}}B_{2}\cong(A_{1}{\mathbin{\parallel}}B_{2}^{\perp})^{\perp}{\mathbin{\parallel}}(A_{2}^{\perp}{\mathbin{\parallel}}B_{1})\,.$

So $\sigma$, as a strategy in $A^{\perp}{\mathbin{\parallel}}B$, corresponds
to a strategy from the purely Player game
$A_{1}{\mathbin{\parallel}}B_{2}^{\perp}$ to the purely Player game
$A_{2}^{\perp}{\mathbin{\parallel}}B_{1}$. We are back to the simple situation
considered in the previous section, of strategies between purely Player games.

Strategies between GoI games, from $A$ to $B$ correspond to stable spans from
${A_{1}{\mathbin{\parallel}}B_{2}^{\perp}}$ to
${A_{2}^{\perp}{\mathbin{\parallel}}B_{1}}$, and to stable functions when
deterministic. Note that a configuration of a parallel composition of games
splits into a pair of configurations:

${\>\\!{\mathscr{C}}(A_{1}{\mathbin{\parallel}}B_{2}^{\perp})\cong\>\\!{\mathscr{C}}(A_{1})\times\,\>\\!{\mathscr{C}}(B_{2}),\
\>\\!{\mathscr{C}}(A_{2}^{\perp}{\mathbin{\parallel}}B_{1})\cong\>\\!{\mathscr{C}}(A_{2})\times\,\>\\!{\mathscr{C}}(B_{1}).}$

Thus deterministic strategies from $A$ to $B$ correspond to stable functions

$S=\langle
f,g\rangle:\>\\!{\mathscr{C}}(A_{1})\times\>\\!{\mathscr{C}}(B_{2})\to\>\\!{\mathscr{C}}(A_{2})\times\>\\!{\mathscr{C}}(B_{1})\,,$

associated with a pair of stable functions
$f:\>\\!{\mathscr{C}}(A_{1})\times\>\\!{\mathscr{C}}(B_{2})\to\>\\!{\mathscr{C}}(A_{2})$
and
$g:\>\\!{\mathscr{C}}(A_{1})\times\,\>\\!{\mathscr{C}}(B_{2})\to\>\\!{\mathscr{C}}(B_{1})$,
summarised diagrammatically by:

$\textstyle{A_{1}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{S}$$\textstyle{B_{1}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{f}$$\textstyle{A_{2}}$$\textstyle{B_{2}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{g}$

Such maps are obtained by Abramsky and Jagadeesan’s GoI construction, here
starting from stable domain theory (Abramsky and Jagadeesan, 1994).

The composition of deterministic strategies between GoI games, $\sigma$ from
$A$ to $B$ and $\tau$ from $B$ to $C$ coincides with the composition of GoI
given by “tracing out” $B_{1}$ and $B_{2}$. Precisely, supposing $\sigma$
corresponds to the stable function

$S:\>\\!{\mathscr{C}}(A_{1})\times\,\>\\!{\mathscr{C}}(B_{2})\to\>\\!{\mathscr{C}}(A_{2})\times\,\>\\!{\mathscr{C}}(B_{1})\,$

and $\tau$ to the stable function

$T:\>\\!{\mathscr{C}}(B_{1})\times\,\>\\!{\mathscr{C}}(C_{2})\to\>\\!{\mathscr{C}}(B_{2})\times\,\>\\!{\mathscr{C}}(C_{1})\,,$

we see a loop in the functional dependency at $B$:

$\textstyle{A_{1}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{S}$$\textstyle{{B_{1}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{T}$$\textstyle{C_{1}}$$\textstyle{A_{2}}$$\textstyle{B_{2}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{C_{2}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$

Accordingly, the composition $\tau{{\odot}}\sigma$ corresponds to the stable
function taking
$(x_{1},z_{2})\in\>\\!{\mathscr{C}}(A_{1})\times\,\>\\!{\mathscr{C}}(C_{2})$
to
$(x_{2},z_{1})\in\>\\!{\mathscr{C}}(A_{2})\times\,\>\\!{\mathscr{C}}(C_{1})$
in the least solution to the equations

$(x_{2},y_{1})=S(x_{1},y_{2})\ \hbox{ and }\ (y_{2},z_{1})=T(y_{1},z_{2})\,$

—given, as in Kahn networks, by taking a least fixed point.

###### Theorem 6.3.

The bicategory of deterministic strategies on GoI games with rigid 2-cells is
equivalent to the Geometry of Interaction category ${\mathscr{G}}({\bf dI})$
of (Abramsky et al., 2002) built on the category $\bf dI$ of dI-domains and
stable functions.

Geometry of Interaction started as an investigation of the nature of proofs of
linear logic, understood as networks (Girard, 1989). It has subsequently been
tied to optimal reduction in the $\lambda$-calculus (Gonthier et al., 1992),
and inspired implementations via token machines on networks (Mackie, 1995;
Muroya and Ghica, 2019); when the two components of a GoI game match events of
exit and entry of a token at a link.

It is straightforward to extend GoI games with winning conditions. A winning
condition on a GoI game $A=A_{1}{\mathbin{\parallel}}A_{2}$ picks out a subset
of the configurations $\>\\!{\mathscr{C}}(A)$, so amounts to specifying a
property $W_{A}(x_{1},x_{2})$ of pairs $(x_{1},x_{2})$ in
$\>\\!{\mathscr{C}}(A_{1})\times\>\\!{\mathscr{C}}(A_{2})$. That a
deterministic strategy from GoI game $A$ to GoI game
$B=B_{1}{\mathbin{\parallel}}B_{2}$ is winning means

$W_{A}(x,g(x,y))\implies W_{B}(f(x,y),y)\,,$

for all $x\in\>\\!{\mathscr{C}}(A_{1}),y\in\>\\!{\mathscr{C}}(B_{2})$, when
expressed in terms of the pair of stable functions the strategy determines. In
particular, a deterministic winning strategy in the individual GoI game $B$,
with winning conditions $W_{B}$, corresponds to a stable function
$f:\>\\!{\mathscr{C}}(B_{2})\to\>\\!{\mathscr{C}}(B_{1})$ such that $\forall
y\in\>\\!{\mathscr{C}}(B_{2}).\ W_{B}(f(y),y)$.

With stable spans, unlike with dI-domains with stable functions, the operation
of parallel composition ${\mathbin{\parallel}}$ is no longer a product; stable
spans are monoidal-closed and not a cartesian-closed. While general, not just
deterministic, strategies $\sigma:A\\!\\!\\!\lx@xy@svg{\hbox{\raise
0.0pt\hbox{\kern
3.0pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
9.4444pt\raise 0.0pt\hbox{\hbox{\kern
0.0pt\raise-1.75pt\hbox{$\scriptstyle{\\!+\\!}$}}}}}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
18.0pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
18.0pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{}$}}}}}}}\ignorespaces}}}}\ignorespaces\\!\\!\\!B$
between GoI games are expressible as stable spans
$A_{1}{\mathbin{\parallel}}B_{2}^{\perp}\\!\\!\\!\lx@xy@svg{\hbox{\raise
0.0pt\hbox{\kern
3.0pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
9.4444pt\raise 0.0pt\hbox{\hbox{\kern
0.0pt\raise-1.75pt\hbox{$\scriptstyle{\\!+\\!}$}}}}}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
18.0pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
18.0pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{}$}}}}}}}\ignorespaces}}}}\ignorespaces\\!\\!\\!A_{2}^{\perp}{\mathbin{\parallel}}B_{1}$,
their expression doesn’t project to an equivalent pair of separate components
as with lenses.

####  6.3.1. The GoI adjunctions

For any game $A$ there is a map of event structures with polarity

$f_{A}:A\to A^{+}{\mathbin{\parallel}}A^{-}\,,$

where $A^{+}$ is the projection of $A$ to its $+$ve events and $A^{-}$ is the
projection to its $-$ve events: the map $f_{A}$ acts as the identity function
on events; it sends a configurations $x\in\>\\!{\mathscr{C}}(A)$ to
$f_{A}x=x^{+}{\mathbin{\parallel}}x^{-}$. It determines an adjunction
$f_{!}\dashv f^{*}$ from $A$ to $A^{+}{\mathbin{\parallel}}A^{-}$. Because the
game $A$ is race-free, both ${f_{A}}_{!}$ and ${f_{A}}^{*}$ are deterministic
strategies. This provides a lax functor from deterministic strategies in
general, to those between GoI games. Let
$\sigma:A\\!\\!\\!\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
3.0pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
9.4444pt\raise 0.0pt\hbox{\hbox{\kern
0.0pt\raise-1.75pt\hbox{$\scriptstyle{\\!+\\!}$}}}}}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
18.0pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
18.0pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{}$}}}}}}}\ignorespaces}}}}\ignorespaces\\!\\!\\!B$ be a
deterministic strategy between games $A$ and $B$. Defining ${\it
goi}(\sigma)={f_{B}}_{!}{{\odot}}\,\sigma\,{{\odot}}{f_{A}}^{*}$ we obtain a
deterministic strategy

${\it
goi}(\sigma):A^{+}{\mathbin{\parallel}}A^{-}\\!\\!\\!\lx@xy@svg{\hbox{\raise
0.0pt\hbox{\kern
3.0pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
9.4444pt\raise 0.0pt\hbox{\hbox{\kern
0.0pt\raise-1.75pt\hbox{$\scriptstyle{\\!+\\!}$}}}}}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
18.0pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
18.0pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{}$}}}}}}}\ignorespaces}}}}\ignorespaces\\!\\!\\!B^{+}{\mathbin{\parallel}}B^{-}\,.$

Then, the strategy ${\it goi}(\sigma)$ corresponds to a stable function from
$A^{+}{\mathbin{\parallel}}B^{-}$ to $A^{-}{\mathbin{\parallel}}B^{+}$, so to
a GoI map. The operation ${\it goi}$ only forms a lax functor however: for
$\sigma:A\\!\\!\\!\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
3.0pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
9.4444pt\raise 0.0pt\hbox{\hbox{\kern
0.0pt\raise-1.75pt\hbox{$\scriptstyle{\\!+\\!}$}}}}}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
18.0pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
18.0pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{}$}}}}}}}\ignorespaces}}}}\ignorespaces\\!\\!\\!B$ and
$\tau:B\\!\\!\\!\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
3.0pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
9.4444pt\raise 0.0pt\hbox{\hbox{\kern
0.0pt\raise-1.75pt\hbox{$\scriptstyle{\\!+\\!}$}}}}}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
18.0pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
18.0pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{}$}}}}}}}\ignorespaces}}}}\ignorespaces\\!\\!\\!C$,
there is, in general, a nontrivial 2-cell ${\it
goi}(\tau{{\odot}}\sigma)\Rightarrow{\it goi}(\tau){{\odot}}{\it
goi}(\sigma)$. This puts pay to ${\it goi}$ being right adjoint to the
“inclusion” functor in a pseudo adjunction from the category of GoI games to
deterministic strategies. But, there is a lax pseudo adjunction, of potential
use in abstract interpretation.

###  6.4. Dialectica games

Dialectica categories were devised in the late 1980’s by Valeria de Paiva in
her Cambridge PhD work with Martin Hyland (de Paiva, 1988). The motivation
then was to provide a model of linear logic underlying Kurt Gödel’s dialectica
interpretation of first-order logic (Avigad and Feferman, 1999). They have
come to prominence again recently because of a renewed interest in their maps
in a variety of contexts, in formalisations of reverse differentiation and
back propagation, open games and learners, and as an early occurrence of maps
as lenses. The dialectica interpretation underpins most proof-mining
techniques (Feferman, 1996; Kohlenbach, 2008).

We obtain a particular dialectica category, based on Berry’s stable functions,
as a full subcategory of deterministic strategies on dialectica games.
Dialectica games are obtained as GoI games of imperfect information,
intuitively by not allowing Player to see the moves of Opponent.

A dialectica game is a GoI game $A=A_{1}{\mathbin{\parallel}}A_{2}$ with
winning conditions, and with imperfect information given as follows. The
imperfect information is determined by particularly simple order of access
levels: ${1}\prec{2}$. All Player moves, those in $A_{1}$, are assigned to
${1}$ and all Opponent moves, those in $A_{2}$, are assigned to ${2}$. It is
helpful to think of the access levels ${1}$ and ${2}$ as representing two
rooms separated by a one-way mirror allowing anyone in room ${2}$ to see
through to room ${1}$. In a dialectica game, Player is in room ${1}$ and
Opponent in room ${2}$. Whereas Opponent can see the moves of Player, and in a
counterstrategy make their moves dependent on those of Player, the moves of
Player are made blindly, in that they cannot depend on Opponent’s moves.

Although we are mainly interested in strategies between dialectica games it is
worth pausing to think about strategies in a single dialectica game
$A=A_{1}{\mathbin{\parallel}}A_{2}$ with winning conditions $W_{A}$. Because
Player moves cannot causally depend on Opponent moves, a deterministic
strategy in $A$ corresponds to a configuration
$x\in\>\\!{\mathscr{C}}(A_{1})$; that it is winning means $\forall
y\in\>\\!{\mathscr{C}}(A_{2}).\ W_{A}(x,y)$. So to have a winning strategy for
the dialectica game means

$\exists x\in\>\\!{\mathscr{C}}(A_{1})\forall y\in\>\\!{\mathscr{C}}(A_{2}).\
W_{A}(x,y)\,.$

Consider now a deterministic winning strategy $\sigma$ from a dialectica game
$A=A_{1}{\mathbin{\parallel}}A_{2}$ with winning conditions $W_{A}$ to another
$B=B_{1}{\mathbin{\parallel}}B_{2}$ with winning conditions $W_{B}$. Ignoring
access levels, $\sigma$ is also a deterministic strategy between GoI games, so
corresponds to a pair of stable functions

$f:\>\\!{\mathscr{C}}(A_{1})\times\>\\!{\mathscr{C}}(B_{2})\to\>\\!{\mathscr{C}}(B_{1})\hbox{
and
}g:\>\\!{\mathscr{C}}(A_{1})\times\>\\!{\mathscr{C}}(B_{2})\to\>\\!{\mathscr{C}}(A_{2})\,.$

But moves in $B_{2}$ have access level ${2}$, moves of $B_{1}$ access level
${1}$; a causal dependency in the strategy $\sigma$ of a move in $B_{1}$ on a
move in $B_{2}$ would violate the access order ${1}\prec{2}$. That no move in
$B_{1}$ can causally depend on a move in $B_{2}$ is reflected in the
functional independence of $f$ on its second argument. As a deterministic
strategy between dialectica categories, $\sigma$ corresponds to a pair of
stable functions

$f:\>\\!{\mathscr{C}}(A_{1})\to\>\\!{\mathscr{C}}(B_{1})\hbox{ and
}g:\>\\!{\mathscr{C}}(A_{1})\times\>\\!{\mathscr{C}}(B_{2})\to\>\\!{\mathscr{C}}(A_{2})\,,$

which we can picture as:

$\textstyle{A_{1}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{g}$$\scriptstyle{f}$$\textstyle{B_{1}}$$\textstyle{A_{2}}$$\textstyle{B_{2}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$

That $\sigma$ is winning means, for all
$x\in\>\\!{\mathscr{C}}(A_{1}),y\in\>\\!{\mathscr{C}}(B_{2})$,

$W_{A}(x,g(x,y))\implies W_{B}(f(x),y)\,.$

Pairs of functions $f,g$ satisfying this winning condition are precisely the
maps of de Paiva’s construction of a dialectica category from Berry’s stable
functions.

Such pairs of functions are the lenses of functional programming where they
were invented to make composable local changes on data-structures (Oles, 1982;
Foster et al., 2007). We recover their at-first puzzling composition from the
composition of strategies. Let $\sigma$ be a deterministic strategy from
dialectica game $A$ to dialectica game $B$; and $\tau$ a deterministic
strategy from $B$ to another dialectica game $C$. Assume $\sigma$ corresponds
to a pair of stable functions $f$ and $g$, as above, and analogously that
$\tau$ correponds to stable functions $f^{\prime}$ and $g^{\prime}$. Then, the
composition of strategies $\tau{{\odot}}\sigma$ corresponds to the composition
of lenses: with first component $f^{\prime}\circ f$ and second component
taking $x\in\>\\!{\mathscr{C}}(A_{1})$ and $y\in\>\\!{\mathscr{C}}(C_{2})$ to
$g(x,g^{\prime}(f(x),y))$.

###### Theorem 6.4.

The bicategory of deterministic strategies on dialectica games with rigid
2-cells is equivalent to the dialectica category of (de Paiva, 1988) built on
dI-domains and stable functions.

#### Girard’s variant

In the first half of de Paiva’s thesis she concentrates on the construction of
dialectica categories. In the second half, she follows up on a suggestion of
Girard to explore a variant. This too is easily understood in the context of
concurrent games: imitate the work of this section, with GoI games extended
with imperfect information, but now with access levels modified to the
discrete order on ${1},{2}$. Then the causal dependencies of strategies are
further reduced and deterministic strategies from
$A=A_{1}{\mathbin{\parallel}}A_{2}$ to $B=B_{1}{\mathbin{\parallel}}B_{2}$
correspond to pairs of stable functions
$f:\>\\!{\mathscr{C}}(A_{1})\to\>\\!{\mathscr{C}}(B_{1})$,
$g:\>\\!{\mathscr{C}}(B_{2})\to\>\\!{\mathscr{C}}(A_{2})$.

#### Combs

Discussions of causality in science, and quantum information in particular,
are often concerned with what causal dependencies are feasible; then
structures similar to orders of access levels are used to capture one-way
signalling, as in dialectica games, and non-signalling, as in Girard’s
variant. In this vein, through another variation of games with imperfect
information, we obtain the generalisation of lenses to combs, used in quantum
architecture and information (Chiribella et al., 2008; Kissinger and Uijlen,
2017). Combs arise as strategies between comb games which, at least formally,
are an obvious generalisation of dialectica games; their name comes from their
graphical representation as structures that look like (hair) combs, with each
tooth representing a transformation from input to output. An $n$-comb game,
for a natural number $n$, is an $n$-fold parallel composition
$A_{1}{\mathbin{\parallel}}A_{2}{\mathbin{\parallel}}\cdots{\mathbin{\parallel}}A_{n}$
of purely Player or purely Opponent games $A_{i}$ of alternating polarity; it
is a game of imperfect information associated with access levels $1\prec
2\prec\cdots\prec n$ with moves of component $A_{i}$ having access level $i$.
Dialectica games are 2-comb games with winning conditions.

#### Open games and learners

There are intriguing connections with open games and learners (Ghani et al.,
2018; Fong et al., 2019). They have recently been presented as parameterised
lenses or optics, in the case of open games with some concept of equilibrium
or winning condition (Capucci et al., 2021). As an example, we obtain a form
of open game between dialectica games $A$ and $B$ as a strategy
$A{\mathbin{\parallel}}P\\!\\!\\!\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
3.0pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
9.4444pt\raise 0.0pt\hbox{\hbox{\kern
0.0pt\raise-1.75pt\hbox{$\scriptstyle{\\!+\\!}$}}}}}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
18.0pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
18.0pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{}$}}}}}}}\ignorespaces}}}}\ignorespaces\\!\\!\\!B$,
where $P$ is a dialectica game of which the configurations specify strategy
profiles. A variation based on optimal strategies between dialectica games
with payoff, following (Clairambault and Winskel, 2013), introduces Nash
equilibria and takes us into game-theory territory, and to a testing ground
for open games and the notions being developed there.

###  6.5. Optics

Now we show that general, possibly nondeterministic, strategies between
dialectica games are precisely optics (Pickering et al., 2017; Riley, 2018)
based on stable spans (Saunders-Evans and Winskel, 2007; Nygaard, 2003;
Winskel, 2011). Recall that a dialectica game comprises
$A_{1}{\mathbin{\parallel}}A_{2}$ where $A_{1}$ is a purely Player game, all
events of which have access level ${1}$ and $A_{2}$ is a purely Opponent game
with all events of access level ${2}$, w.r.t. access order $\Lambda$
specifying $1\prec 2$. We ignore winning conditions.

Let $A$ and $B$ be dialectica games. Let $Q$ be a purely Player
$\Lambda$-game. Recall that nondeterministic strategies between purely Player
games correspond to stable spans. Consider strategies

$F:A_{1}\\!\\!\\!\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
3.0pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
9.4444pt\raise 0.0pt\hbox{\hbox{\kern
0.0pt\raise-1.75pt\hbox{$\scriptstyle{\\!+\\!}$}}}}}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
18.0pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
18.0pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{}$}}}}}}}\ignorespaces}}}}\ignorespaces\\!\\!\\!B_{1}{\mathbin{\parallel}}Q\hbox{
and }G:Q{\mathbin{\parallel}}B_{2}^{\perp}\\!\\!\\!\lx@xy@svg{\hbox{\raise
0.0pt\hbox{\kern
3.0pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
9.4444pt\raise 0.0pt\hbox{\hbox{\kern
0.0pt\raise-1.75pt\hbox{$\scriptstyle{\\!+\\!}$}}}}}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
18.0pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
18.0pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{}$}}}}}}}\ignorespaces}}}}\ignorespaces\\!\\!\\!A_{2}^{\perp}\,.$

Then the strategies $F$ and $G$ are between purely Player games, so correspond
to stable spans—Appendix B. As any causal dependencies of $F$ or $G$ respect
$\Lambda$, they are $\Lambda$-strategies.

Hence the composition

$\textstyle{A_{1}{\mathbin{\parallel}}B_{2}^{\perp}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\\!+\\!}$$\scriptstyle{F{\mathbin{\parallel}}B_{2}^{\perp}}$$\textstyle{B_{1}{\mathbin{\parallel}}Q{\mathbin{\parallel}}B_{2}^{\perp}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\\!+\\!}$$\scriptstyle{B_{1}{\mathbin{\parallel}}G}$$\textstyle{B_{1}{\mathbin{\parallel}}A_{2}^{\perp}}$

is also a $\Lambda$-strategy and, being between purely Player games,
corresponds to a stable span. The composition, rearranges to a strategy

$\sigma:A_{1}{\mathbin{\parallel}}A_{2}\\!\\!\\!\lx@xy@svg{\hbox{\raise
0.0pt\hbox{\kern
3.0pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
9.4444pt\raise 0.0pt\hbox{\hbox{\kern
0.0pt\raise-1.75pt\hbox{$\scriptstyle{\\!+\\!}$}}}}}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
18.0pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
18.0pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{}$}}}}}}}\ignorespaces}}}}\ignorespaces\\!\\!\\!B_{1}{\mathbin{\parallel}}B_{2}\,,$

which is a $\Lambda$-strategy, so to a strategy between the original
dialectica games $A$ and $B$. We call this strategy ${\rm optic}(F,G)$ and
call $(F,G)$ its presentation from $A$ to $B$ with residual $Q$. The
terminology is apt, as we’ll show strategies obtained in this way coincide
with optics as usually defined. Presentations can be represented
diagrammatically:

---
$\textstyle{A_{1}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{F}$$\textstyle{B_{1}}$$\textstyle{Q\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{A_{2}}$$\textstyle{B_{2}\,,\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{G}$

illustrating how $F$ and $G$ are “coupled” via the residual $Q$.

As usually defined, an optic is an equivalence class of presentations. Let
$(F,G)$ and $(F^{\prime},G^{\prime})$ be presentations from $A$ to $B$ with
residuals $Q$ and $Q^{\prime}$ respectively. The equivalence relation $\sim$
on presentations is that generated by taking
$(F,G)\sim(F^{\prime},G^{\prime})$ if, for some
$f:Q\\!\\!\\!\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
3.0pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
9.4444pt\raise 0.0pt\hbox{\hbox{\kern
0.0pt\raise-1.75pt\hbox{$\scriptstyle{\\!+\\!}$}}}}}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
18.0pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
18.0pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{}$}}}}}}}\ignorespaces}}}}\ignorespaces\\!\\!\\!Q^{\prime}$,
the following triangles commute

$None$
---
$\textstyle{A_{1}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{+}$$\scriptstyle{F^{\prime}}$$\scriptstyle{\times}$$\scriptstyle{F}$$\textstyle{B_{1}{\mathbin{\parallel}}Q^{\prime}\\!\\!\\!}$$\textstyle{Q^{\prime}{\mathbin{\parallel}}B_{2}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{+}$$\scriptstyle{G^{\prime}}$$\textstyle{B_{1}}$$\textstyle{B_{1}{\mathbin{\parallel}}Q\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{+}$$\scriptstyle{B_{1}{\mathbin{\parallel}}f}$$\textstyle{Q{\mathbin{\parallel}}B_{2}\,.\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{+}$$\scriptstyle{f{\mathbin{\parallel}}B_{2}}$$\scriptstyle{\times}$$\scriptstyle{G}$

Presentations of optics compose. Let $A$, $B$ and $C$ be dialectica games.
Given a presentation $(F,G)$ from $A$ to $B$ with residual $Q$ and another
$(F^{\prime},G^{\prime})$ from $B$ to $C$ with residual $P$ we obtain a
presentation from $A$ to $C$ with residual $P{\mathbin{\parallel}}Q$ guided by
the diagram

---
$\textstyle{A_{1}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{F}$$\textstyle{B_{1}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{F^{\prime}}$$\textstyle{C_{1}}$$\textstyle{Q\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{P\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{A_{2}}$$\textstyle{B_{2}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{G}$$\textstyle{C_{2}\,,\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{G^{\prime}}$

precisely, as
$((F^{\prime}{\mathbin{\parallel}}Q){{\odot}}F,\,G{{\odot}}(Q{\mathbin{\parallel}}G^{\prime}){{\odot}}(s_{PQ}{\mathbin{\parallel}}C_{2}))$,
where $s_{PQ}$ expresses the symmetry $P{\mathbin{\parallel}}Q\cong
Q{\mathbin{\parallel}}P$.

Composition preserves $\sim$ and has the evident identity presentation, with
residual the empty game. It follows that ${\rm optic}$ is functorial and that
if $(F,G)\sim(F^{\prime},G^{\prime})$ then

${\rm optic}(F,G)\cong{\rm optic}(F^{\prime},G^{\prime})\,.$

To show any strategy between container games is an optic, we exploit the
monoidal-closure of stable spans—see Appendix B. A presentation $(F,G)$ is
$\sim$-equivalent to a canonical presentation $(F^{\prime},G^{\prime})$ with
residual $Q^{\prime}=[B_{2}^{\perp}\multimap A_{2}^{\perp}]$ and $G^{\prime}$
as application ${\rm apply}$: in ($\sim$def), take $f={\rm curry\,}G$ and
$F^{\prime}=(B_{1}{\mathbin{\parallel}}f){{\odot}}F$.

Now, strategies $\sigma:A\\!\\!\\!\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
3.0pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
9.4444pt\raise 0.0pt\hbox{\hbox{\kern
0.0pt\raise-1.75pt\hbox{$\scriptstyle{\\!+\\!}$}}}}}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
18.0pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
18.0pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{}$}}}}}}}\ignorespaces}}}}\ignorespaces\\!\\!\\!B$,
between dialectica games $A$ and $B$, correspond to canonical presentations.
To see this, ignoring the access levels for the moment, a general strategy

$\sigma:A_{1}{\mathbin{\parallel}}A_{2}\\!\\!\\!\lx@xy@svg{\hbox{\raise
0.0pt\hbox{\kern
3.0pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
9.4444pt\raise 0.0pt\hbox{\hbox{\kern
0.0pt\raise-1.75pt\hbox{$\scriptstyle{\\!+\\!}$}}}}}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
18.0pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
18.0pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{}$}}}}}}}\ignorespaces}}}}\ignorespaces\\!\\!\\!B_{1}{\mathbin{\parallel}}B_{2}$

corresponds to a strategy between purely Player games

$\sigma_{1}:A_{1}{\mathbin{\parallel}}B_{2}^{\perp}\\!\\!\\!\lx@xy@svg{\hbox{\raise
0.0pt\hbox{\kern
3.0pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
9.4444pt\raise 0.0pt\hbox{\hbox{\kern
0.0pt\raise-1.75pt\hbox{$\scriptstyle{\\!+\\!}$}}}}}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
18.0pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
18.0pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{}$}}}}}}}\ignorespaces}}}}\ignorespaces\\!\\!\\!B_{1}{\mathbin{\parallel}}A_{2}^{\perp}\,,$

so to a stable span. From the monoidal-closure of stable spans we can curry
$\sigma_{1}$, to obtain a corresponding strategy

$\sigma_{2}:A_{1}\\!\\!\\!\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
3.0pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
9.4444pt\raise 0.0pt\hbox{\hbox{\kern
0.0pt\raise-1.75pt\hbox{$\scriptstyle{\\!+\\!}$}}}}}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
18.0pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
18.0pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{}$}}}}}}}\ignorespaces}}}}\ignorespaces\\!\\!\\![B_{2}^{\perp}\multimap(B_{1}{\mathbin{\parallel}}A_{2}^{\perp})]\,$

with the property

$\sigma_{1}\cong{\rm
apply}_{B_{1}{\mathbin{\parallel}}A_{2}^{\perp}}{{\odot}}(\sigma_{2}{\mathbin{\parallel}}B_{2}^{\perp})\,.$

Recalling the access levels, no event of $B_{1}$ can causally depend on an
event of $B_{2}$, ensuring that $\sigma_{2}$ corresponds to

$\sigma^{+}:A_{1}\\!\\!\\!\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
3.0pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
9.4444pt\raise 0.0pt\hbox{\hbox{\kern
0.0pt\raise-1.75pt\hbox{$\scriptstyle{\\!+\\!}$}}}}}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
18.0pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
18.0pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{}$}}}}}}}\ignorespaces}}}}\ignorespaces\\!\\!\\!B_{1}{\mathbin{\parallel}}[B_{2}^{\perp}\multimap
A_{2}^{\perp}]\,$

where

$\sigma_{1}\cong{\rm
apply}_{B_{1}{\mathbin{\parallel}}A_{2}^{\perp}}{{\odot}}(\sigma_{2}{\mathbin{\parallel}}B_{2}^{\perp})\cong(B_{1}{\mathbin{\parallel}}{\rm
apply}_{A_{2}^{\perp}}){{\odot}}(\sigma^{+}{\mathbin{\parallel}}B_{2}^{\perp})\,.$

It follows that $(\sigma^{+},{\rm apply}_{A_{2}^{\perp}})$ is a canonical
presentation for which

$\sigma\cong{\rm optic}(\sigma^{+},{\rm apply}_{A_{2}^{\perp}})\,,$

giving a correspondence between strategies
$\sigma:A\\!\\!\\!\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
3.0pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
9.4444pt\raise 0.0pt\hbox{\hbox{\kern
0.0pt\raise-1.75pt\hbox{$\scriptstyle{\\!+\\!}$}}}}}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
18.0pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
18.0pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{}$}}}}}}}\ignorespaces}}}}\ignorespaces\\!\\!\\!B$
between dialectica games and canonical presentations $(\sigma^{+},{\rm
apply}_{A_{2}^{\perp}})$.

Via canonical presentations we obtain a bicategory of optics. Its objects are
dialectica games. Its maps are stable spans
$A_{1}\\!\\!\\!\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
3.0pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
9.4444pt\raise 0.0pt\hbox{\hbox{\kern
0.0pt\raise-1.75pt\hbox{$\scriptstyle{\\!+\\!}$}}}}}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
18.0pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
18.0pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{}$}}}}}}}\ignorespaces}}}}\ignorespaces\\!\\!\\!B_{1}{\mathbin{\parallel}}[B_{2}^{\perp}\multimap
A_{2}^{\perp}]\,,$ with the associated 2-cells, from dialectica game $A$ to
dialectica game $B$.

###### Theorem 6.5.

The bicategories of strategies on dialectica games with rigid 2-cells and that
of optics built on stable spans are equivalent.

###  6.6. Containers

A container game is a game of imperfect information $A$ w.r.t. access levels
${1}\prec{2}$; each Player move of $A$ is sent to ${1}$ and each Opponent move
to ${2}$. So in $A$ the only causal dependencies between moves of different
polarity are ${\boxplus}\leq{\boxminus}$.

The configurations of a container game $A$ have a dependent-type structure.
Opponent moves can causally depend on Player moves, but not conversely. Let
$A_{1}$ denote the subgame comprising the initial substructure of purely
Player moves of $A$. A configuration $x\in\>\\!{\mathscr{C}}(A_{1})$
determines a subgame $A_{2}(x)$ comprising the substructure of $A$ based on
all those Opponent moves for which all the Player moves on which they depend
appear in $x$. A configuration of $A$ breaks down uniquely into a union $x\cup
y$, so a pair $(x,y)$, where $x\in\>\\!{\mathscr{C}}(A_{1})$ and
$y\in\>\\!{\mathscr{C}}(A_{2}(x))$. We can see the configurations of a
container game $A$ as forming a dependent sum
$\Sigma_{x:{A_{1}}}\,{{A_{2}(x)}}$. In this way a container game represents a
container type, familiar from functional programming (Abbott et al., 2005);
configurations $x$ of $A_{1}$ are its “shapes” and $y\in A_{2}(x)$ their
“positions.” 111We won’t treat symmetry in concurrent games at all here, but
it is important in many applications. With the addition of symmetry,
configurations form a nontrivial category, not merely a partial order based on
inclusion (Castellan et al., 2014a).

We can of course extend a container game $A$ with winning conditions which we
identify with a property $W_{A}$ of the dependent sum
$\Sigma_{x:{A_{1}}}\,{{A_{2}(x)}}$. A deterministic winning strategy in the
container game corresponds to a configuration $x\in\>\\!{\mathscr{C}}(A_{1})$
such that $\forall y\in\>\\!{\mathscr{C}}({A_{2}(x)}).\ W_{A}(x,y)$.

Strategies between container games respect $\preceq$ on access levels. A
deterministic strategy $\sigma$ from a container game $A$ to a container game
$B$ corresponds to a map of container types, also called a dependent lens,
having type

$None$ $\Sigma_{f:[{A_{1}}\to{B_{1}}]}\Pi_{x:{A_{1}}}\
[{B_{2}(f(x))}\to{A_{2}(x)}]\,;$

so $\sigma$ corresponds to a pair of stable functions

$f:[{A_{1}}\to{B_{1}}]\ \hbox{ and }\
g:\Pi_{x:{A_{1}}}\,[{B_{2}(f(x))}\to{A_{2}(x)}]\,,$

where we are using the function space, dependent sum and product of stable
functions—see Appendix A.2. With winning conditions $W_{A}$ and $W_{B}$, the
strategy from $A$ to $B$ would be winning iff, for all
$x\in\>\\!{\mathscr{C}}(A_{1})$, $y\in\>\\!{\mathscr{C}}(B_{2}(f(x)))$,

$W_{A}(x,g_{x}(y))\implies W_{B}(f(x),y)\,.$

The correspondence respects composition. Container types built on dI-domains
and stable functions arise as a full subcategory of deterministic concurrent
games.

###### Theorem 6.6.

The bicategory of deterministic strategies on container games with rigid
2-cells is equivalent to a full subcategory of containers of dI-domains and
stable functions (Abbott et al., 2005).

###  6.7. Dependent optics

What about general, nondeterministic, strategies between container games? A
way to motivate their characterisation is to observe the isomorphism of the
type of a dependent lens $(*)$ above with

$\Pi_{x:{A_{1}}}\Sigma_{y:{B_{1}}}\ [{B_{2}(y)}\to A_{2}(x)]\,.$

It is this nonstandard way to present the type of lenses that generalises to
the monoidal-closed bicategory of stable spans, once we move to the dependent
product $\Pi^{s}$ of stable spans—Appendix A.2.

Ignoring winning conditions, a general strategy between container games
corresponds to a new form of optic. A dependent optic between container games,
from $A$ to $B$, is a stable span of type

${\bf dOp}[A,B]=\Pi^{s}_{x:{A_{1}}}\Sigma_{y:{B_{1}}}\
[{B_{2}(y)}\multimap{A_{2}(x)}]\,,$

so a rigid map into ${\bf dOp}[A,B]$. A 2-cell $f:F\Rightarrow F^{\prime}$
between dependent optics $F,F^{\prime}:{\bf dOp}[A,B]$ is a 2-cell of stable
spans. Composition of dependent optics is the stable span

${\circ}:{\bf dOp}[B,C]\,{\mathbin{\parallel}}\,{\bf
dOp}[A,B]\\!\\!\\!\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
3.0pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
9.4444pt\raise 0.0pt\hbox{\hbox{\kern
0.0pt\raise-1.75pt\hbox{$\scriptstyle{\\!+\\!}$}}}}}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
18.0pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
18.0pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{}$}}}}}}}\ignorespaces}}}}\ignorespaces\\!\\!\\!{\bf
dOp}[A,C]$

described by

$\displaystyle{G{\circ}F\coloneqq\lambda x:{A_{1}}.\ \hbox{ {\rm let }}}$ | $\displaystyle{{}(y,F^{\prime})\Leftarrow F(x)\hbox{ {\rm in} }}$
---|---
let | $\displaystyle{{}(z,G^{\prime})\Leftarrow G(y)\hbox{ {\rm in} }(z,F^{\prime}{{\odot}}G^{\prime})\,,}$

where $F^{\prime}{{\odot}}G^{\prime}:[{C_{2}(z)}\multimap{A_{2}(x)}]$ is the
composition of stable spans $G^{\prime}:[{C_{2}(z)}\multimap{B_{2}(y)}]$ and
$F^{\prime}:[{B_{2}(y)}\multimap{A_{2}(x)}]$. The identity optic of container
game $A$ acts on $x:A_{1}$ to return the identity at the $x$-component of
$\Sigma_{x:A_{1}}[A_{2}(x)\multimap A_{2}(x)]$.

The equivalence of strategies between container games with dependent optics,
hinges on recasting ${\bf dOp}[A,B]$ as a strategy $\hbox{{\it
do}}[A,B]:A\\!\\!\\!\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
3.0pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
9.4444pt\raise 0.0pt\hbox{\hbox{\kern
0.0pt\raise-1.75pt\hbox{$\scriptstyle{\\!+\\!}$}}}}}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
18.0pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
18.0pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{}$}}}}}}}\ignorespaces}}}}\ignorespaces\\!\\!\\!B$
between container games $A$ and $B$. Any strategy between container games is
of course a strategy where we forget the access levels. We can express that a
strategy $\sigma:A\\!\\!\\!\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
3.0pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
9.4444pt\raise 0.0pt\hbox{\hbox{\kern
0.0pt\raise-1.75pt\hbox{$\scriptstyle{\\!+\\!}$}}}}}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
18.0pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
18.0pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{}$}}}}}}}\ignorespaces}}}}\ignorespaces\\!\\!\\!B$
respects the access levels, so is truly a strategy between container games,
precisely through the presence of a rigid 2-cell

$\textstyle{A\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\\!+\\!}$$\scriptstyle{\sigma}$$\scriptstyle{\\!+\\!}$$\scriptstyle{\hbox{{\it
do}}[A,B]}$$\textstyle{\Downarrow r\\!\\!\\!\\!\\!}$$\textstyle{B\,.}$

The 2-cell $r$ is unique, making the strategy $\hbox{{\it do}}[A,B]$ terminal
amongst strategies $\sigma$ between container games, from $A$ to $B$. By
restricting $r$ to Player moves we obtain the dependent optic $\sigma^{+}:{\bf
dOp}[A,B]$ which corresponds to $\sigma$.

###### Theorem 6.7.

The bicategory of strategies between container games, with rigid 2-cells, is
equivalent to the bicategory of dependent optics.

##  7\. Enrichment

Games and strategies support enrichments, to: probabilistic strategies, also
with continuous distributions (Winskel, 2013a; Paquet and Winskel, 2018);
quantum strategies (Clairambault et al., 2019); and strategies on the reals
(Alcolei, 2019). The enrichments specialise to the cases above; e.g.,
probabilistic strategies specialise to optics based on Markov kernels when
between dialectica games.

The enrichments were developed individually and are not always the final
story. For instance, the assignment of quantum operators to configurations of
strategies in (Clairambault et al., 2019) is not functorial w.r.t. inclusion
on configurations, a defect when it comes to understanding how the operator of
a configuration is built up. The authors’ remedy also achieves all the
enrichments just named, now uniformly by the same construction.

The construction is w.r.t. a symmetric monoidal category
$(\mathscr{M},\otimes,{\rm I})$. For example, $\mathscr{M}$ can be the monoid
$([0,1],\cdot,1)$ comprising the unit interval under multiplication (for
probabilistic strategies); measurable spaces with Markov kernels (for
probabilistic strategies with continuous distributions); CPM, finite-
dimensional Hilbert spaces with completely positive maps (for quantum
strategies); or Euclidean spaces with smooth maps, to support (reverse)
differentiation.

We first extend $\mathscr{M}$ to allow interaction beyond that from argument
to result. The parameterised category $\rm Para({\mathscr{M}})$ has the same
objects, now with maps $(P,f,Q):X\to Y$ consisting of $f:X\otimes P\to
Q\otimes Y$ in $\mathscr{M}$; the parameters $P$ and $Q$ allow input and
output with the environment. Composition accumulates parameters:
$(R,g,S)\circ(P,f,Q)\coloneqq(P\otimes R,\ (Q\otimes g)\circ(f\otimes R),\
Q\otimes S)$. Then,

(1)  moves $a$ of a game $A$ are assigned objects ${\mathscr{H}}(a)$ in
$\mathscr{M}$, extended to $X\in{\rm Con}_{A}$ by
${\mathscr{H}}(X)\coloneqq\bigotimes_{a\in X}{\mathscr{H}}(a)$. (When neutral
moves appear, as in interaction, they are assigned the tensor unit $\rm I$.)

(2)  an $\mathscr{M}$-enriched strategy $\sigma:S\to A$ is accompanied by a
functor ${\mathscr{Q}}:(\>\\!{\mathscr{C}}(S)^{o},\subseteq)\to\rm
Para({\mathscr{M}})$. To an interval $x\subseteq x^{\prime}$ in
$\>\\!{\mathscr{C}}(S)^{o}$ this assigns a parameterised map
${\mathscr{Q}}(x\subseteq x^{\prime})$ with input parameters
${\mathscr{H}}(\sigma{(x^{\prime}\setminus x)}^{-})$ and output parameters
${\mathscr{H}}(\sigma{(x^{\prime}\setminus x)}^{+})$.

The assignment in (2) describes how the internal state is transformed in
moving from $x$ to $x^{\prime}$ under interaction via events
$x^{\prime}\setminus x$. In the probabilistic and quantum cases, observation
is contextual, reflected in the presence of a drop condition, a form of
inclusion-exclusion principle (Winskel, 2013a; Clairambault et al., 2019); it
requires $\mathscr{M}$ be enriched over, at least, cancellative commutative
monoids. Then, the assignment in (2) is oblivious, i.e.
${\mathscr{Q}}(x\subseteq^{-}x^{\prime})$ is always an isomorphism in
$\mathscr{M}$, expressing that the input from $x^{\prime}\setminus x$ is
adjoined to the internal state.

Events, their positions, dependencies and polarities, orchestrate the
functional dependency and dynamic linkage in composing enriched strategies.

Enrichments achieved in this way transfer automatically to subcategories, and
the functional cases we have considered, without needing extra demands on the
category $\mathscr{M}$.

##  8\. Conclusion

In conclusion, functional paradigms can help tame the wild world of
interactive computation. On the other hand, discovering the simplifying
paradigms has often required considerable ingenuity. The challenges are even
more acute with enrichments, say to probabilistic, quantum or real number
computation. The traditional categories of mathematics do not often support
all the features required by computation. They often don’t have function
spaces or support recursion. It is as if each case has had to be dealt with
separately.

A model of interaction is more technically challenging and requires a new,
more local, way of thinking. But, as has been demonstrated here, it can
provide a broad general context for interaction which can be specialised to
functional paradigms, also in providing enrichments to probabilistic, quantum
and real number computation, without requiring clever extensions to the
traditional categories of mathematics. There is work to do, specifically in
connecting concurrent games and strategies with the theory of effects (Moggi,
1989; Plotkin and Power, 2004), but a lot can be said for a single,
intrinsically higher-order framework which readily adapts to enrichments.

###### Acknowledgements.

I’m grateful for discussions with Bob Atkey, Matteo Capucci, Fredrik Nordvall
Forsberg, Bruno Gavranovic, Neil Ghani, Dan Ghica, Samuel Ben Hamou, Jules
Hedges, Martin Hyland, Clemens Kupke, Jérémy Ledent, Valeria de Paiva, Hugo
Paquet and James Wood; I learnt of optics and combs from Jules and Jérémy.
Samuel Ben Hamou, ENS Paris Saclay, tackled the verification of the early part
of the dialectica-games section for his student internship. Section 7 is
directly inspired by joint work with Pierre Clairambault and Marc de Visme.

## References

  * (1)
  * Abbott et al. (2005) Michael Gordon Abbott, Thorsten Altenkirch, and Neil Ghani. 2005\.  Containers: Constructing strictly positive types.  _Theor. Comput. Sci._ 342, 1 (2005), 3–27.  https://doi.org/10.1016/j.tcs.2005.06.002
  * Abramsky et al. (2002) Samson Abramsky, Esfandiar Haghverdi, and Philip J. Scott. 2002\.  Geometry of Interaction and Linear Combinatory Algebras.  _Math. Struct. Comput. Sci._ 12, 5 (2002), 625–665.  https://doi.org/10.1017/S0960129502003730
  * Abramsky and Jagadeesan (1994) Samson Abramsky and Radha Jagadeesan. 1994.  New Foundations for the Geometry of Interaction.  _Inf. Comput._ 111, 1 (1994), 53–119.  https://doi.org/10.1006/inco.1994.1041
  * Alcolei (2019) Aurore Alcolei. 2019\.  _Enriched concurrent games : witnesses for proofs and resource analysis. (Jeux concurrents enrichis : témoins pour les preuves et les ressources)_.  Ph.D. Dissertation. University of Lyon, France.  https://tel.archives-ouvertes.fr/tel-02448974
  * Avigad and Feferman (1999) Jeremy Avigad and Solomon Feferman. 1999.  Gödel’s functional (”Dialectica”) interpretation.  (1999), 337–405.
  * Berry (1978) Gérard Berry. 1978\.  Stable Models of Typed lambda-Calculi. In _ICALP_ _(Lecture Notes in Computer Science)_ , Vol. 62. Springer, 72–89.
  * Capucci et al. (2021) Matteo Capucci, Bruno Gavranović, Jules Hedges, and Eigil Fjeldgren Rischel. 2021.  Towards foundations of categorical cybernetics.  arXiv:2105.06332 [math.CT]
  * Castellan et al. (2014a) Simon Castellan, Pierre Clairambault, and Glynn Winskel. 2014a.  Symmetry in concurrent games. In _Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS ’14, Vienna, Austria, July 14 - 18, 2014_. ACM.
  * Castellan et al. (2014b) Simon Castellan, Jonathan Hayman, Marc Lasson, and Glynn Winskel. 2014b.  Strategies as concurrent processes.  _Electr. Notes Theor. Comput. Sci._ 308 (2014), 87–107.
  * Chiribella et al. (2008) G. Chiribella, G. M. D’Ariano, and P. Perinotti. 2008\.  Quantum Circuit Architecture.  _Physical Review Letters_ 101, 6 (Aug 2008).  https://doi.org/10.1103/physrevlett.101.060401
  * Clairambault et al. (2019) Pierre Clairambault, Marc de Visme, and Glynn Winskel. 2019\.  Game semantics for quantum programming.  _Proc. ACM Program. Lang._ 3, POPL (2019), 32:1–32:29.  https://doi.org/10.1145/3290345
  * Clairambault et al. (2012) Pierre Clairambault, Julian Gutierrez, and Glynn Winskel. 2012\.  The Winning Ways of Concurrent Games. In _LICS 2012: 235-244_.
  * Clairambault and Winskel (2013) Pierre Clairambault and Glynn Winskel. 2013.  On Concurrent Games with Payoff.  _Electr. Notes Theor. Comput. Sci. 298: 71-92_ (2013).
  * Conway (2000) John Conway. 2000\.  _On Numbers and Games_.  Wellesley, MA: A K Peters.
  * Coquand et al. (1987) Thierry Coquand, Carl A. Gunter, and Glynn Winskel. 1987\.  DI-Domains as a Model of Polymorphism. In _Mathematical Foundations of Programming Language Semantics, 3rd Workshop, Tulane University, New Orleans, Louisiana, USA, April 8-10, 1987, Proceedings_ _(Lecture Notes in Computer Science)_ , Michael G. Main, Austin Melton, Michael W. Mislove, and David A. Schmidt (Eds.), Vol. 298. Springer, 344–363.  https://doi.org/10.1007/3-540-19020-1_18
  * Coquand et al. (1989) Thierry Coquand, Carl A. Gunter, and Glynn Winskel. 1989\.  Domain Theoretic Models of Polymorphism.  _Inf. Comput._ 81, 2 (1989), 123–167.  https://doi.org/10.1016/0890-5401(89)90068-0
  * de Paiva (1988) Valeria de Paiva. 1988\.  _The Dialectica categories_.  PhD Thesis, University of Cambridge.
  * Faggian and Piccolo (2009) Claudia Faggian and Mauro Piccolo. 2009.  Partial orders, event structures and linear strategies. In _TLCA ’09_ _(LNCS)_ , Vol. 5608. Springer.
  * Feferman (1996) Solomon Feferman. 1996\.  Kreisel’s ‘Unwinding Program’, Kreiseliana: about and around Georg Kreisel.  (1996), 247–273.
  * Fiore et al. (2018) Marcelo Fiore, Nicola Gambino, Martin Hyland, and Glynn Winskel. 2018.  Relative pseudomonads, Kelisli bicategories and substitution monoidal structures.  _Selecta Mathematica - New Series_ 24, 3 (2018), 2791–2830.
  * Fong et al. (2019) Brendan Fong, David I. Spivak, and Rémy Tuyéras. 2019\.  Backprop as Functor: A compositional perspective on supervised learning. In _34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019, Vancouver, BC, Canada, June 24-27, 2019_. IEEE, 1–13.  https://doi.org/10.1109/LICS.2019.8785665
  * Foster et al. (2007) J. Nathan Foster, Michael B. Greenwald, Jonathan T. Moore, Benjamin C. Pierce, and Alan Schmitt. 2007\.  Combinators for bidirectional tree transformations: A linguistic approach to the view-update problem.  _ACM Trans. Program. Lang. Syst._ 29, 3 (2007), 17\.  https://doi.org/10.1145/1232420.1232424
  * Ghani et al. (2018) Neil Ghani, Jules Hedges, Viktor Winschel, and Philipp Zahn. 2018\.  Compositional Game Theory. In _Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018_ , Anuj Dawar and Erich Grädel (Eds.). ACM, 472–481.  https://doi.org/10.1145/3209108.3209165
  * Girard (1989) Jean-Yves Girard. 1989\.  Geometry of interaction I: Interpretation of system F. In _Logic Colloquium ’88_ , C. Bonotto, S R. Ferro, Valentini, and A. Zanardo (Eds.). North-Holland, 221–260.
  * Gonthier et al. (1992) Georges Gonthier, Martín Abadi, and Jean-Jacques Lévy. 1992.  The Geometry of Optimal Lambda Reduction. In _Conference Record of the Nineteenth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Albuquerque, New Mexico, USA, January 19-22, 1992_ , Ravi Sethi (Ed.). ACM Press, 15–26.  https://doi.org/10.1145/143165.143172
  * Johnson and Yau (2020) Niles Johnson and Donald Yau. 2020.  2-Dimensional Categories.  arXiv:2002.06055 [math.CT]
  * Joyal (1997) Andre Joyal. 1997\.  Remarques sur la théorie des jeux à deux personnes.  _Gazette des sciences mathématiques du Québec, 1(4)_ (1997).
  * Kissinger and Uijlen (2017) Aleks Kissinger and Sander Uijlen. 2017.  A categorical semantics for causal structure. In _32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, June 20-23, 2017_. IEEE Computer Society, 1–12.  https://doi.org/10.1109/LICS.2017.8005095
  * Kohlenbach (2008) Ulrich Kohlenbach. 2008\.  _Applied Proof Theory: Proof Interpretations and their Use in Mathematics_.  Springer Monographs in Mathematics.
  * Mackie (1995) Ian Mackie. 1995\.  The Geometry of Interaction Machine. In _Conference Record of POPL’95: 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Francisco, California, USA, January 23-25, 1995_ , Ron K. Cytron and Peter Lee (Eds.). ACM Press, 198–208.  https://doi.org/10.1145/199448.199483
  * Melliès and Mimram (2007) Paul-André Melliès and Samuel Mimram. 2007.  Asynchronous games : innocence without alternation. In _CONCUR ’07_ _(LNCS)_ , Vol. 4703. Springer.
  * Moggi (1989) Eugenio Moggi. 1989\.  Computational Lambda-Calculus and Monads. In _Proceedings of the Fourth Annual Symposium on Logic in Computer Science (LICS ’89), Pacific Grove, California, USA, June 5-8, 1989_. IEEE Computer Society, 14–23.  https://doi.org/10.1109/LICS.1989.39155
  * Muroya and Ghica (2019) Koko Muroya and Dan R. Ghica. 2019.  The Dynamic Geometry of Interaction Machine: A Token-Guided Graph Rewriter.  _Log. Methods Comput. Sci._ 15, 4 (2019).  https://doi.org/10.23638/LMCS-15(4:7)2019
  * Nygaard (2003) Mikkel Nygaard. 2003\.  _Domain theory for concurrency_.  PhD Thesis, Aarhus University.
  * Nygaard and Winskel (2002) Mikkel Nygaard and Glynn Winskel. 2002.  Linearity in Process Languages. In _LICS’02_. IEEE Computer Society.
  * Oles (1982) Frank J. Oles. 1982\.  _A category theoretic approach to the semantics of programming languages_.  PhD Thesis, University of Syracuse.
  * Paquet (2020) Hugo Paquet. 2020\.  _Probabilistic concurrent game semantics_.  Ph.D. Dissertation. Computer Laboratory, University of Cambridge, UK.
  * Paquet and Winskel (2018) Hugo Paquet and Glynn Winskel. 2018.  Continuous Probability Distributions in Concurrent Games. In _Proceedings of the Thirty-Fourth Conference on the Mathematical Foundations of Programming Semantics, MFPS 2018, Dalhousie University, Halifax, Canada, June 6-9, 2018_ _(Electronic Notes in Theoretical Computer Science)_ , Sam Staton (Ed.), Vol. 341. Elsevier, 321–344.  https://doi.org/10.1016/j.entcs.2018.11.016
  * Pickering et al. (2017) Matthew Pickering, Jeremy Gibbons, and Nicolas Wu. 2017\.  Profunctor Optics: Modular Data Accessors.  _Art Sci. Eng. Program._ 1, 2 (2017), 7.  https://doi.org/10.22152/programming-journal.org/2017/1/7
  * Plotkin and Power (2004) Gordon D. Plotkin and A. John Power. 2004.  Computational Effects and Operations: An Overview.  _Electron. Notes Theor. Comput. Sci._ 73 (2004), 149–163.  https://doi.org/10.1016/j.entcs.2004.08.008
  * Rideau and Winskel (2011) Silvain Rideau and Glynn Winskel. 2011.  Concurrent Strategies. In _LICS 2011_.
  * Riley (2018) Mitchell Riley. 2018\.  Categories of Optics.  arXiv:1809.00738 [math.CT]
  * Saunders-Evans and Winskel (2007) Lucy Saunders-Evans and Glynn Winskel. 2007.  Event Structure Spans for Nondeterministic Dataflow.  _Electr. Notes Theor. Comput. Sci. 175(3): 109-129_ (2007).
  * Winskel (1982) Glynn Winskel. 1982\.  Event Structure Semantics for CCS and Related Languages. In _ICALP’82_ _(LNCS)_ , Vol. 140. Springer, A full version is available from Winskel’s Cambridge homepage.
  * Winskel (1986) Glynn Winskel. 1986\.  Event Structures. In _Advances in Petri Nets_ _(LNCS)_ , Vol. 255. Springer, 325–392.
  * Winskel (2009) Glynn Winskel. 2009\.  Prime algebraicity.  _Theor. Comput. Sci._ 410, 41 (2009), 4160–4168.  https://doi.org/10.1016/j.tcs.2009.06.015
  * Winskel (2011) Glynn Winskel. 2011\.  Events, Causality and Symmetry.  _Comput. J._ 54, 1 (2011), 42–57.
  * Winskel (2012a) Glynn Winskel. 2012a.  Deterministic concurrent strategies.  _Formal Asp. Comput._ 24, 4-6 (2012), 647–660.
  * Winskel (2012b) Glynn Winskel. 2012b.  Winning, Losing and Drawing in Concurrent Games with Perfect or Imperfect Information. In _Festschrift for Dexter Kozen_ _(LNCS)_ , Vol. 7230. Springer.
  * Winskel (2013a) Glynn Winskel. 2013a.  Distributed Probabilistic and Quantum Strategies.  _Electr. Notes Theor. Comput. Sci. 298: 403-425_ (2013).
  * Winskel (2013b) Glynn Winskel. 2013b.  Strategies as profunctors. In _FOSSACS 2013_ _(Lecture Notes in Computer Science)_. Springer.
  * Winskel (2016) Glynn Winskel. 2016\.  _ECSYM Notes: Event Structures, Stable Families and Concurrent Games_.  http://www.cl.cam.ac.uk/$\sim$gw104/ecsym-notes.pdf.

##  Appendix A dI-domains and stable functions

That dI-domains are exactly the partial orders of configurations of an event
structure was first published in (Winskel, 1982)—see the extended version or
(Winskel, 2009) for the proof. A stable function between dI-domains is a Scott
continuous function (i.e. preserves least upper bounds of directed sets) which
preserves meets of compatible pairs of elements. Gérard Berry developed stable
domain theory axiomatically, following operational guidelines (Berry, 1978).
For the reader’s convenience, we include the constructions on event structures
which realise the cartesian-closure of dI-domains and their dependent types.

###  A.1. Stable function space

Berry’s cartesian-closed category of dI-domains 222Strictly speaking, Berry
defined dI-domains to have a countable basis of finite elements. Countability
plays no role in the work here and we shall not impose it. and stable
functions can be presented as an equivalent category of event structures
(Winskel, 1986). We summarise the product and stable function space
constructions on stable families and event structures.

Let ${\mathscr{A}}$ and ${\mathscr{B}}$ be stable families with events $A$ and
$B$ respectively. The product of their domains of configurations is easily
realised as a simple parallel composition:
${\mathscr{A}}{\mathbin{\parallel}}{\mathscr{B}}\coloneqq{\\{x{\mathbin{\parallel}}y\
|\ x\in{\mathscr{A}}\ \&\ y\in{\mathscr{B}}\\}}$.

We construct the stable function space of domains as a stable family
$[{\mathscr{A}}\to{\mathscr{B}}]$. The stable family
$[{\mathscr{A}}\to{\mathscr{B}}]$ comprises those
$f\subseteq{\mathscr{A}}^{o}\times B$ for which, for all $x\in{\mathscr{A}}$,

  * •

${\\{b\ |\ \exists x^{\prime}\subseteq x.\ (x^{\prime},b)\in