<figure><img src="image_1.png" /></figure>

HAL
open science

# Causal Investigations in Interactive Semantics

Pierre Clairambault

► To cite this version:

Pierre Clairambault. Causal Investigations in Interactive Semantics. Computer Science and Game Theory [cs.GT]. Aix-Marseille Université, 2024. tel-04523273

HAL Id: tel-04523273

https://hal.science/tel-04523273

Submitted on 27 Mar 2024

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_2.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
Causal Investigations in Interactive Semantics

<figure><img src="image_3.png" /></figure>

Mémoire présenté par

Pierre Clairambault

en vue d'obtenir

l'Habilitation à Diriger des Recherches
(Informatique)

le 21 février 2024 devant le jury composé de:

Dan Ghica

Delia Kesner

Ugo Dal Lago

Damiano Mazza

Guy McCusker

Paul-André Melliès

Laurent Regnier

Huawei, University of Birmingham

IRIF, Université Paris Cité

University of Bologna

CNRS, LIPN, Université Paris Nord

University of Bath

CNRS, IRIF, Université Paris Cité

Aix-Marseille Université

Rapporteur

Examinatrice

Examineur

Président

Rapporteur

Rapporteur

Examineur

<figure><img src="image_4.png" /></figure>
Remerciements

Tout d'abord, merci à tous mes collaborateurs passés sur ce formidable thème des jeux
concurrents. Merci à Glynn pour m'avoir fait découvrir les structures d'événements et
avoir accompagné mes premiers pas dans cette belle direction de recherche. Merci à
Simon C.: nos séances de travail sur les jeux concurrents fins et l'innocence parallèle
resteront parmis mes plus beaux souvenirs de collaboration scientifique. Merci à Aurore
pour m'avoir accompagné sur les traces de Herbrand. Merci à Hugo pour une touche
de probabilité, et pour m'avoir convaincu que les bicatégories, c'est après tout peut-être
pas complètement inutile. Merci à Marc d'avoir insisté pour faire du quantique, menant
à, à mon avis, une des plus belles applications des jeux concurrents. Merci à Lison et
Lionel grâce à qui j'ai enfin pû comprendre le développement de Taylor (c'est de la
sémantique des jeux). Merci à Simon F., grâce à qui on peut maintenant faire des jeux
concurrents fins sans jeux concurrents.

Merci à tous les collègues de l'équipe Plume du LIP de m'avoir patiemment écouté parler de structures d'événements pendant toutes ces années, et en particulier Colin qui ne pouvait pas s'enfuir puisque nous partagions le même bureau. Merci à tous les collègues marseillais, du LIS et de l'I2M, d'avoir pris le relais, de m'avoir si bien acceuilli lors de mon arrivée à Marseille, et de contribuer à un cadre de vie et de travail exceptionnel – en particulier Raphaëlle, qui a brillamment pris la suite de Colin.

Merci à Dan, Guy et Paul-André d'avoir accepté de rapporter ce travail, malgré son
volume déraisonnable: vous êtes sûrement les trois chercheurs dont le travail a le plus
influencé ma vision scientifique, et je vous suis reconnaissant de votre relecture appro-
fondie de ma contribution. Merci à Delia, Ugo et Damiano d'avoir bien voulu être mem-
bres de ce jury, et merci à Laurent de m'avoir guidé dans cette aventure de l'habilitation.

Merci à tous ceux que j'oublie et qui regrettent de ne pas trouver leur nom ici.

Et pour tout le reste, merci à Marie-Laure.
# Résumé

La sémantique des jeux est un cadre mathématique puissant pour raisonner de façon compositionnelle sur les programmes. Contrairement aux méthodes plus classiques de sémantique dénotationnelle, elle ne voit pas les programmes simplement comme des fonctions mathématiques prenant une valeur en entrée et rendant une valeur en sortie, mais comme des processus dynamiques et interactifs. Elle capture de façon compositionnelle le flot de contrôle même pour des programmes disposants de primitives calculatoires complexes: ordre supérieur, état mutable, opérateurs de contrôle, etc.

Mais la sémantique des jeux n’est pas une théorie mathématique: c’est plus une con-
stellation de modèles disparates sans réel liant autre que le folklore de quelques experts
du domaine. L’un de ces modèles disparates est celui des jeux concurrents, qui hérite
des jeux concurrents d’Abramsky et Melliès et des jeux asynchrones de Melliès. Dans
sa formulation récente proposée par Rideau et Winskel, ce modèle est basé sur les struc-
tures d’événements, un modèle de concurrence vraie qui évite de supposer l’existence
d’une horloge globale et représente plutôt les programmes par leur structure causale.

Bien entendu, les jeux concurrents permettent de modéliser la programmation con-
currente. Mais dans ce manuscrit, je montre que plus qu’un modèle comme un autre,
leur expressivité permet de mettre en avant des structures implicites dans plusieurs
autres modèles de la littérature pour des langages concurrents, ou pas. Ce faisant, sur
les traces de la vision d’Abramsky et Melliès, ils permettent une synthèse jusqu’alors
absente et contribuent à faire de la sémantique des jeux une théorie mathématique.

Concrètement, ce manuscrit commence en Partie I par une introduction détaillée à
différentes sémantiques des jeux traditionnelles à pointeurs: d'abord pour le langage
fonctionnel paradigmatique PCF, son extension IA avec mémoire mutable, puis le mod-
èle de jeux non alternants pour son extension concurrente IA<sub>∥</sub>. En Partie II, je donne
une présentation complète des jeux concurrents et de leur extension avec symétrie. En
partie III, je relie les jeux concurrents aux différents modèles de la Partie I – mais aussi
d'autres, tels que le modèle relationnel – via des foncteurs préservant l'interprétation.
Finalement, en Partie IV, je passe en revue d'autres développements en jeux concur-
rents, et conclus sur des problèmes ouverts et perspectives futures.
# Abstract

*Game Semantics* is a powerful mathematical framework to reason compositionally on programs. In contrast to other more classical methods in denotational semantics, game semantics sees programs not merely as mathematical functions taking inputs (which may be functions themselves) and producing outputs, but rather, sees them as dynamic and interactive processes. It captures compositionally the control flow even for programs with complex computational primitives such as higher-order, mutable state, control operators, etc.

However, game semantics is not a *mathematical theory*: rather, it is a loose collection of separated technical settings, sometimes only loosely connected by the folklore of a handful of experts. One of those technical setting is *concurrent games*, inheriting from the concurrent games of Abramsky and Melliès and from Melliès' asynchronous games. In its recent technical set-up proposed by Rideau and Winskel, this model is based on *event structures*, a *true concurrency* model that avoids assuming the existence of a global clock, representing instead programs via their causal structure.

Of course, concurrent games can handle the semantics of concurrent programs. But in this monograph, I show that more than yet another new model, their expressivity reveals structures implicitly present in several other models from the literature, for concurrent languages, or not. In doing so, walking in the footsteps of Abramsky and Melliès' vision, they give us the means for a synthesis between various games or other denotational models, bringing game semantics one step closer to a mathematical theory.

Concretely, this monograph starts in Part I with a detailed introduction to several traditional *pointer game semantics*: first for the paradigmatic purely functional language PCF, its extension IA with mutable state, and the non-alternating variant for its concurrent extension IA$\parallel$. In Part II, I give a complete presentation of concurrent games and their extension with symmetry. In Part III, I link concurrent games to the different games models introduced in Part I – but also other models, such as the relational model – via interpretation-preserving functors. Finally, in Part IV, I survey other developments in concurrent games, and I conclude with some open problems and perspectives.
# Contents

<table><tbody><tr><td><strong>1 Introduction</strong></td><td><strong>12</strong></td></tr><tr><td>&nbsp;&nbsp;&nbsp;&nbsp;1.1 Operational Semantics</td><td>12</td></tr><tr><td>&nbsp;&nbsp;&nbsp;&nbsp;1.2 Toward a Mathematical Semantics</td><td>13</td></tr><tr><td>&nbsp;&nbsp;&nbsp;&nbsp;1.3 The Next 700 Denotational Semantics</td><td>16</td></tr><tr><td>&nbsp;&nbsp;&nbsp;&nbsp;1.4 Full Abstraction and Intentional Intensionality</td><td>17</td></tr><tr><td>&nbsp;&nbsp;&nbsp;&nbsp;1.5 Plays Considered Harmful</td><td>18</td></tr><tr><td>&nbsp;&nbsp;&nbsp;&nbsp;1.6 A Case for Causal Game Semantics</td><td>21</td></tr><tr><td>&nbsp;&nbsp;&nbsp;&nbsp;1.7 Contributions and Outline</td><td>23</td></tr><tr><td><strong>2 General Preliminaries</strong></td><td><strong>26</strong></td></tr><tr><td>&nbsp;&nbsp;&nbsp;&nbsp;2.1 Mathematical Language</td><td>26</td></tr><tr><td>&nbsp;&nbsp;&nbsp;&nbsp;2.2 IA<sub>∥</sub> and its Fragments</td><td>27</td></tr><tr><td>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;2.2.1 Syntax of IA<sub>∥</sub></td><td>28</td></tr><tr><td>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;2.2.2 Operational Semantics of IA<sub>∥</sub></td><td>30</td></tr><tr><td>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;2.2.3 Expressiveness of IA<sub>∥</sub></td><td>30</td></tr><tr><td>&nbsp;&nbsp;&nbsp;&nbsp;2.3 Generalities on Semantics</td><td>34</td></tr><tr><td><strong>I Pointer Game Semantics</strong></td><td><strong>37</strong></td></tr><tr><td><strong>3 First Steps in Game Semantics</strong></td><td><strong>41</strong></td></tr><tr><td>&nbsp;&nbsp;&nbsp;&nbsp;3.1 Executions, Plays, and Strategies</td><td>41</td></tr><tr><td>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;3.1.1 Dialogues, Plays, and Simple Games</td><td>41</td></tr><tr><td>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;3.1.2 Replication and Thread Indexing</td><td>44</td></tr><tr><td>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;3.1.3 Pointer Games</td><td>45</td></tr><tr><td>&nbsp;&nbsp;&nbsp;&nbsp;3.2 Carving Out Innocent Strategies</td><td>48</td></tr><tr><td>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;3.2.1 The Strategies of PCF</td><td>48</td></tr><tr><td>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;3.2.2 Well-Bracketing</td><td>50</td></tr><tr><td>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;3.2.3 Visibility and Innocence</td><td>52</td></tr><tr><td>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;3.2.4 Finite Definability and Full Abstraction</td><td>54</td></tr><tr><td>&nbsp;&nbsp;&nbsp;&nbsp;3.3 Non-Innocence and Effects</td><td>57</td></tr><tr><td>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;3.3.1 Non-Local State</td><td>57</td></tr><tr><td>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;3.3.2 Higher-Order State</td><td>58</td></tr><tr><td>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;3.3.3 The “Semantic Cube”</td><td>59</td></tr></tbody></table>
<table><tr><td>3.4</td><td>An Alternative to Pointers: Copy Indices</td><td>63</td></tr></table>

<table><tr><td>3.5</td><td>Conclusions and Historical Notes</td><td>66</td></tr></table>

4 The Category of Alternating Strategies 67

<table><tr><td>4.1</td><td>The Ambient Cartesian Closed Category $\downarrow\uparrow$-Strat</td><td>67</td></tr></table>

<table><tr><td>4.1.1</td><td>More Arena Constructions</td><td>67</td></tr></table>

<table><tr><td>4.1.2</td><td>Composition of Strategies</td><td>68</td></tr></table>

<table><tr><td>4.1.3</td><td>A Category of Arenas and Strategies</td><td>72</td></tr></table>

<table><tr><td>4.1.4</td><td>Cartesian Closed Structure</td><td>74</td></tr></table>

<table><tr><td>4.1.5</td><td>Recursion</td><td>76</td></tr></table>

<table><tr><td>4.2</td><td>Interpretation of IA</td><td>76</td></tr></table>

<table><tr><td>4.2.1</td><td>Interpretation of PCF</td><td>77</td></tr></table>

<table><tr><td>4.2.2</td><td>Interpretation of State</td><td>77</td></tr></table>

<table><tr><td>4.3</td><td>Complements on Alternating Strategies</td><td>82</td></tr></table>

<table><tr><td>4.3.1</td><td>Complements on Single-Threadedness</td><td>82</td></tr></table>

<table><tr><td>4.3.2</td><td>Factorization and Definability</td><td>84</td></tr></table>

<table><tr><td>4.3.3</td><td>Summary of Results</td><td>85</td></tr></table>

<table><tr><td>4.4</td><td>Conclusions and Historical Notes</td><td>85</td></tr></table>

5 Non-Alternating Game Semantics 87

<table><tr><td>5.1</td><td>Concurrency and Non-Alternation</td><td>87</td></tr></table>

<table><tr><td>5.1.1</td><td>Non-Alternating Plays</td><td>87</td></tr></table>

<table><tr><td>5.1.2</td><td>Non-Alternating Strategies</td><td>90</td></tr></table>

<table><tr><td>5.1.3</td><td>Single-Threadedness</td><td>92</td></tr></table>

<table><tr><td>5.1.4</td><td>Full Abstraction for IA<sub>✓</sub></td><td>93</td></tr></table>

<table><tr><td>5.2</td><td>The Ambient Cartesian Closed Category $\mathcal{O}$-Strat</td><td>96</td></tr></table>

<table><tr><td>5.2.1</td><td>Constructing $\mathcal{O}$-Strat</td><td>96</td></tr></table>

<table><tr><td>5.2.2</td><td>Cartesian Closed Structure</td><td>98</td></tr></table>

<table><tr><td>5.2.3</td><td>Recursion</td><td>99</td></tr></table>

<table><tr><td>5.3</td><td>Interpretation of IA<sub>✓</sub></td><td>100</td></tr></table>

<table><tr><td>5.3.1</td><td>Interpretation of PCF<sub>✓</sub></td><td>100</td></tr></table>

<table><tr><td>5.3.2</td><td>Interpretation of State</td><td>102</td></tr></table>

<table><tr><td>5.3.3</td><td>Summary of Results</td><td>103</td></tr></table>

<table><tr><td>5.4</td><td>Conclusions and Historical Notes</td><td>103</td></tr></table>

II Thin Concurrent Games 104

6 Basic Concurrent Games 107

<table><tr><td>6.1</td><td>Games and Strategies as Event Structures</td><td>107</td></tr></table>

<table><tr><td>6.1.1</td><td>Basic Intuitions on Concurrent Strategies</td><td>107</td></tr></table>

<table><tr><td>6.1.2</td><td>Formalizing Concurrent Strategies</td><td>109</td></tr></table>

<table><tr><td>6.1.3</td><td>Basic Properties of Event Structures and Maps</td><td>113</td></tr></table>

<table><tr><td>6.2</td><td>Composition of Prestrategies</td><td>118</td></tr></table>

<table><tr><td>6.2.1</td><td>Interaction of prestrategies</td><td>119</td></tr></table>

<table><tr><td>6.2.2</td><td>Composition of prestrategies</td><td>127</td></tr></table>
<table><tbody><tr><td>6.2.3</td><td>The associator</td><td>129</td></tr><tr><td>6.3</td><td>Composition of Strategies</td><td>131</td></tr><tr><td>6.3.1</td><td>Composition of Strategies</td><td>131</td></tr><tr><td>6.3.2</td><td>Strategies and +-covered configurations</td><td>132</td></tr><tr><td>6.3.3</td><td>Composition and +-coveredness</td><td>133</td></tr><tr><td>6.4</td><td>The Bicategory CG</td><td>135</td></tr><tr><td>6.4.1</td><td>Copycat</td><td>135</td></tr><tr><td>6.4.2</td><td>Copycat and Strategies</td><td>137</td></tr><tr><td>6.4.3</td><td>Horizontal Composition and Bicategorical Structure</td><td>138</td></tr><tr><td>6.4.4</td><td>Characterization of Strategies</td><td>139</td></tr><tr><td>6.5</td><td>Conclusions and Historical Notes</td><td>140</td></tr><tr><td>7</td><td>Thin Concurrent Games</td><td>142</td></tr><tr><td>7.1</td><td>Symmetry in Games and Strategies</td><td>142</td></tr><tr><td>7.1.1</td><td>Event Structures with Symmetry</td><td>143</td></tr><tr><td>7.1.2</td><td>Saturated Games with Symmetry</td><td>146</td></tr><tr><td>7.1.3</td><td>Thin Concurrent Games</td><td>149</td></tr><tr><td>7.1.4</td><td>Constructions on Thin Concurrent Games</td><td>152</td></tr><tr><td>7.2</td><td>Mediating Between Strategies</td><td>155</td></tr><tr><td>7.2.1</td><td>A Zoology of Morphisms and Equivalences</td><td>155</td></tr><tr><td>7.2.2</td><td>A Study of Positive Morphisms</td><td>157</td></tr><tr><td>7.2.3</td><td>All Equivalences Coincide</td><td>160</td></tr><tr><td>7.2.4</td><td>Constructing Positive Morphisms</td><td>162</td></tr><tr><td>7.3</td><td>Composition and Copycat</td><td>164</td></tr><tr><td>7.3.1</td><td>Interactions with Symmetry</td><td>165</td></tr><tr><td>7.3.2</td><td>Composition with Symmetry</td><td>168</td></tr><tr><td>7.3.3</td><td>Copycat</td><td>171</td></tr><tr><td>7.4</td><td>The Bicategory TCG</td><td>174</td></tr><tr><td>7.4.1</td><td>Synchronization up to Symmetry</td><td>176</td></tr><tr><td>7.4.2</td><td>Horizontal Composition</td><td>179</td></tr><tr><td>7.4.3</td><td>Bicategorical Laws</td><td>181</td></tr><tr><td>7.4.4</td><td>A ~-category</td><td>185</td></tr><tr><td>7.5</td><td>History and Related Work</td><td>186</td></tr><tr><td>8</td><td>Constructing Games and Strategies</td><td>188</td></tr><tr><td>8.1</td><td>A Compact closed ~-Category</td><td>189</td></tr><tr><td>8.1.1</td><td>A bifunctor</td><td>189</td></tr><tr><td>8.1.2</td><td>Lifting Maps to Strategies</td><td>191</td></tr><tr><td>8.1.3</td><td>Compact Closed Structure</td><td>192</td></tr><tr><td>8.2</td><td>Negative Winning Games</td><td>194</td></tr><tr><td>8.2.1</td><td>Relative Seely categories</td><td>195</td></tr><tr><td>8.2.2</td><td>Playing Board Games</td><td>196</td></tr><tr><td>8.2.3</td><td>Negative Winning Strategies</td><td>201</td></tr><tr><td>8.2.4</td><td>Symmetric Monoidal Structure</td><td>202</td></tr><tr><td>8.2.5</td><td>Cartesian Product of Strict --Boards</td><td>204</td></tr><tr><td>8.2.6</td><td>Relative Closure</td><td>205</td></tr></tbody></table>
<table><tr><td>8.3</td><td>Non-Linear Structure</td><td>208</td></tr><tr><td>8.3.1</td><td>The Resource Modality</td><td>208</td></tr><tr><td>8.3.2</td><td>Recursion</td><td>215</td></tr><tr><td>8.4</td><td>History and Related Work</td><td>217</td></tr></table>

## III Disentangling Parallelism and State 219

### 9 The Causal Semantics of IA<sub>∥</sub> and its Unfolding 222

<table><tr><td>9.1</td><td>Interpretation of IA<sub>∥</sub></td><td>222</td></tr><tr><td>9.1.1</td><td>Interpretation of PCF<sub>∥</sub></td><td>222</td></tr><tr><td>9.1.2</td><td>Semantics of state</td><td>226</td></tr><tr><td>9.1.3</td><td>Discussion on the Interpretation</td><td>229</td></tr><tr><td>9.2</td><td>Unfolding Causal to Non-Alternating Strategies</td><td>233</td></tr><tr><td>9.2.1</td><td>A First Unfolding</td><td>233</td></tr><tr><td>9.2.2</td><td>Mixed Boards and Pointifixion</td><td>235</td></tr><tr><td>9.2.3</td><td>Unfoldings of a Causal Strategy</td><td>240</td></tr><tr><td>9.3</td><td>→-Strat and Full Abstraction</td><td>242</td></tr><tr><td>9.3.1</td><td>Unfolding the Categorical Structure</td><td>242</td></tr><tr><td>9.3.2</td><td>Unfolding the Interpretation of IA<sub>∥</sub></td><td>247</td></tr><tr><td>9.4</td><td>History and Related Work</td><td>248</td></tr></table>

### 10 Parallel Innocence 249

<table><tr><td>10.1</td><td>Defining Parallel Innocence</td><td>250</td></tr><tr><td>10.1.1</td><td>Causal Determinism</td><td>250</td></tr><tr><td>10.1.2</td><td>Pre-innocence</td><td>253</td></tr><tr><td>10.1.3</td><td>Visibility</td><td>254</td></tr><tr><td>10.2</td><td>Composition of Visibility</td><td>256</td></tr><tr><td>10.2.1</td><td>Justifiers in causal strategies</td><td>256</td></tr><tr><td>10.2.2</td><td>Justifiers in interactions</td><td>257</td></tr><tr><td>10.2.3</td><td>Views of gccs</td><td>257</td></tr><tr><td>10.2.4</td><td>The Relative Seely ~ Category NTCG-Vis</td><td>259</td></tr><tr><td>10.3</td><td>Composition of Innocence</td><td>259</td></tr><tr><td>10.3.1</td><td>The "forking lemma"</td><td>260</td></tr><tr><td>10.3.2</td><td>Stability of pre-innocence</td><td>261</td></tr><tr><td>10.3.3</td><td>The Relative Seely Category NTCG-Inn</td><td>262</td></tr><tr><td>10.3.4</td><td>Complement: the "Bang Lemma"</td><td>263</td></tr><tr><td>10.4</td><td>Relational Collapse</td><td>265</td></tr><tr><td>10.4.1</td><td>Stopping Positions and Witnesses</td><td>265</td></tr><tr><td>10.4.2</td><td>Composition and Deadlocks</td><td>267</td></tr><tr><td>10.4.3</td><td>The Deadlock-Free Lemma</td><td>269</td></tr><tr><td>10.4.4</td><td>A Relative Seely ~-Functor</td><td>273</td></tr><tr><td>10.5</td><td>Globularity</td><td>278</td></tr><tr><td>10.5.1</td><td>Motivation and Definition</td><td>278</td></tr><tr><td>10.5.2</td><td>Composition of Globularity</td><td>280</td></tr><tr><td>10.6</td><td>History and Related Work</td><td>281</td></tr></table>
<table><tbody><tr><td><strong>11 Sequentiality</strong></td><td><strong>282</strong></td></tr><tr><td>11.1 Sequentiality</td><td>283</td></tr><tr><td>11.1.1 Definition of Sequentiality</td><td>283</td></tr><tr><td>11.1.2 Categorical Structure</td><td>286</td></tr><tr><td>11.1.3 A Relative Seely ~-Category</td><td>290</td></tr><tr><td>11.1.4 -Seq and Interpretation of IA</td><td>291</td></tr><tr><td>11.2 The Alternating Unfolding</td><td>292</td></tr><tr><td>11.2.1 Alternating Unfolding on a Mixed Board</td><td>292</td></tr><tr><td>11.2.2 Alternating Unfoldings of Sequential Strategies</td><td>295</td></tr><tr><td>11.2.3 Unfolding the Basic Categorical Structure</td><td>297</td></tr><tr><td>11.2.4 Unfolding the Interpretation of IA</td><td>299</td></tr><tr><td>11.3 Sequential Innocence</td><td>301</td></tr><tr><td>11.3.1 Causal Analysis of Sequential Innocence</td><td>301</td></tr><tr><td>11.3.2 The Unfolding Preserves Innocence</td><td>304</td></tr><tr><td>11.3.3 Sequential Globularity</td><td>306</td></tr><tr><td>11.3.4 Intensional Full Abstraction</td><td>307</td></tr><tr><td>11.4 History and Related Work</td><td>308</td></tr><tr><td><strong>12 Finite Definability for PCF</strong></td><td><strong>309</strong></td></tr><tr><td>12.1 Meager Form</td><td>310</td></tr><tr><td>12.1.1 Updating Mixed Boards</td><td>311</td></tr><tr><td>12.1.2 Meager Innocent Strategies</td><td>313</td></tr><tr><td>12.1.3 The Meager Form of Sequential Globularity</td><td>321</td></tr><tr><td>12.1.4 Finite Tests Suffice</td><td>322</td></tr><tr><td>12.2 Factorization</td><td>323</td></tr><tr><td>12.2.1 The Flow Substrategy</td><td>324</td></tr><tr><td>12.2.2 The Argument Substrategies</td><td>326</td></tr><tr><td>12.2.3 Recomposition</td><td>330</td></tr><tr><td>12.3 Finite Definability and Full Abstraction</td><td>333</td></tr><tr><td>12.3.1 First-Order Definability</td><td>333</td></tr><tr><td>12.3.2 Positional First-Order Definability</td><td>334</td></tr><tr><td>12.3.3 Finite Globular Definability</td><td>337</td></tr><tr><td>12.3.4 Intensional Full Abstraction</td><td>338</td></tr><tr><td><strong>IV Other Developments and Openings</strong></td><td><strong>339</strong></td></tr><tr><td><strong>13 Further Work</strong></td><td><strong>341</strong></td></tr><tr><td>13.1 Effects and Concurrency</td><td>341</td></tr><tr><td>13.1.1 Non-canonical causal presentation</td><td>343</td></tr><tr><td>13.1.2 Non-angelic concurrent games</td><td>343</td></tr><tr><td>13.1.3 Resource-tracking concurrent games</td><td>345</td></tr><tr><td>13.2 Quantitative Concurrent Games</td><td>346</td></tr><tr><td>13.2.1 Probabilistic PCF</td><td>347</td></tr><tr><td>13.2.2 Quantum strategies</td><td>349</td></tr><tr><td>13.3 Quantitative Relational Collapses</td><td>352</td></tr></tbody></table>
<table><tbody><tr><td>13.3.1 Counting witnesses and quantitative collapse</td><td>352</td></tr><tr><td>13.3.2 Generalized species of structure</td><td>355</td></tr><tr><td>13.4 Game Semantics as Taylor Expansion</td><td>357</td></tr><tr><td>13.4.1 Pointer concurrent games and positional injectivity</td><td>357</td></tr><tr><td>13.4.2 Isogmentations and the resource calculus</td><td>359</td></tr><tr><td>13.4.3 Taylor expansion, extensional resource terms</td><td>360</td></tr><tr><td>13.5 Operational Concurrent Games</td><td>360</td></tr><tr><td>13.6 Miscellaneous</td><td>363</td></tr><tr><td>13.6.1 Full Abstraction for Parallel-Or</td><td>363</td></tr><tr><td>13.6.2 A Semantic Proof of Herbrand's Theorem</td><td>366</td></tr><tr><td>13.6.3 Revisiting Games Models of MALL</td><td>368</td></tr><tr><td><strong>14 Conclusions</strong></td><td><strong>370</strong></td></tr><tr><td>14.1 The Work Done so Far</td><td>370</td></tr><tr><td>14.2 Open Problems</td><td>371</td></tr><tr><td>14.2.1 Non-deterministic parallel innocence</td><td>371</td></tr><tr><td>14.2.2 Proper determinism</td><td>373</td></tr><tr><td>14.2.3 All well-bracketings</td><td>374</td></tr><tr><td>14.2.4 Observing causality</td><td>374</td></tr><tr><td>14.3 Perspectives and Future Directions</td><td>375</td></tr><tr><td><strong>V Appendices</strong></td><td><strong>393</strong></td></tr><tr><td><strong>A Complements on Relative Seely Categories</strong></td><td><strong>394</strong></td></tr><tr><td>A.1 Definition and Kleisli Category</td><td>395</td></tr><tr><td>A.2 Relative Seely Functors</td><td>396</td></tr></tbody></table>
# Preface

This document is my HDR – “Habilitation à Diriger les Recherches”. As such, its
principal aim is to motivate and present the heart of my research work so far.

Of course, I was not the only one in this adventure, this is the product of collaborations
with a number of people. Firstly with Glynn Winskel: I started working with Glynn
during my postdoc in Cambridge from September 2011 to September 2013, and our
collaboration kept going strong long after that. My work owes a lot to him; many results
presented here may not exist at all if not for his encouragements and insights.

Secondly, almost of my further work in this direction is collaborative, and was car-
ried out with PhD students. First with Simon Castellan (2014 – 2017), with whom we
constructed thin concurrent games and parallel innocence. This forms the core of the
material that I have chosen to present in this monograph, though I believe the presenta-
tion has since then significantly gained in maturity. Then, with Aurore Alcolei (2016 –
2019) and Marc de Visme (2017 – 2020). Though the work done with them will not be
covered therein, this document does greatly benefit from the intuitions gained with them
– their work will be mentioned in the outline of further work in Chapter 13. Finally, the
story currently continues with Lison Blondeau-Patissier (2021 – 2024).

No research is done in a vacuum and this work, as usual, stands on the shoulders of giants. First and foremost, the giants include the pioneers of game semantics: Martin Hyland and Luke Ong; Samson Abramsky, Radha Jagadeesan and Pasquale Malacaria; Hanno Nickau; and Thierry Coquand. Beyond those, the giants also include those who realized the strength of game semantics as a means to represent computational effects, for instance Guy McCusker, Jim Laird, Dan Ghica and Andrzej Murawski. And finally, the giants include those who kept deciphering the foundations of game semantics and maintained the sometimes thinning connection with linear logic: for instance, Pierre-Louis Curien, Laurent Regnier and Paul-André Melliès. The present work builds on their inheritance (and surely that of many others), and to an extent is a synthesis of their ideas. It is not at all obvious that such a synthesis was possible: it was first foreseen by Paul-André Melliès that this was possible, building on techniques from concurrency theory, and to a large extent this was the intent behind his line of work on asynchronous games. This line of work, which for simplicity (and although it can be slightly misleading) I will often refer to as concurrent games, inherits Paul-André's vision. Many of our technical steps parallels his, with the hindsight provided by 15 more years of work.
Beyond presenting this work, this document has two further objectives:

Firstly, I intend it as an entry point to my work on concurrent games. The technical underpinning of concurrent games is fairly elaborate: event structures are much more mathematically demanding than sequential structures (traces, trees, etc). The foundations are spread over a number of papers, written over the years. These papers rely on definitions and notations that are not quite consistent with each other, as our conceptual understanding progressed over time. In this manuscript, I present a complete and detailed construction of *Thin Concurrent Games*, a bicategory of concurrent strategies which plays a pivotal role in my further work – this is the purpose of Part II. I also present in Part III a detailed presentation of two developments at the core of the theory of Thin Concurrent Games, which I will introduce and motivate in Section 1.7.

Secondly, I needed an introduction to game semantics for programming languages, beyond merely concurrent games. In part, this is because I needed a precise set of definitions to refer to for the work presented in Part III. But beyond that, over the years I had come to dread the question “Where can I find a good introduction to game semantics”? While good introductory texts do exist, I felt that none gave a satisfactory answer. Indeed, many were written in the late 90s or earlier 00s and are not very modern or up-to-date. Others give a good survey, focusing on intuitions, but do not offer precise technical definitions; or they do offer a technical introduction, but to one particular technical setting, ignoring the wider picture. Hence, Part I is the result of my attempt at an accessible introduction to game semantics for programming languages.
# Chapter 1

# Introduction

Attempts to formally prove properties of the execution of programs (e.g functional correctness, safety, termination, etc) must rest on formal semantics turning the execution into a well-specified mathematical object. This is the main purpose of the field of semantics of programming languages, for which a reference textbook is [Winskel, 1993].

## 1.1 Operational Semantics

Typically, this is done via the methodology of **operational semantics**: by means of formal rules operating on syntax, showing how the source code is transformed throughout computation. For instance, assuming we have a value $\underline{n}$ for every $n \in \mathbb{N}$, the rules

$$ \frac{e_1 \rightsquigarrow e'_1}{e_1 + e_2 \rightsquigarrow e'_1 + e_2} \qquad \frac{e_2 \rightsquigarrow e'_2}{\underline{n} + e_2 \rightsquigarrow \underline{n} + e'_2} \qquad \frac{\underline{n} + \underline{m} \rightsquigarrow \underline{n} + \underline{m}}{\underline{n} + \underline{m} \rightsquigarrow \underline{n} + \underline{m}} $$

inductively define an evaluation relation $\rightsquigarrow$ between additive arithmetic expressions, specifying the operational behaviour of the sum: here, it has a left-to-right evaluation strategy: given a sum expression $e_1 + e_2$, we first evaluate $e_1$ to a value $\underline{n}$ – which may take many steps – then evaluate $e_2$ to a value $\underline{m}$. Once both operands are values, the expression $\underline{n} + \underline{m}$ is rewritten to $\underline{n} + \underline{m}$. For instance, we have the reduction sequence

$$ (2 + 3) + (7 + (1 + 2)) \rightsquigarrow 5 + (7 + (1 + 2)) \rightsquigarrow 5 + (7 + 3) \rightsquigarrow 5 + 10 \rightsquigarrow 15, $$

omitting the underlining. Each step above is justified by a derivation, e.g.

$$ \frac{\overline{1 + 2 \rightsquigarrow 3}}{\overline{7 + (1 + 2) \rightsquigarrow 7 + 3}} \qquad \frac{5 + (7 + (1 + 2)) \rightsquigarrow 5 + (7 + 3)}{5 + (7 + (1 + 2)) \rightsquigarrow 5 + (7 + 3)} $$
for the second step. This would be usually called a *small-step operational semantics*; *big-step semantics* also exist, where one axiomatises directly the evaluation relation $e \Downarrow \underline{n}$ of an expression to a value. More generally, there is a large body of literature studying variations of operational semantics; including a mathematical theory of operational semantics initiated by Turi and Plotkin [Turi and Plotkin, 1997].

Operational semantics is a powerful methodology for formal semantics of programming languages. It is very robust to the addition of syntactic constructs or programming features, and has proved capable of handling realistic programming languages. As it builds on simple inductive structures, it is amenable to mechanization in a proof assistant – as powerfully illustrated in the celebrated CompCert project by Leroy et al [Leroy, 2009, Krebbers et al., 2014]. However, operational semantics also has some drawbacks. By design, it is very much tied to syntax. More importantly, most frameworks are exclusively designed to reason on complete programs, operating in a closed world. They are ill-equipped to reason about *open* programs, that may include free variables or appeal to external libraries, and consequently are not compositional<fnref n="1" />.

## 1.2 Toward a Mathematical Semantics

Another approach to the formal semantics of programs is that of **denotational semantics**, initiated by Scott and Strachey under the name of *mathematical semantics* [Scott and Strachey, 1971]. Following the methodology of denotational semantics, any program *M* is sent to a mathematical object [[*M*]], its *meaning* or **denotation**. It is usually an invariant of evaluation, in the sense that if *M* $\rightsquigarrow$ *M*', then [[*M*]] = [[*M*']]. Thus a closed program of ground type is typically sent directly to the value it returns, if any, giving no insight on the evaluation process itself (at least explicitly). In contrast with operational semantics, denotational semantics focuses on *open programs*. To those it also gives a proper meaning, often as a function, as in the example below:

$$ \llbracket x + (x + 5) \rrbracket : \mathsf{N} \rightarrow \mathsf{N} \\ n \mapsto 2n + 5 $$

In contrast with operational semantics, compositionality is at the core of the methodology of denotational semantics. A denotation is assigned to each syntactic construct, and the denotation of the program is obtained by replacing modularly each piece of syntax by its denotation, as illustrated by the computation below:

$$ \begin{align*} \llbracket x + (x + 5) \rrbracket(n) &= \llbracket + \rrbracket(\llbracket x \rrbracket(n), \llbracket x + 5 \rrbracket(n)) \\ &= \llbracket + \rrbracket(n, \llbracket + \rrbracket(\llbracket x \rrbracket(n), \llbracket 5 \rrbracket(n))) \\ &= \llbracket + \rrbracket(n, \llbracket + \rrbracket(n, 5)) \\ &= \llbracket + \rrbracket(n, n + 5) \\ &= 2n + 5 \end{align*} $$

<footnote n="1">¹There are, of course, formalisms for compositional operational semantics, used for instance to make CompCert compositional [Stewart et al., 2015]. By and large, those put into play structures strongly related to denotational semantics; for instance [Stewart et al., 2015] acknowledge similarity with Ghica and Tzevelekos' *system-level game semantics* [Ghica and Tzevelekos, 2012].</footnote>
where $[+] : \mathbb{N}^2 \to \mathbb{N}$ is the usual arithmetical addition operation.

The traditional core of denotational semantics is *domain theory*, in which types are represented by certain posets satisfying completeness properties useful to represent in- finite data and partial computation, and open or higher-order programs are represented as (continuous) functions. But this traditional approach to denotational semantics has limitations, the focus on representing programs as functions being in tension with com- putational effects such as non-deterministic choice, probabilistic choice, references, ex- ceptions, etc (though many of those effects can be accommodated via adequate monads [Moggi, 1991]). The modern understanding of *denotational semantics* is often taken more generally to mean a compositional interpretation of programs, usually structured categorically (typically as a cartesian closed category [Lambek and Scott, 1988]). In this wider understanding, denotational semantics may be regarded as the art of reason- ing compositionally about program behaviour, which is of paramount importance for the purpose of having formal semantic techniques that scale [O'Hearn, 2015].

Over the years, a wealth of denotational models have appeared for programming lan- guages, according to which programs are represented as other structures than functions. For instance, in the *relational model* [Girard, 1988], we have

$$ \begin{align*} [[x + (x + 5)]] &\subseteq \mathcal{M}_f(\mathbb{N}) \times \mathbb{N} \\ &= \{([n, m], \quad n + m + 5) \mid n, m \in \mathbb{N}\} \end{align*} $$

where $\mathcal{M}_f(X)$ is the set of *finite multisets* of elements of $X$ – in this semantics, we record that we may obtain value $n + m + 5$ provided we have *two* successful evaluations of the argument, one yielding value $n$, the other yielding value $m$. In contrast to the functional models mentioned earlier, this one is *quantitative*: we see in the interpretation that the program makes *two* calls to its argument, an information lost in domain semantics.

We also account for the behaviour of the program against a potentially non-deterministic environment: for instance, while in functional semantics the program $x \text{ xor } x$ will return $\mathfrak{f}\mathfrak{f}$ for any value of $x$ (writing $\mathfrak{t}\mathfrak{t}$ and $\mathfrak{f}\mathfrak{f}$ the two boolean values), we have

$$ ([\mathfrak{t}\mathfrak{t}, \mathfrak{f}\mathfrak{f}], \mathfrak{t}\mathfrak{t}) \in [[x \text{ xor } x]] $$

in relational semantics, accounting for an execution of $x \text{ xor } x$ in the context of a non- deterministic $x$. Note that here, $[\mathfrak{t}\mathfrak{t}, \mathfrak{f}\mathfrak{f}] = [\mathfrak{f}\mathfrak{f}, \mathfrak{t}\mathfrak{t}]$. There is no sense in which an element of the multiset may be unambiguously assigned to an occurrence of $x$ – we do not know if the program returns $\mathfrak{t}\mathfrak{t}$ because the first $x$ returned $\mathfrak{t}\mathfrak{t}$ and the second $\mathfrak{f}\mathfrak{f}$, or the other way around. We can enrich the model to account for the fact that $([\mathfrak{t}\mathfrak{t}, \mathfrak{f}\mathfrak{f}], \mathfrak{t}\mathfrak{t})$ is realized by these *two* executions, by assigning a *weight* to every point of the relational model

$$ [[x \text{ xor } x]]([\mathfrak{t}\mathfrak{t}, \mathfrak{f}\mathfrak{f}], \mathfrak{t}\mathfrak{t}) = 2 $$

and obtain in this way a *weighted relational model* [Laird et al., 2013], in which two terms of PCF are sent to the same representation iff they cannot be distinguished by PCF with probabilistic choice [Ehrhard et al., 2018]!

But the above still forgets much about the program, for instance it tells us nothing about the behaviour of the program under a stateful execution environment. For that,
we must yet again move up in the intensionality ladder, into the realm of *game semantics* [Hyland and Ong, 2000, Abramsky et al., 2000], and record the behaviour of the program over time as illustrated in the diagram below

<figure><img src="image_5.png" /></figure>

breaking the symmetry between the two calls by explicitly showing them over time.

There are multiple ways to enrich denotational models with time, leading to many mathematical settings for game semantics: for instance, one can interpret a PCF program in Abramsky and McCusker's model [Abramsky and McCusker, 1996] which characterizes programs undistinguishable with ground state, in Berry and Curien's sequential algorithms which characterize indistinguishability in the presence of control operators [Cartwright et al., 1994], in Murawski's model for indistinguishability by state and control [Murawski, 2007], in Ghica and Murawski's model for indistinguishability by shared state and concurrency [Ghica and Murawski, 2008]. . . That is just the tip of the iceberg, and only listing game semantics models. Overall, a term of PCF can be interpreted into maybe a dozen different denotational models, sometimes similar and sometimes different, each recording a different aspect of its interactive behaviour<fnref n="2" />.

In our tour of denotational models we should certainly also mention bicategorical models such as *generalized species of structure* [Fiore et al., 2008] or *Melliès' template games* [Melliès, 2019a], which assign to each point of the interpretation of a type in the relational model a *set* (or a category) of witnesses, presenting the different executions realizing that point – so rather than merely stating $[[x \text{ xor } x]]([tt, ff], tt) = 2$, the interpretation would yield a particular two-element set. Finally, all these developments phrased explicitly as denotational models fit into a more general landscape of tools and methods to approximate program behaviour (including idempotent or non-idempotent intersection types, resource or differential calculi, the Taylor expansion of programs, etc). There is an impressive breadth here: denotational semantics go way beyond the somewhat boring formalization of the “intended” denotation of a term as an official mathematical function, it is in fact the quite varied art of extracting compositional information from programs, and of reasoning about program identity.

<footnote n="2">²Game semantics models, along with others such as Girard's *geometry of interaction* [Girard, 1989], are often collectively referred to as *interactive semantics*. But this might be a misnomer: in reality, all the above semantics are interactive semantics in the sense that they all collect information about the interactive or compositional behaviour of the program, as opposed to the mechanics of its evaluation.</footnote>
1.3 The Next 700 Denotational Semantics

It is fascinating that so many subtly different compositional accounts can be given, even if one considers only a single computational object such as PCF. What is also striking, is that there are comparatively surprisingly few results formally *relating* all these different models – even though many of those largely rely on similar intuitions, notably inherited from Linear Logic [Girard, 1987]. One explanation is that the community has focused more on building new models, taming new languages and effects, than on linking existing models. There is also a social aspect, individual researchers sticking with their favourite tools and methods. But besides those reasons, it remains true that such connections have in the past proved much more elusive than anticipated.

This is well-illustrated by the *relational collapse* of game semantics: we introduced above game semantics as relational semantics plus time, so it is only natural to attempt to send game semantics to the relational model by simply forgetting time:

<figure><img src="image_6.png" /></figure>

but this almost simple-minded idea hides two major conceptual hurdles: firstly, the traditional notion of plays in game semantics has time too wired in, and does not support an adequate notion of *position*. Secondly, composition of strategies also involves time; two interacting strategies may agree on a common position but not on a common *trajectory*, preventing synchronization. Understanding this prompted the work of many researchers, spanning over two decades [Baillot et al., 1997b, Melliès, 2005, Boudes, 2009, Calderon and McCusker, 2010, Clairambault and Paquet, 2021].

There are a few landmark results relating different models, such as Ehrhard's exten-
sional collapse theorem [Ehrhard, 2012], which links the qualitative and quantitative
views of resource replication. But by and large, a lot of seemingly simple questions
turn out to hide a surprising amount of conceptual and technical depth<fnref n="3" />.

Despite this relative rarity of actual formal connections, experts in the field do have
a strong intuition as to what all these models record, and where they intuitively stand in
relation to each other. After all, intuitively all those models are not independent: they
all refer to, and present a part of, the interactive behaviour of the program. Over time,
the working semanticist builds up an intuition of this full interactive behaviour, through
the lens of their favourite technical tools. This “full interactive behaviour” is, arguably,

<footnote n="3">³As a more recent example, generalized species of structure are often presented – as we did above – as refining the weighted relational model, replacing mere cardinality information by an explicit of witnesses. This suggests that the coefficients computed by the weighted relational model are simply the cardinal of the set of witnesses computed by generalized species; but that is simply not true! (see Section 13.3).</footnote>
the actual object of study of our field. In a scientific meeting on denotational semantics, there might be some talks about relational models, vectorial semantics, game semantics, Taylor expansion, categorical models, and others; but in essence, all these talks are about this common "full interactive behaviour". Yet the "full interactive behaviour" is not a formal object. It is intuitively there, but it seems that it can only be accessed indirectly through the various models – one cannot look at it in the eye.

But what if one could, at least to an extent? If nothing else, this would be a precious help in understanding rigorously how the models relate to each other, transporting results, etc. It would be a cornerstone of a unified theory of denotational semantics.

## 1.4 Full Abstraction and Intentional Intensionality

Of course, a model presenting the “full intensional behaviour” would be by nature extremely intensional<fnref n="4" />, and representing the intensional behaviour of programs has not been the historical focus of denotational semantics. Instead, the driving question has long been that of full abstraction: the problem of capturing observational equivalence.

Let us make things a bit more precise. Informally, two programs *M* and *N* in a fixed language *L* are **observationally equivalent** if their behaviour cannot be separated within *L*: there is no context *C*[*M*] – a program of *L* with a hole – such that, for instance, *C*[*M*] converges while *C*[*N*] diverges. In other words, within *L*, *M* and *N* are completely interchangeable. In that case, we write *M* ≃ *N*. In many ways, observational equivalence appears to be the “ideal” semantic equivalence between programs; with implications in both theory and practice (for instance, one could hope that an optimization pass in a compiler replaces a program with an optimized, but observationally equivalent, variant). But observational equivalence is hard to establish, due to the infinitary universal quantification on contexts. Accordingly, the driving question in denotational semantics has long been to seek characterizations of observational equivalence: an interpretation [−] is **fully abstract** when we have *M* ≃ *N* iff [*M*] = [*N*].

In the 90s, much research on denotational semantics was driven by the *full abstraction* problem, of building a fully abstract model for the purely functional language PCF. This was not a practical question, but rather a quest to understand higher-order sequentiality. As an extensional solution remained elusive, this prompted the development of *game semantics for PCF* [Hyland and Ong, 2000, Abramsky et al., 2000, Nickau, 1994]: rather than to find conditions for functions to be sequentially computable, the idea became to find conditions for certain sequential interactive processes called *strategies* to compute *functions*; in other words, to find conditions on strategies to represent the interactive behaviour of purely functional programs. In Hyland-Ong games [Hyland and Ong, 2000], two were necessary: *innocence* and *well-bracketing*. It is debatable whether this did solve the full abstraction problem for PCF<fnref n="5" />, but game semantics had a much better sur-

<footnote n="4">⁴Meaning, recording information about the dynamics of programs, which might not be observable by the execution environment – as opposed to the extensional behaviour, i.e. input/output.</footnote>

<footnote n="5">⁵Nowadays, it seems that the consensus is that it *did not*: the additional intensional behaviour carried by strategies is eliminated by an undecidable quotient. On the other hand, it appears that we cannot do better: there is no effectively presentable fully abstract model for PCF, because observational equivalence in PCF is</footnote>
prise in store: in the subsequent years, it quickly turned out that lifting *innocence* gave a model of PCF plus local references of ground type [Abramsky and McCusker, 1996, McCusker, 2003], lifting *well-bracketing* gave a model of PCF plus **call/cc**, while lifting both gave a model of PCF with those two effects combined [Murawski, 2007], all fully abstract and effectively presentable! In other words, we had *one single* semantic framework for all combinations of state and control, with each condition on strategies corresponding to (the absence of) a certain effect. This was not missed by the community, eventually acknowledged by the 2017 Alonzo Church Award for Outstanding Contributions to Logic and Computation awarded to the authors of the three full abstraction for PCF papers, with the following excerpt from the announcement<fnref n="6" />.

> "Game semantics has changed the landscape of programming language semantics by giving a unified view of the denotational universes of many different languages. This is a remarkable achievement that was not previously thought to be within reach."

To explain this success, we argue that what game semantics has stumbled upon here while seeking full abstraction for PCF, is a glimpse of this “full interactive behaviour” – *at least in a world where everything is sequential deterministic*. This made it possible to understand computational effects in terms of their induced intensional behaviour, and to present four fully abstract models, which could otherwise have appeared completely independent from each other, as four projections of this interactive behaviour.

Of course, game semantics did not stop at the sequential deterministic picture outlined above: there are also fully abstract models for non-deterministic programming languages [Harmer, 1999], probabilistic [Danos and Harmer, 2000] or concurrent languages [Laird, 2001b, Ghica and Murawski, 2008] among others; but they are defined by separate, seemingly incompatible sets of definitions, and they no longer fit in a unified framework as above. For instance the models for non-deterministic or probabilistic computation do not support a notion of *innocence* eliminating state; there is no clear path to a probabilistic extension of the game semantics of concurrent computation, etc.

So why do we get this appealing unified picture for sequential deterministic computation, only to lose it immediately after? Where does this come from?

## 1.5 Plays Considered Harmful

We argue that the limitation causing this is hidden in the very basic definition:

**Definition 1.5.1.** Consider A a game, inducing a set of moves $M_A$ and plays $P_A \subseteq M_A^*$.
A strategy on A is a non-empty, prefix-closed $\sigma \subseteq P_A$, subject to further conditions.

This seems natural: the interpretation of a type specifies the valid executions, the plays of the game; and $\sigma$ lists the paths that the strategy is prepared to take.

<footnote>undecidable even with finite basic datatypes and without recursion [Loader, 2001].</footnote>

<footnote n="6">⁶https://eatcs.org/index.php/component/content/article/1-news/2473-the-2017-alonzo-church-award</footnote>
But this choice of representation has a cost.

**Bounding Opponent's behaviour.** When setting up a game semantics, one must usu-
ally start by specifying the plays. Plays form the basic backbone of a game semantics –
strategies are formed out of plays, composition starts with operations on plays, etc.

This may not sound like much, but this choice of plays is perhaps *the* aspect that keeps the most game semantics settings apart and incompatible. Should plays be alternating? Or just locally alternating, as in AJM games? Should they be well-bracketed? Visi- ble? Or even innocent? Some developments carry easily from one choice to another, for instance, essentially the same well-bracketed innocent strategies can be defined on many of those options. But in general, this choice has heavy consequences: it essen- tially specifies the computational effect available to the ambient environment. Picking a notion of plays is picking a computational universe, it is choosing the *programming language* that the *rest of the world* is written in. If a program was interpreted in a model based on well-bracketed plays, we can say nothing about its execution against **call/cc**. If a program was interpreted in a model based on alternating plays, then we can say nothing about its execution in a concurrent environment.

Should we just adopt once and for all the most general available setting, say based on non-alternating plays? That may be appealing in principle, but many key constructions in game semantics (such as the notion of *P-view*) only make sense for restricted plays.

**Losing the branching structure.** A play describes a *single* interactive execution, in isolation from all the other ways in which history could have unfolded. A strategy is a set of such plays, with an induced tree structure, that may *branch*. If the first moves that differ are Opponent moves, this simply corresponds to different evaluation choices by the execution environment. In contrast, if the first moves that differ are Player moves, then this witnesses a non-deterministic choice by the program. For instance, the plays

<figure><img src="image_7.png" /></figure>

together inform a strategy **coin** : $\mathbb{B}$ implementing non-deterministic choice.

But the point where branches of the tree of plays separate is only the point where a
non-deterministic choice becomes observable, not necessarily where the choice actually
happens! For instance, the two terms (for $\cup$ a unit type with only one value)

$x : \cup \vdash \mathbf{if coin then} x; \mathbf{tt else} x; \mathbf{ff} : \mathbb{B}, \quad x : \cup \vdash x; \mathbf{coin} : \mathbb{B}$

allow exactly the same plays, which are all the prefixes of the one below:

<figure><img src="image_8.png" /></figure>
In reality, for the first program, at $q^+$ the coin has already landed and the result is already determined, but we cannot see that. This has a number of consequences: firstly, being unable to see the point of non-deterministic branching means that we are stuck with an *angelic* view of non-determinism, where **if coin then x else** $\perp$ is equivalent to $x$ and the possibility of divergence (with $\perp$ a looping primitive) is ignored$^7$.

Secondly, while this missing branching information turns out unnecessary to obtain a fully abstract model for a higher-order language with non-deterministic choice [Harmer and McCusker, 1999], this model no longer fits into a unified landscape as in the sequential deterministic case. In particular, attempting to ban state by a naive extension of *innocence* fails [Harmer, 2004]. Intuitively, *innocence* works by identifying a well-behaved fragment within the model that looks like syntax; but syntax *does* recall the branching information (as illustrated by the two terms above) while strategies as sets of plays cannot. There is no evident way to ban state in Harmer and McCusker's model [Harmer and McCusker, 1999] and obtain full abstraction for non-deterministic PCF; in this monograph we say that non-determinism and state are *entangled*.

While non-determinism is one possible branching structure, there are other “branching effects” that similarly change the very geometry of execution: two main examples are probabilistic choice and parallelism. As in the non-deterministic case, probabilistic choice and state are entangled in [Danos and Harmer, 2000], while parallelism and state are entangled in [Ghica and Murawski, 2008]; in either case there is no clear notion of innocence banning state while still allowing probabilistic choice and parallelism.

Prior to the line of work reported here, it had already appeared that adopting notions of strategies with explicit branching information, one could indeed obtain a notion of non-deterministic innocence which as desired captures a non-deterministic syntax [Castellan et al., 2014, Tsukada and Ong, 2015]. So it seems that extending the unified picture offered by game semantics beyond the sequential deterministic world is possible in principle, provided we replace plays with adequate mathematical objects giving a true account of various branching structures – we shall see later on that such a mathematical setting may be provided by *event structures* [Winskel, 1986].

**Losing positions.** Games are incredibly widespread beyond semantics; but on the surface their basic definitions often look rather different from Definition 1.5.1. Typically (say e.g. in *parity games* [Arnold and Niwiński, 2001] – or more generally, in games used in verification), a *game* is a graph of *positions*, which are split into *Player* and *Opponent* transitions. A *play* is a path in the graph starting in some initial position, and a *strategy* is a function that to any path ending in a Player position may associate a Player transition. A crucial notion is that of a *positional strategy*, whose behaviour does not depend on the whole play but only on the current position.

Curiously, this notion of *position* is missing from the very basic definitions of traditional game semantics, where instead the fundamental object is that of *plays*. While we

<footnote>$^7$Information about *must-convergence* can be retained by additionally recording *divergences*, as in [Harmer and McCusker, 1999] – but this does not extend to more elaborate resolutions of non-determinism, such as bisimulation or fair-testing equivalences.</footnote>
may *a posteriori* observe that the two plays

$$ \begin{array}{ccc} \mathbb{B} & \otimes & \mathbb{B} \\ \mathbf{q}^{-} \\ \mathbf{tt}^{+} & & \mathbf{q}^{-} \\ & & \mathbf{tt}^{+} \end{array} \qquad \begin{array}{ccc} \mathbb{B} & \otimes & \mathbb{B} \\ \mathbf{q}^{-} \\ \mathbf{tt}^{+} & & \mathbf{q}^{-} \\ & & \mathbf{tt}^{+} \end{array} \qquad (1.1) $$

reach the same *state*, i.e. the same set of moves where the two booleans have been evaluated and both have returned `tt`, the strategies used in semantics are typically not positional, and positional strategies are not stable under composition.

This is more than a peculiarity – at least if one hopes to link game semantics to other denotational models, since as hinted at in Section 1.3, positions are the key notion to establish a link with the relational model. Alternative, positional foundations for game semantics have existed for a while, such as the *graph games* of [Hyland and Schalk, 2002] and the *asynchronous games* of [Melliès, 2004a]. But by and large, they have not been developed beyond models of fragments of linear logic.

## 1.6 A Case for Causal Game Semantics

But if we are to remove plays, by what should they be replaced?

At first sight, *removing plays from game semantics* sounds a bit like removing malt from brewing, or removing wool from knitting. Of course committing to a notion of plays will constrain what you may do with them, but you have to live with that, after all plays *are* the basic material with which the game semanticist builds.

However, there is an alternative: *causal game semantics*. The developments presented in this monograph result from a paradigm shift: rather by presenting computational events in sequence, as they could be observed by a specific environment – however powerful it may be, we propose to organize them *causally*: one event appears before another only if this is imposed by a causal dependency, typically internal to the program.

**Recovering positions.** For instance, the pair `(tt, tt)` would be represented by:

<figure><img src="image_9.png" /></figure>

where below the first line that presents the two type components, we show the Hasse diagram of a *partial order*, read from top to bottom. In each type component, the program is prepared to return `tt`, under the unique cause that Opponent starts computation by playing `q⁻`. The comparison with the two diagrams of (1.1) is clear: we have removed *time* and the induced necessity of a choice for Opponent's scheduling. The diagram
only describes what actions the program is prepared to take, and under which conditions. The *positions* are easily accessible as certain down-closed (so *up-closed* in the diagram) sets of observable events; and we should see in the course of the monograph that this allows for a crisp link with relational semantics.

**Recovering the branching structure(s).** Adopting such partial orders allows us to record explicitly *parallel* branching information. The following diagram represents a strategy evaluating its free variables of unit type $\cup$ (admitting only one value) in parallel

$$x : \cup, y : \cup \vdash \cup$$

<figure><img src="image_10.png" /></figure>

where the branching on the second line with the two $q^+$ is *not* a non-deterministic choice (although it might lead to a non-deterministic choice if that parallelism is resolved by a scheduler), but a *parallel* branching: the events corresponding to the two threads for $x$ and $y$ are, as far as the intention of the program is concerned, *causally independent*.

A warning: this diagram does *not* mean that the program *enforces* the independence of $x$ and $y$, it does not mean that the evaluation of $x$ and $y$ will be independent once the context for $x$ and $y$ is known. It only means that the program does not itself impose causal constraints between the two threads. It is possible that the calls to $x$ and $y$ trigger the access to a shared resource, making them interfere. But this interference is then due to the interaction of the program with its environment, not to the program itself.

Much of concurrency theory is based on *interleavings*: an execution of two processes in parallel $P \parallel Q$ is formalized by considering all interleavings of executions of $P$ and $Q$, hence reducing concurrency to non-determinism by integrating the non-determinism from the scheduler. According to that interpretation, the program above looks non-deterministic as either $x$ or $y$ may be called first in a sequential execution. In contrast, for us (following the so-called *truly concurrent* approach to concurrency theory), this program is considered deterministic: all scheduling eventually reach the same state.

But if that is so, and if branching is parallelism, how can we express actual non-deterministic choice? We do so by adding a *conflict relation*, shown as a wiggly line

$$\mathcal{B} \\ q^{-} \rightarrow^{\mathcal{t}^{+}} \mathcal{f}^{+}$$

indicating that the two moves are *incompatible*, and cannot both occur in a single execution. Altogether, the partial order and the conflict relation form an *event structure* [Winskel, 1986], a well-established notion in concurrency theory.
**Lifting constraints on Opponent.** Those causal structures, which we call *concurrent strategies*, are developed in Part II. By design, concurrent strategies do not put *any* constraint on Opponent's behaviour: unlike all play-based game semantics, concurrent strategies do not record how a program is observed by a fixed environment, but only what observable actions the program is prepared to take, and under which conditions.

The purpose of concurrent games is to record very intensional information on the interactive behaviour of programs; information that is typically not observable, however strong the environment may be. In that, it is at odds with much of the earlier work on game semantics for programming languages, which focuses on obtaining full abstraction results and as such, on capturing the information about program behaviour that is observable by specific programming features. In adopting concurrent games, we exchange that for a crisp description of the *full interactive behaviour* of the programs from which all other denotational interpretations can, at least in principle, be obtained as certain projections – a claim that we shall aim to substantiate in this monograph.

Despite our overarching point about the necessity of capturing the full interactive behaviour, some will surely question the point of a semantics not designed to reason on observational equivalence, and recording interactive behaviour that is unobservable, even by a wildly powerful environment. To those, we oppose the following question: is it really reasonable to consider that a program may only interact with an environment written in a *single* programming language, with a fixed observational power? This “fixed world hypothesis”, followed in much of denotational semantics, is in tension with the heterogeneous and distributed nature of modern software. Like any denotational semantics, game semantics is by nature modular with respect to program construction. But the fixed world hypothesis makes it *less* modular in another direction, that of programming language extensions.

One also could wonder if history will remember the full abstraction results as the most important contribution of game semantics. Arguably, there are already signs that probably not. In the recent past, a few developments have been proposed by groups without prior knowledge and experience in game semantics, but leveraging ideas or techniques for game semantics [Stewart et al., 2015, Xia et al., 2020, Chappe et al., 2023, Koenig and Shao, 2020, Vale et al., 2023]. By and large they are motivated by the need for more compositional structures in program certification – they need game semantics for its compositional description of interactive execution, *not* its full abstraction results!

Thus it seems healthy to part with the “fixed world hypothesis” – but it would be better if that did not mean throwing away decades of work and developments in denotational semantics, and the myriad of results and techniques developed. This is, we claim, what concurrent games may eventually achieve, and this monograph contributes some steps.

## 1.7 Contributions and Outline

In our “concurrent games” line of work, quite a few developments fit into that general line; we survey a few of those at the end of this monograph, in Chapter 13. To form the heart of this document, we had to select a precious few contributions:
**Concurrent games.** In the published literature, the technical construction of our “concurrent games” framework spans quite a few papers. We first build on Rideau and Winskel’s original set of definitions for a bicategory where both games and strategies are event structures [Rideau and Winskel, 2011]. Our work is based on an extension of this bicategory with symmetry, a framework called *thin concurrent games*, that first appeared (without details and proofs) in a conference paper [Castellan et al., 2015] and then detailed in [Castellan et al., 2019], though depending on an earlier reconstruction of the basic bicategory of concurrent games in [Castellan et al., 2017a]. This makes the chain of dependencies of specific results and lemmas a bit challenging to track, especially given that the notations and terminology have matured over time.

Thus the first contribution of this monograph is a complete, self-contained and hopefully pedagogical presentation of thin concurrent games. It comprises a new presentation of the basic bicategory **CG** without symmetry, the central bicategory **TCG** of *thin concurrent games*; and the description of a number of additional constructions useful to define the interpretation of programming languages.

**Disentangling parallelism and state.** We use the above to give a causal version of one of the most expressive games models out there: Ghica and Murawski’s non-alternating games, fully abstract for *Idealized Concurrent Algol* – a concurrent higher-order language with (local) ground state references [Ghica and Murawski, 2008].

In fact, *ICA* may be regarded as PCF enriched with two programming features: *parallelism* adds the ability to perform computations in parallel, a priori with no interaction or side-channel communication; and *state* is given by ground state local references (and semaphores). We regard *concurrency* not as a primitive computing feature, but as a phenomenon emerging from the combination of parallelism and state. Hence rather than *ICA*, we call the language *Idealized Parallel Algol* (*IA*∥), i.e. Idealized Algol plus parallelism – but it is indeed a concurrent language.

Resting on **TCG** we construct **→-Strat**, a cartesian closed category in which we describe an interpretation of *IA*∥. On strategies in **→-Strat**, we introduce two conditions: *sequentiality*, and *globularity*, which induce two sub-cartesian closed categories **→-Glob** (supporting the interpretation of *parallelism*, but not *state*) and **→-Seq** (supporting the interpretation of *state*, but not *parallelism*), and a third sub-cartesian closed category **→-SeqGlob** (supporting the interpretation of PCF only) where the two conditions are required. We construct **interpretation-preserving functors**:

<table><tr><td>→-Strat</td><td>→</td><td>Ο-Strat</td><td>(Theorem 9.3.8)</td></tr><tr><td>→-Seq</td><td>→</td><td>↓↑-Strat</td><td>(Theorem 11.2.18)</td></tr><tr><td>→-SeqGlob</td><td>→</td><td>↓↑-InnWB</td><td>(Theorem 11.3.10)</td></tr></table>

where **Ο-Strat**, **↓↑-Strat** and **↓↑-InnWB** are the reference fully abstract models for *IA*∥, *IA* and PCF respectively, phrased in terms of traditional game semantics – so that **→-Strat**, **→-Seq** and **→-SeqGlob** are also fully abstract. Finally, we prove a new **finite definability result** for **→-Glob** with respect to PCF plus *parallelism*.

Altogether, these results **disentangle** parallelism and state, in the sense above.
**Relational collapse.** Setting up the tools required for this is quite the journey. A particularly significant step encountered along the way is that *visibility*, one of the constituents of *globularity*, ensures that the composition of strategies induces no deadlocks so that we have an **interpretation-preserving functor to the relational model** (Corollary 10.4.15) – a modern account of the link between game semantics with the relational model, in line with our motto of bridging denotational models.

**A uniform presentation of pointer games.** Of course, a challenge in constructing the interpretation-preserving functors above to traditional games models, is that they refer to models constructed in a number of different papers, working with different notations, definitions that differ in subtle but significant ways... To achieve our goals, it was necessary to first recast the various games models of interest, which we attempted to do in an introductive and pedagogical way.

**Outline.** In the next chapter, we introduce a few mathematical conventions and notations used throughout the monograph.

Part I contains our introduction to pointer games. It focuses on alternating pointer games, covering innocence, well-bracketing, the full abstraction results for PCF and Idealized Algol. Then, it also presents non-alternating pointer games and the fully abstract model for $IA_\llcorner$. We mention a few other topics along the way: e.g. the *semantic cube*, and the alternative approach to uniformity via *copy indices*.

Part II contains our detailed construction of concurrent games. We start with the basic bicategory **CG**, then add symmetry to obtain *thin concurrent games (TCG)*. Finally, we construct additional structure aiming for (essentially) a cartesian closed category, as required by the interpretation of (call-by-name) programming languages.

Part III contains all the developments required to disentangle parallelism and state. It contains the interpretation of $IA_\llcorner$, the developments of *sequentiality* and *globularity* along with all the proofs of stability under composition. It contains all our interpretation-preserving functors, including that to the relational model. Finally, it contains a proof of finite definability for globular strategies.

Part IV surveys other developments in concurrent games fitting in our general pattern of bridging denotational models; as well as perspectives and open problems.

Finally, Part V contains some appendices.
# Chapter 2

## General Preliminaries

In this first technical chapter, we introduce some preliminaries to the preliminaries: first, we fix some of the general notations and conventions used in this monograph. Then, we introduce our programming languages of interest. Finally, we will recall definitions for a few of the basic denotational semantics concepts used later on.

### 2.1 Mathematical Language

To start off, let us introduce a few notations that we will use throughout this monograph.

**Sets.** If $X$ is a set, then we write $P(X)$ for the **powerset** of $X$, i.e. the set comprising all subsets of $X$. If $X$ and $Y$ are sets, we write $X + Y$ for the **tagged disjoint union** of $X$ and $Y$, defined as $X + Y = \{(1, x) \mid x \in X\} \cup \{(2, y) \mid y \in Y\}$. We are careful to distinguish this with $X \uplus Y$ which is the usual set-theoretic union, when it is known or assumed to be disjoint – for instance, we may write $X + Y = \{1\} \times X \uplus \{2\} \times Y$.

**Sequences.** If $X$ is a set, then $X^*$ denotes the set of **words** or **finite sequences** of elements of $X$. We write $\varepsilon \in X^*$ for the empty sequence, and $\sqsubseteq$ denotes the **prefix ordering** on finite sequences.

**Functions.** If $X$ and $Y$ are sets, we write $f : X \to Y$ to mean that $f$ is a function from $X$ to $Y$ (if $X$ and $Y$ are understood from the context to be objects in a specific category $C$, this might mean that $f$ is a morphism of $C$ from $X$ to $Y$ instead). Likewise, we write $f : X \to Y$ to mean that $f$ is a partial function from $X$ to $Y$. In both cases, we write the application of $f$ to $x \in X$ as $f(x)$ or sometimes simply as $fx$. If $f : X \to Y$ is a bijection, we write $f : X \cong Y$.

**Categories.** We assume familiarity with the basic notions of category theory and categorical logic. We write **Set** for the category of sets and functions. If $C$ is a category, we
write $C_0$ for its set of objects; if $A$ and $B$ are objects of $C$, we write $C(A, B)$ for the set of morphisms from $A$ to $B$. If $f \in C(A, B)$ is an isomorphism, we write $f : A \cong B$. For an isomorphism in Set, we tend to prefer the term *bijection* and the notation $f : A \simeq B$, but use *isomorphism* and write $f : A \cong B$ in the presence of further structure – for instance if $A$ and $B$ are partial orders, and $f$ is an order-isomorphism.

We write $\mathbf{T}$ for the terminal object of $C$, if it exists. If $C$ is a cartesian category, then we write $A\&B$ for the cartesian product of $A$ and $B$. We write $\pi_A : A\&B \to A$ and $\pi_B : A\&B \to B$ for the two projections, and $\langle f, g \rangle : X \to A\&B$ for the pairing of $f : X \to A$ and $g : X \to B$. We will also use $n$-ary versions of these constructions.

If $C$ is cartesian closed, we write $A \Rightarrow B$ for the arrow object of $A$ and $B$ and $ev_{A,B} : (A \Rightarrow A)\&A \to B$ for the evaluation morphism. If $h : X \times A \to B$, we write $\Lambda(h) : X \to A \Rightarrow B$ for its currying.

**Common abbreviations.** We shall use the following abbreviations in the text: *iff* for “if and only if”, *lhs* for “left hand side”, *rhs* for “right hand side”, *s.t.* for “such that” and *w.r.t.* for “with respect to”.

## 2.2 $IA_\llcorner$ and its Fragments

The contributions of this monograph are not about a programming language in particular: we view them as methodological contributions in denotational semantics, that may apply, in principle, to a variety of languages – the past body of work on game semantics has indeed proved that the insights gained when studying programming features in a specific setting could, to a large extent, be transported to other settings (e.g. the notion of *innocence*, originally intended to ban state in a call-by-name language, turned out to apply just as well to ban state in a call-by-value language [Honda and Yoshida, 1999]).

But we do need to fix target programming languages to illustrate our game semantics contributions, and to serve as target for our technical developments. For that, we settled on *Idealized Parallel Algol (IA$\llcorner$)*, a call-by-name concurrent higher-order programming language with ground local references. The main reason we adopted $IA_\llcorner$ is because among the languages that are well-studied in game semantics, this is one of the most expressive. Removing parallelism and/or state allows one to recover languages that are *also* very well-studied, though the corresponding models do not fit in a uniform semantic picture. If we want to prove full abstraction for the different fragments of $IA_\llcorner$, it “suffices” to relate to the existing fully abstract models, saving us some work.

The core of $IA_\llcorner$ is PCF, the prototypal higher-order sequential language introduced by Plotkin [Plotkin, 1977]: a call-by-name simply-typed $\lambda$-calculus with booleans, natural numbers and their combiners, plus recursion. We consider two extensions of PCF: firstly, *Idealized Algol (IA)* is PCF extended with *shared state*, under the form of (mainly) ground type local references. Secondly, *Parallel PCF (PCF$_\llcorner$)* extends PCF with a primitive for pure parallel evaluation, without communication. $IA_\llcorner$, obtained by putting all these together, is rather complex: in particular it is a *concurrent* language, as the combination of parallelism and shared memory induce *racy behaviour*.
In the rest of this section, we introduce formally the syntax of IA<sub>//</sub> and its fragments. A disclaimer: IA<sub>//</sub> and its fragments are not claimed to be realistic or in any way faithful to actual programming languages; nor do we think that realistic programming languages should be inspired by IA<sub>//</sub>. It is a toy language, whose only purpose is to put together certain programming aspects in a controlled environment where they can be studied in isolation; like a physicist studying properties of matter in a vacuum. Likewise, the reader should not see this work as a "study of the semantics of IA<sub>//</sub>" or its fragments. Again, our contribution is semantic and methodological, IA<sub>//</sub> being merely a way to illustrate it and provide a target that is challenging but achievable.

### 2.2.1 Syntax of IA<sub>//</sub>

**Types.** The types of IA<sub>//</sub> are the following, highlighting types relative to state.

$$ A, B ::= \begin{array}{l} \mathbb{U} | \mathbb{B} | \mathbb{N} | A \to B \quad \text{PCF} \\ | \mathbb{V} | \mathbb{S} \quad +\text{state} \end{array} $$

Above, $\mathbb{U}$ is a unit type with only one value, and $\mathbb{B}$ and $\mathbb{N}$ are types for *booleans* and *natural numbers*. In the presence of state, $\mathbb{V}$ is a type for *references* storing natural numbers, while $\mathbb{S}$ is for *semaphores*. We refer to $\mathbb{U}$, $\mathbb{B}$ and $\mathbb{N}$ as *ground types*, and use $\mathbb{X}$, $\mathbb{Y}$ to range over those. Let us now give the term constructions and typing rules.

**Terms and typing.** We define the terms of the language directly via typing rules.

**Contexts** are lists $x_1 : A_1, \dots, x_n : A_n$. **Typing judgments** have form $\Gamma \vdash M : A$ with $\Gamma$ a context and $M$ a type. In addition to Figure 2.1, we consider present an exchange rule letting us permute the order of variable declarations in contexts. The eliminator rules for basic datatypes are restricted to eliminate only to ground types – general eliminators are defined as syntactic sugar: e.g. a conditional to $\mathbb{V}$ may be obtained as

$$ \frac{\Gamma \vdash M : \mathbb{B} \qquad \Gamma \vdash N_1 : \mathbb{V} \qquad \Gamma \vdash N_2 : \mathbb{V}}{\Gamma \vdash \mathbf{mkvar} (\lambda x. \mathbf{if} \ M (N_1 := x) (N_2 := x)) (\mathbf{if} \ M ! N_1 ! N_2) : \mathbb{V}} $$

The **bad variable** and **bad semaphore** constructs **mkvar** and **mksem** are a common occurrence in the game semantical literature. While a "good" reference is tied to a memory location, many game models also comprise so-called "bad variables" inhabiting $\mathbb{V}$ but not behaving as actual variables. Full abstraction results in the concerned games models [Abramsky and McCusker, 1996, Ghica and Murawski, 2008] require a corresponding syntactic construct **mkvar** allowing one to form bad variables by appending arbitrary read and write methods<fnref n="1" />. The same holds for semaphores.

<footnote n="1">¹A very nice result by McCusker is that in fact, the fully abstract games model for IA is also fully abstract without bad variables [McCusker, 2003]!</footnote>
<figure><img src="image_11.png" /><figcaption>Figure 2.1: Typing rules for IA<sub>//</sub></figcaption></figure>
### 2.2.2 Operational Semantics of IA$_{//}$

In this monograph, we shall not refer explicitly to the operational semantics for IA$_{//}$, as we will only interact with those through already established denotational models. However, for the sake of completeness, we include here the definition.

We refer to constants of ground type as **values**; we use $v$ to range over those, and $n, b$ or $c$ to range over values of respective types $\mathbb{N}, \mathbb{B}$ or $\mathbb{U}$. We give a small-step operational semantics, following [Ghica and Murawski, 2008]. We fix a countable set $\mathcal{L}$ of **memory locations**. A **store** is a partial map $s: \mathcal{L} \to \mathbb{N}$ with finite domain where $\mathbb{N}$ stands, overloading notations, for natural numbers. A **configuration** is a term together with a store, formally a pair $(M, s)$ where $s$ is a store with $dom(s) = \{\ell_1, \dots, \ell_n\}$ and $\Sigma \vdash M : A$ with $\Sigma = \{\ell_1 : \mathbb{V}, \dots, \ell_i : \mathbb{V}, \ell_{i+1} : \mathbb{S}, \dots, \ell_n : \mathbb{S}\}$.

Execution is formalized via reductions between configurations, with shape

$$ \langle M, s \rangle \rightsquigarrow \langle M', s' \rangle $$

where $dom(s) = dom(s')$; we write $\rightsquigarrow^*$ for the reflexive transitive closure. If $\vdash M : \mathbb{X}$, we write $M \Downarrow v$ if $\langle M, \emptyset \rangle \rightsquigarrow^* \langle v, \emptyset \rangle$ for some value $v$ or simply $M \Downarrow$ leaving $v$ implicit. We give in Figure 2.2 the reduction rules; separated in basic rules listing the basic cases, and the context rules specifying the next available redexes. For rules not interacting with the state, we omit the state component – it is simply left unchanged by stateless basic reductions, and propagated upwards by stateless context rules.

### 2.2.3 Expressiveness of IA$_{//}$

We shall illustrate the expressiveness of the language via its fragments.

**The core language: PCF.** Introduced in [Plotkin, 1977], PCF is the paradigmatic (call-by-name) language for higher-order recursive computation.

PCF is of course Turing-complete, and may be used to program any (higher-order) computable function. For instance, the Ackermann function may be defined with

$$ \mathcal{Y}(\lambda A^{\mathbb{N} \to \mathbb{N} \to \mathbb{N} \to \mathbb{N}} m^{\mathbb{N}}. \text{ if (iszero } n\text{) (succ } m\text{) (iter (A (pred } n\text{)) } m\text{)}) $$

with $iter = \lambda f^{\mathbb{N} \to \mathbb{N}} x^{\mathbb{N}}$. $\mathcal{Y}(\lambda I^{\mathbb{N} \to \mathbb{N}} n^{\mathbb{N}}. \text{ if (iszero } n\text{) } x (f (I (pred } n\text{)))}$; showing how we can use recursion on higher-order functions in PCF. We define additional combiners in PCF that will eventually be used in the monograph. First, there is a **divergence**

$$ \Gamma \vdash \perp_A : A $$

for any type $A$, defined as any looping program, for instance via $\perp_A = \mathcal{Y}_A(\lambda x^A. x)$. We also add syntactic sugar for an **equality test** for all ground types, with rule

$$ \frac{\Gamma \vdash M : \mathbb{X} \quad \Gamma \vdash N : \mathbb{X}}{\Gamma \vdash M =_X N : \mathbb{B}} $$
<figure><img src="image_12.png" /><figcaption>Figure 2.2: Operational semantics of IA$_{\parallel}$</figcaption></figure>
returning `tt` iff the two terms yield the same value. For $\mathcal{X} = \cup$ we may define $M =_{\cup} N$ simply as $M; N; tt$. Likewise, we set $M =_{\mathcal{B}} N$ as if $MN$ (if $N$ `ff` `tt$), and $\Gamma \vdash M =_{\mathcal{N}} N$ : $\mathcal{B}$ similarly, with the obvious recursive program.

Next we introduce a *-ary case construct branching on all values of ground types. If $V = \{v_1, \dots, v_n\}$ is a finite set of values of ground type $\mathcal{X}$, we set

$$
\begin{array}{l@{\qquad}l@{\qquad}l}
\textbf{case } M \textbf{ of} & v_1 \mapsto N_1 & \textbf{let } x = M \textbf{ in} \\
& v_2 \mapsto N_2 & \textbf{if } x =_\mathcal{X} v_1 \textbf{ then } N_1 \\
& \dots & \textbf{else if } x =_\mathcal{X} v_2 \textbf{ then } N_2 \\
& v_n \mapsto N_n & \dots \\
& & \textbf{else if } x =_\mathcal{X} v_n \textbf{ then } N_n \\
& & \textbf{else } \perp
\end{array}
$$

of type $\mathcal{Y}$ in context $\Gamma$ if $\Gamma \vdash M : \mathcal{X}$ and $\Gamma \vdash N_i : \mathcal{Y}$ for all $1 \le i \le n$.

This makes crucial use of the **let** construct, ensuring that *M* is evaluated only once.
Note that the historical presentation of PCF has no **let** construct; however including it
makes for a more complete language of study with some control over the evaluation
order, and also allows for a neater correspondence with the game semantics.

**Idealized Algol.** *Idealized Algol*, or IA for short, corresponds in Figure 2.1 to PCF + state. It is used in the game semantics community (starting with the seminal paper [Abramsky and McCusker, 1996]) as the (call-by-name) paradigmatic programming language with ground type references: one can store an integer (though nothing much would change if one could store other finite datatypes), but one cannot store a function, or a reference. IA subsumes PCF, so all the programs and syntactic sugar mentioned above may still be defined here. But IA also supports imperative programming, e.g.

$\lambda n^N$. **newref** *r* in
**newref** *i* in
$r$ := 1;
*i* := n;
**while** (**not** (**iszero** !*i*) ) **do**
$r$ := (!*i*) * (!*r*);
*i* := **pred** (!*i*);
**done**;
!*r*

where **while** *M* **do** *N* **done* is syntactic sugar for $\mathcal{Y}(\lambda x. \mathbf{if} \ M(N; x) \mathbf{skip})$; and **not** and the arithmetic operation $*$ are defined in the obvious way.

Beyond first-order imperative programming, IA supports a combination of higher-
order and state letting us write programs such as the following *strictness test*

$\lambda f \upharpoonright_{\cup} \cup$. **newref** *r* in *f* (*r* := 1);

**if** (**iszero** (!*r*)) **ff** **tt**

: (*U* --> *U*) --> *B*
relying **if** when applied to a constant function, and **it** if the function calls its argument.

Our presentation of IA differs from the historical one in two inessential ways. First, as for PCF the **let** construct is usually missing from IA. But our **let** evaluates only terms of ground type, which is definable<fnref n="2" /> in IA by letting **let x = M in N** be sugar for

$$ \mathbf{newref} r \mathbf{in} r := M; (\lambda x. N)(!r), $$

illustrating an important aspect of IA references: they store *values* and not *computations*, so an expression *r* := *M* must evaluate *M* fully before storing the value.

The second inessential difference is that our version of IA includes semaphores – which we need, because they are unavoidable to get full abstraction in the presence of parallelism also. For sequential IA, semaphores of course are definable via:

$$ \mathbf{newsem} s \mathbf{in} M = \mathbf{newref} s \mathbf{in} M $$

$$ \mathbf{grab} M = \mathbf{if} (\mathbf{iszero} !M) (M := 1) \perp $$

$$ \mathbf{release} M = \mathbf{if} (\mathbf{iszero} !M) \perp (M := 0), $$

which is fine only because IA is sequential: if a program attempts to grab a semaphore which is not free (or dually, to release a semaphore which is free), then computation will hang as there is no other thread to free the semaphore while the program waits.

**Parallel PCF.** *Parallel PCF*, or PCF<sub>∥</sub> for short, corresponds in Figure 2.1 to PCF + parallelism. To PCF it adds mere parallel computation. This is made official by the operational semantics of Figure 2.2, which will indeed evaluate both branches of a parallel let *in parallel*. But keep in mind that this parallelism is not observable as there is no primitive in PCF<sub>∥</sub> allowing one to observe the evaluation order. Because of that, giving denotational semantics to PCF<sub>∥</sub> in isolation is a fairly trivial endeavour: any denotational semantics for standard PCF will do, interpreting the parallel let as

$$ \mathbf{let} x_1 = M_1 \mathbf{in} (\mathbf{let} x_2 = M_2 \mathbf{in} N), $$

but in this monograph we do not wish one denotational semantics for each fragment of IA<sub>∥</sub>, we want all fragments to be interpreted in the *same* denotational universe!

**Idealized Parallel Algol.** *Idealized Parallel Algol*, or IA<sub>∥</sub> for short, corresponds in Figure 2.1 to PCF + parallelism + state. It is used in the game semantics community [Ghica and Murawski, 2008] as the (call-by-name) paradigmatic higher-order concurrent programming language with shared memory and semaphores.

To IA, our version of IA<sub>∥</sub> adds parallelism, under the form of

$$ \frac{\Gamma, x_1 : X, x_2 : X \vdash M : Y \quad \Gamma \vdash N_1 : X \quad \Gamma \vdash N_2 : X}{\Gamma \vdash \mathbf{let} \left( \begin{array}{l} x_1 = N_1 \\ x_2 = N_2 \end{array} \right) \mathbf{in} M : Y} $$

<footnote n="2">²Up to observational equivalent; interestingly the two do not have the same causal behaviour!</footnote>
a parallel let operation which evaluates $N_1$ and $N_2$ independently. We refer to this as *parallelism* and not *concurrency* because this **let** only adds parallel evaluation; in our view concurrency emerges from parallel computation plus shared resources.

The usual presentation of $IA_\llcorner$ instead has a parallel composition operator

$$ \frac{\Gamma \vdash M : \bigcup \quad \Gamma \vdash N : \bigcup \\ \qquad \Gamma \vdash M \parallel N : \bigcup}{} $$

which may be defined as syntactic sugar, via $M \parallel N = \text{let} \begin{array}{l} (x = M) \\ (y = N) \end{array}$ in skip.

In this work, we adopt the parallel let rather than merely parallel composition because we also consider parallelism without shared state; but without state $M \parallel N$ is not a relevant construction as $M, N$ produce no value and can only communicate with the ambient program via the shared memory. Again, this is not a significant change with respect to the usual formulation of $IA_\llcorner$, as the same behaviour may be obtained with

$$ \textbf{let} \begin{array}{l} (x_1 = N_1) \\ (x_2 = N_2) \end{array} \textbf{in} M = \textbf{newref} r_1, r_2 \textbf{in} (r_1 := N_1) \parallel (r_2 := N_2); \\ (\lambda x_1 x_2. M) (!r_1) (!r_2) $$

if $\parallel$ is primitive rather than the parallel let.

$IA_\llcorner$ is a very expressive language. The most impactful thing to notice is that the combination of parallelism and shared state make it non-deterministic: one can define

$$ \vdash \textbf{choice} = \textbf{newref} r \textbf{in let} \begin{array}{l} (x = (r := 1)) \\ (y = !r) \end{array} \textbf{in iszero} y : \mathbb{B} $$

exploiting a race in the memory to generate non-deterministic behaviour.

## 2.3 Generalities on Semantics

Finally, we include some reminders and settle on some terminology and notations regarding observational equivalence, and denotational semantics. In this section, we use $\mathcal{L}$ as the *ambient programming language* – it can refer to PCF, IA, PCF$\llcorner$, or $IA_\llcorner$.

**Observational equivalence.** A $\mathcal{L}$-context for the judgment $\Gamma \vdash A$ is a term $C[]$ of $\mathcal{L}$ with a hole written $[]$, such that for any $\Gamma \vdash M : A$ in $\mathcal{L}$, we have $\vdash C[M] : \bigcup$ obtained by the (non capture-avoiding) substitution of $[]$ with $M$.

Two terms $\Gamma \vdash M, N : A$ of $\mathcal{L}$ are $\mathcal{L}$-observationally equivalent iff

$$ M \cong_{\mathcal{L}} N \Leftrightarrow \text{ for all } C[] \text{ a } \mathcal{L}\text{-context for } \Gamma \vdash A, (C[M] \Downarrow \Leftrightarrow C[N] \Downarrow) $$

We omit $\mathcal{L}$ when it is clear from the context. Observational equivalence is usually regarded as the canonical equivalence on programs: $\mathcal{L}$-observationally equivalent programs are interchangeable as long as the evaluation context is in $\mathcal{L}$.
**Denotational semantics.** Observational equivalence is ultimately an *operational notion* of program identity; it rests on the evaluation relation $M \Downarrow$, itself defined via the operational semantics. An alternative to study program identity is given by *denotational semantics*, embedding programs in a syntax-independent mathematical universe.

Denotational semantics is usually formulated *categorically*: the language $\mathcal{L}$ is interpreted in a category $C$ equipped with sufficient structure. More precisely, a denotational semantics in $C$ consists in several components. First, there is an interpretation function

$$ [[-]] : \mathbf{Types} \to C_0 $$

for *types* – this usually exploits the categorical structure, with e.g. $[[A \to B]] = [[A]] \Rightarrow [[B]]$ resting on a cartesian closed structure. This interpretation is extended to

$$ [[-]] : \mathbf{Contexts} \to C_0 $$

an interpretation of contexts, defined simply via $[[\Gamma]] = \mathcal{L}_{(x_i:A_i)\in\Gamma}[[A_i]]$. Now, we have

$$ [[-]] : \mathbf{Terms}(\Gamma \vdash A) \to C([\Gamma], [A]) $$

the interpretation of terms, defined by structural induction on the typing rules of $\mathcal{L}$ – for the simply-typed $\lambda$-calculus this interpretation typically follows a cartesian closed structure on $C$, while the primitives of $\mathcal{L}$ (e.g. natural numbers, booleans, manipulations of state, etc) are interpreted by well-chosen morphisms in $C$. By a **denotational model** of $\mathcal{L}$, we mean a category $C$ along with the interpretation function $[[–]]$ – sometimes focusing on $C$ and leaving the latter implicit.

In this monograph, we assume the reader is familiar with basic categorical logic, including the interpretation of the simply-typed $\lambda$-calculus in a cartesian closed category. For details, the reader is referred to [Lambek and Scott, 1988].

**Adequacy and full abstraction.** A denotational model should reflect the operational evaluation. We say that an interpretation in a model $C$ is **computationally adequate**, or simply *adequate* for short, if for all $\vdash M : \mathcal{X}$ a closed term of ground type,

$$ M \Downarrow v \Leftrightarrow [[M]] = [[v]], $$

i.e. the denotational model faithfully predicts the evaluation of a program to a value. For general reasons, an adequate model is automatically *sound* with respect to observational equivalence, i.e. if $[[M]] = [[N]]$ then $M \cong_L N$; it is **fully abstract** if the converse also holds: if $M \cong_L N$ then we actually have $[[M]] = [[N]]$.

**Intensional full abstraction.** Given a denotational model $C$, we may replay in $C$ the syntactic definition of observational equivalence: we fix an object for observations, typically $[[U]]$ (still written $\cup$ to alleviate notations). An *observation* on $A$ is then any

$$ \alpha \in C(A, \cup) $$
playing the role of $\mathcal{L}$-contexts: $f, g \in C(A, B)$ are **observationally equivalent** iff<fnref n="3" />

$$f \approx_C g \Leftrightarrow \text{ for all } \alpha \in C(A \Rightarrow B, \cup), \alpha \circ f = \alpha \circ g$$

like syntactic observational equivalence. Quotienting $C$ by this yields a new model, and $C$ is **intensionally fully abstract** when this quotiented model is fully abstract.

The term “intensional full abstraction” was originally proposed by Abramsky, Jageesan and Malacaria [Abramsky et al., 2000] to better describe the “full abstraction” results for PCF. Intensional full abstraction is *not* full abstraction: it is full abstraction of the quotiented model, but this quotiented model is usually not very useful as it is obtained non-constructively – in particular, a model constructed in this way rarely helps directly in reasoning on observation equivalence.

In contrast, *intensional full abstraction* keeps the focus on the model pre-quotient (which, at least in the case of game semantics, turned out to be more important). There we understand it as meaning that the “intensional behaviour” of morphisms of $C$ captures that of $\mathcal{L}$, or at least is sufficiently close that the morphisms of $C$ have the *same distinguishing power* as contexts of $\mathcal{L}$ through the interpretation – there is no “abstraction leaks”. Interestingly, it is in that sense that the term “full abstraction” is often understood in compilation – see e.g. [New et al., 2016].

In this monograph, we try to be careful in distinguishing *full abstraction* from *intensional full abstraction*, though we might occasionally slip and omit *intensional*.

<footnote n="3">³This definition is adequate when $C(T, \cup)$ has only two elements, for convergence and divergence. In some settings such as in concurrent games, this must be adapted to match syntactic observational equivalence.</footnote>
# Part I

## Pointer Game Semantics
# Introduction to Part I

<figure><img src="image_13.png" /><figcaption>Figure 2.3: As a low-pressure system moves in from the west, we can expect widespread pointer showers to develop by Chapter 3, and these showers are likely to continue on and off throughout Part I.</figcaption></figure>
The first part of this monograph is an introduction to “pointer game semantics”, a phrasing intended to include both the traditional (sequential deterministic) Hyland-Ong games [Hyland and Ong, 2000], and the non-alternating games by Ghica and Muraski [Ghica and Murawski, 2008], which of course have much in common with the former.

There are two pedagogical difficulties when learning game semantics. The first is coming up with an intuition as to what *plays* and *strategies* represent in relation with the interactive behaviour of the program – the operational meaning of well-bracketing, innocence, *etc*. Understanding this is not enough to *work* with game semantics, but it suffices to see the scientific value and role of game semantics. The second difficulty is understanding the denotational machinery: the composition of strategies, the cartesian closed structure, *etc*. We organized our introduction to pointer games addressing these two difficulties separately, so that a reader wanting to get the *point* of game semantics without mastering the combinatorics of the categorical structure can do so.

Accordingly, Chapter 3 introduces pointer games and its main notions and achievements, independently of the mechanics of the interpretation of programs. The content *is* technical and mathematically precise, but omits the definition of the interpretation and the corresponding categorical structure. The chapter starts by introducing the basic intuitions behind game semantics, at first without committing to any particular technical setting, then motivates and introduces the main concepts of pointer games: *arenas*, *plays with pointers*, *strategies*, *etc*; resting on operational intuitions. Still relying on operational intuitions, we show how certain patterns in plays witness the use of computational effects such as state or control, and use this to motivate the notions of well-bracketing and innocence, and showcase the associated full abstraction results. Finally, we mention an alternative to pointers, *copy indices*, as in AJM games [Abramsky et al., 2000].

Then, Chapter 4 addresses the denotational interpretation of programs. We define the composition of strategies, constructing a cartesian closed category $\downarrow\uparrow$-Strat. We define the interpretation of IA in $\downarrow\uparrow$-Strat, and wrap up with a few complements.

Finally, Chapter 5 introduces non-alternating pointer games in the sense of Ghica and Murawski [Ghica and Murawski, 2008]. The exposition roughly following the pattern of the previous two chapters: first we define non-alternating strategies and illustrate how they capture the interactive behaviour of programs of IA$_{\emptyset}$; then we build the corresponding cartesian closed category $\mathcal{O}$-Strat, and define the interpretation of IA$_{\emptyset}$.
# Chapter 3

## First Steps in Game Semantics

In this first chapter, we give an introduction to game semantics – focusing in particular on so-called HO or *Hyland-Ong* games<fnref n="1" /> [Hyland and Ong, 2000] presenting a selection of developments and landmark historical results. The presentation is technical, in that we give mathematically precise definitions and statements. However, we focus on operational intuitions, (temporarily) remaining elusive on the main source of complexity in game semantics: the categorical structure and denotational definition of the interpretation of programs. This, in turn, shall be the topic of Chapter 4 – so altogether, Chapters 3 and 4 give an introduction to sequential alternating game semantics.

Of course, as an introduction to game semantics, this presentation is far from complete. Many developments in game semantics do not fit in the framework presented here; we also focus on semantics of programming languages and essentially omit the works on logics and proof systems, on the other side of the Curry-Howard correspondence.

### 3.1 Executions, Plays, and Strategies

This section aims to convey some intuitions, and to motivate and gradually put into place our choices of mathematical formalizations for the basic ingredients of game semantics.

#### 3.1.1 Dialogues, Plays, and Simple Games

Game Semantics is designed as a way to give a clean mathematical description of the behaviour of *open* programs, as a back-and-forth interaction with an unspecified execution environment. More precisely, a program is interpreted as an aggregate of all

<footnote n="1">¹Those are often called Hyland-Ong/Nickau or *HON* games, also acknowledging Nickau, who came up independently with a model of PCF [Nickau, 1994] that is essentially the same as Hyland and Ong's. That is fair, but then one should also acknowledge the work of Coquand, who also proposed independently definitions having much in common with those [Coquand, 1995] (though not for PCF). Rather than the cumbersome *HONC* games, we prefer to stick with *HO* games, which is well-recognized in the community and refers to the specific set of technical definitions introduced by Hyland and Ong.</footnote>
$$x : \mathbb{N}, y : \mathbb{N} \vdash \mathbb{N} \\ q^{-}$$

$$q^{+}$$

$$q^{+}$$

$$42^{+}$$

$$f : \mathbb{N} \to \mathbb{N}, x : \mathbb{N} \vdash \mathbb{N} \\ q^{-}$$

$$q^{+}$$

$$q^{-}$$

$$q^{+}$$

$$50^{-}$$

$$50^{+}$$

$$42^{-}$$

$$42^{+}$$

$$x : \mathbb{N} \vdash \mathbb{N} \\ q^{-}$$

$$q^{+}$$

$$12^{-}$$

$$q^{+}$$

$$30^{-}$$

$$42^{+}$$

<caption>Figure 3.1: First-order</caption>

<caption>Figure 3.2: Higher-order</caption>

<caption>Figure 3.3: Repetition</caption>

its possible interactive behaviour with an execution environment. This is formalized as a two-player game between **Player** – which plays for the program under scrutiny; and **Opponent** – which plays the execution environment. Execution unfolds as those two players exchange *moves*, each of which represents an observable computational event.

**First-order.** As a first example, let us consider the following open PCF program:

$$x : \mathbb{N}, y : \mathbb{N} \vdash x + y : \mathbb{N}$$

For the sake of this discussion, we assume that the addition is computed on a left-to-right basis. From the point of view of standard operational semantics, there is no computation to perform here: the program is in normal form. Game semantics start where usual operational semantics stop, by asking the environment the value of x. One may then imagine a dialogue between the program and its environment, as follows:

**O** : "What is the value of x + y?"

**P** : "Evaluation is stuck: what is the value of x?"

**O** : "The value of x is 12."

**P** : "Evaluation is stuck: what is the value of y?"

**O** : "The value of y is 30."

**P** : "The value of x + y is 42."

In game semantics, such a sequence is called a **play**, and is typically drawn in a diagram as in Figure 3.1. By convention, we assign to Player the positive polarity +, and to Opponent the negative polarity -. In this diagram and all game semantics diagrams to come, we label moves with their polarity. The flow of time is from top to bottom, and each column corresponds to a component of the interface of the program with its environment. Variable calls are represented with the symbol **q** which stands for "Questions". All other moves correspond to returns, and are called "Answers".
This dialogue is one possible interaction between our program of interest and an execution environment; there are countably many of those, for each values for x and y. Such interactions only display the events observable by the environment: the program (x + 0) + y has exactly the same plays as x + y, the internal computation is ignored.

**Higher-order.** Let us now consider another example:

$$f : \mathbb{N} \to \mathbb{N}, x : \mathbb{N} \vdash f(x) : \mathbb{N}$$

One could expect Player to first prompt the environment for an actual function f from integers to integers. It is a central feature of game semantics that we instead have:

* **O**: “What is the value of $f(x)$?”

* **P**: “Evaluation is stuck: what is the output value of $f$?”

* **O**: “What is the input value of $f$?”

* **P**: “Evaluation is stuck: what is the value of $x$?”

* **O**: “The value of $x$ is 50.”

* **P**: “The input value of $f$ is 50.”

* **O**: “The output value of $f$ is 42.”

* **P**: “The value of $f(x)$ is 42.”

which, in the usual style of game semantics, would appear as in Figure 3.2: we interact with f in a lazy fashion, never fully grasping the infinite object behind. In this way, game semantics reduces higher-order evaluation to an exchange of first-order tokens.

**Simple games.** But what are, formally, the plays of Figures 3.1 and 3.2?

In traditional game semantics, each type (or typing judgment) yields by interpretation a **game** whose rules describe the valid open executions on the interface given by that type. Exact formalizations vary wildly in the literature and we will see several of those in this monograph; as a stepping stone we first present what must be the simplest notion of game considered in the game semantics literature, **simple games** [Hyland, 1997]:

**Definition 3.1.1.** A simple game comprises $A = (|A|, \text{pol}_A, P_A)$ with $|A|$ a set of moves, $\text{pol}_A : |A| \to \{-, +\}$ a polarity function, and $P_A \subseteq |A|^*$ a set of plays such that:

non-empty: $\varepsilon \in P_A$,

prefix-closed: for all $s \in P_A$, for all $s' \subseteq s$, we have $s' \in P_A$,

alternating: for all $s = s_1 \dots s_n$, for all $1 \le i \le n-1$, $\text{pol}_A(s_i) \ne \text{pol}_A(s_{i+1})$,

negative: for all $s = s_1 \dots s_n$, if $n \ge 1$ then $\text{pol}_A(s_1) = -$.

For instance, a game $\mathbb{B}$ for the booleans would have $|\mathbb{B}| = \{\mathbf{q}, \mathbf{t}, \mathbf{f}\}$, with $\text{pol}_{\mathbb{B}}(\mathbf{q}) = -$, $\text{pol}_{\mathbb{B}}(\mathbf{t}) = \text{pol}_{\mathbb{B}}(\mathbf{f}) = +$, and $P_{\mathbb{B}} = \{\varepsilon, \mathbf{q}, \mathbf{q}\mathbf{t}, \mathbf{q}\mathbf{f}\}$. As above, we shall often write moves with their polarities, as in $|\mathbb{B}| = \{\mathbf{q}^{-}, \mathbf{t}^{+}, \mathbf{f}^{+}\}$ and $P_{\mathbb{B}} = \{\varepsilon, \mathbf{q}^{-}, \mathbf{q}^{-}\mathbf{t}^{+}, \mathbf{q}^{-}\mathbf{f}^{+}\}$. However do keep in mind that this is merely for convenience: polarities are given by $\text{pol}_A$, and not intrinsic to moves, i.e. to the elements of $|A|$.

A program $M : A$ is then interpreted as a *strategy for Player* on the game for $A$:
**Definition 3.1.2.** A strategy $\sigma$: A on simple game A is a subset $\sigma \subseteq P_A$ satisfying:

non-empty: $\varepsilon \in \sigma$,

prefix-closed: for all $s \in \sigma$, if $s' \sqsubseteq s$, then $s' \in \sigma$,

receptive: for all $s \in \sigma$, if $sa^- \in P_A$, then $sa^- \in \sigma$,

deterministic: for all $sa_1^+, sa_2^+ \in \sigma$, we have $a_1 = a_2$.

A strategy aggregates all executions that the program is prepared to make against any execution environment; prescribing, in each state, the next observable action. When presented an Opponent-ending play $sa^- \in P_A$, a strategy $\sigma$: A checks whether $sa^-$ appears in $\sigma$; and if so, if there is some extension $sa^-b^+$. If that is the case, $\sigma$ plays $b^+$. For instance, the strategy for the constant $tt$ would be given by the set:

$$ \{\varepsilon, q^-, q^-tt^+\} : \mathbb{B}. $$

Simple games are appealing; they seem to capture exactly the intuitions so far, without useless mathematical arabesque. But their expressiveness is limited in various ways, making them seldom used in game semantics. We review next a major constraint, playing a central role in the design of essentially all game semantics formalisms.

### 3.1.2 Replication and Thread Indexing

We consider the term $x: N \vdash x + x: N$; whose game semantics admits:

O : "What is the value of $x+x$?"

P : "Evaluation is stuck: what is the value of $x$?"

O : "The value of $x$ is 12."

P : "Evaluation is stuck: what is the value of $x$?"

O : "The value of $x$ is 30."

P : "The value of $x+x$ is 42."

drawn in game semantics style in Figure 3.3. This illustrates an important aspect of game semantics: it is *quantitative*, in that it replays separately each variable call. This may seem redundant but it is not: if the execution environment is non-deterministic or has access to state, then the two calls to $x$ may obtain different values.

This does, however, ask the question of how this repetition is managed. Of course, the definition of simple games does not forbid simply repeating the same move. For instance, one could redefine the simple game for booleans as having the same set of moves and polarities as above, but plays given by the recursive definition:

$$ P_{\mathbb{B}} ::= \varepsilon \mid q^{-} \mid q^{-}tt^{+}P_{\mathbb{B}} \mid q^{-}ff^{+}P_{\mathbb{B}}, $$

but this idea quickly fails as we climb the type-theoretic ladder. Consider the term:

$$ f : \mathbb{B} \to \mathbb{B} \to \mathbb{B} \vdash f (f \tt ff) \tt : \mathbb{B} $$

and the play in Figure 3.4. On the right, we illustrate each position with an indicative, informal description of the corresponding operational state. Intuitively, Opponent
<figure><img src="image_14.png" /><figcaption>Figure 3.4: Ambiguity without thread-indexing</figcaption></figure>

moves are requests to evaluate a certain subterm; so at Opponent moves we highlight the subterm currently being evaluated. Likewise, Player questions correspond to variable calls; so at Player moves we underline the corresponding variable occurrence.

On the first line, the initial Opponent move $q^-$ prompts the evaluation of the whole term – so the whole term $f(f \tt ff) \tt$ is highlighted. In call-by-name, this prompts a Player question $q^+$ corresponding to requesting an output for the first occurrence of $f$, which is therefore underlined in the second line. In our example, Opponent then plays $q^-$ in the column corresponding to the first argument of $f$ – so the first occurrence of $f$ requests an evaluation of its first argument, highlighted in the third line. Yet again, the highlighted sub-term starts with an occurrence of $f$, so the next Player move, on the fourth line, is a move $q^+$ asking an output for $f$, seemingly identical to the move on the second line – but the variable occurrence underlined is not the same.

Now, in our example, the next move is an Opponent move corresponding to $f$ calling its *second* argument. But which occurrence of $f$? We have seen two of those, on the second and fourth lines! As this last $q^-$ reacts to the $q^+$ in the fourth line, it is natural to expect that it refers to it so that the operational state is $f(f \tt ff) \tt$. But in a sufficiently expressive language, it is also possible to find an environment in which the Opponent asks to evaluate the *first* occurrence of $f$, i.e. in which case the operational state is $f(f \tt ff) \tt!$ Because there are two copies of the move $q^+$ calling to $f$, Opponent has, intuitively, two available copies of the move $q^-$ requesting the evaluation of the second argument of $f$; and without further structure, we cannot disambiguate<fnref n="2" />.

The literature proposes two ways to solve this: *pointers*, or *copy indices*.

### 3.1.3 Pointer Games

The most widely used solution to this problem, used in particular in Hyland-Ong games [Hyland and Ong, 2000], is to enrich plays with *pointers* providing exactly the missing information. For instance, we show in Figure 3.5 two *plays with pointers* disambiguating

<footnote n="2">²To be precise, the usual arrow construction of simple games [Hyland, 1997] enforces a property called *local alternation* that only allows one of these options. But the phenomenon does occur at third-order, or in game semantics not enforcing local alternation such as that for higher-order state [Abramsky et al., 1998].</footnote>
<figure><img src="image_15.png" /><figcaption>Figure 3.5: Two plays with pointers disambiguating Figure 3.4.</figcaption></figure>

ing Figure 3.4. On the left hand side, Player is next to play $\mathbf{ff}^+$ while on the right hand side, Player is to play $\mathbf{tt}^+$. Pointers provide the missing *thread indexing*.

Adding pointers to plays require reworking the notion of game, which must now specify which pointers are allowed. This is achieved by switching to *arenas*:

**Definition 3.1.3.** An arena comprises $A = (|A|, \text{pol}_A, \le_A)$ with $|A|$ a countable set of moves, $\text{pol}_A : |A| \to \{-,+\}$ a polarity function, $\le_A$ a causality partial order, s.t.:

forestial: for all $a_1, a_2, a \in |A|$, if $a_1, a_2 \le_A a$, then $a_1 \le_A a_2$ or $a_2 \le_A a_1$,

well-founded: there is no infinite descending $a_1 >_A a_2 >_A a_3 >_A \dots$,

negative: if $a \in |A|$ is minimal for $\le_A$, then $\text{pol}_A(a) = -$,

alternating: for all $a_1, a_2 \in |A|$, if $a_1 \to_A a_2$, then $\text{pol}_A(a_1) \neq \text{pol}_A(a_2)$,

where $a_1 \to_A a_2$ means $a_1 <_A a_2$ and $a_1 \le_A a \le_A a_2$ implies $a = a_1$ or $a = a_2$.

This shall be completed (with Question/Answer labelling) in Definition 3.2.4.

We call $\to_A$ the **immediate causality** relation on $A$. Historically it has been written $\vdash_A$ in Hyland-Ong games, and called the *enabling relation* [Hyland and Ong, 2000]; but in this monograph we prefer to consider the partial order $\le_A$ as primitive.

The arena for the typing judgment $f : \mathbb{B} \to \mathbb{B} \to \mathbb{B} \vdash \mathbb{B}$ appears in Figure 3.6. We have annotated the type to highlight the correspondence between components of the arena and ground type occurrences. Usually these annotations are not present in diagrams for arenas or plays, but the same information is conveyed by displaying the type, and placing each move under the corresponding type component.

Both simple games and arenas are forests; but should be read differently: while in simple games an execution amounts to exploring a branch of the forest, an arena simply presents the set of observable computational events along with their hierarchical dependencies. For instance, in Figure 3.6, Opponent may start computation with $q_4^-$. This enables three moves: $\mathbf{tt}_4^+$ and $\mathbf{ff}_4^+$, as Player may implement a constant function answering without evaluating its arguments. And, $q_3^+$ if Player wishes to evaluate $f$. In turn, this lets Opponent return $\mathbf{tt}_3^-$ or $\mathbf{ff}_3^-$, or evaluate one of its arguments – and so on.
<figure><img src="image_16.png" /><figcaption>Figure 3.6: The arena for the sequent $f : \mathbb{B} \to \mathbb{B} \to \mathbb{B} \vdash \mathbb{B}$</figcaption></figure>

Clearly, executions will not be merely walks on this tree: typically a function evaluates some of its arguments, possibly several times, then returns a value. Accordingly, executions may hop around branches of the arena, as captured formally by:

**Definition 3.1.4.** A pointing sequence on arena A is $s = s_1 \dots s_n \in |A|^*$, where each $s_i$ may come with a pointer to some $s_j$ with $j < i$. It is legal if it satisfies:

justified: if $s_i$ points to $s_j$, then $s_j \to_A s_i$,

initialized: if $s_i$ has no pointer, then it is minimal in A.

A (alternating) legal play on A is a legal pointing sequence which is:

alternating: for all $1 \le i \le n-1$, $\text{pol}_A(s_i) \ne \text{pol}_A(s_{i+1})$,

We write $\downarrow\uparrow$-Plays(A) for the set of alternating legal plays on A.

For instance, the following is an alternating legal play in the arena of Figure 3.6:

$$ q_4^- \leftarrow q_3^+ \leftarrow q_1^- \qquad (3.1) $$

but it is not usually drawn like that: instead it is drawn from top to bottom instead of left to right, pointers are represented via dotted lines and without arrow heads (as they must always go back in time), and the indices 1, 2, 3, 4 are omitted, the same information being conveyed by placing moves under the corresponding type component. Following this convention, the alternating legal play above is drawn as in Figure 3.5 on the rhs.

For the rest of this chapter, unless specified otherwise, by *play* we always mean *alternating legal play*. The arguably heavy notation $\downarrow\uparrow$-Plays(A) invites an explanation: say that a play $s \in \downarrow\uparrow$-Plays(A) is in state O if it has even length, i.e. it is Opponent's turn to play. Likewise, an odd-length play is in state P. The two arrows $\downarrow\uparrow$ suggest alternation as the control alternates between two states O and P, while the arrow $\leftarrow$ evokes pointers as in (3.1). This is the first instance of a scheme followed throughout this monograph for different kinds of plays – alternating or not; pointing or not.

We introduce some notations on plays. We use $s, t, u, v$ to range over plays, and $\epsilon$ for the empty play. We write $\sqsubseteq$ for the prefix ordering on plays, which includes compatibility with pointers. We often extend plays by juxtaposing moves as in sab where it is
understood that *s* is a play and *a*, *b* are moves, leaving their possible pointer implicit. When writing equalities such as *sab* = *t*, it is understood that pointers are required to coincide as well. If *s* is a play, we write it *s*₁... *s*ₙ and refer to *s*ᵢ for individual moves. If *s*ᵢ points to *s*ⱼ (with *j* < *i*), we call *s*ⱼ the **justifier** of *s*ᵢ.

Plays with pointers are a powerful formalism, but one drawback is that unlike in simple games, they are no longer simply strings of moves. The reader may notice that they are referred to in english, as in “sⱼ points to sᵢ” rather than via a specific rigorous representation, e.g. conveyed by a partial function from indices to indices. Debatable as it is, this is the standard practice in Hyland-Ong games – manipulations on plays with pointers are always cumbersome, but can quickly become unwieldy especially if done formally, as pointers must be constantly reindexed or reassigned<fnref n="3" />.

We can define strategies on an arena, similarly to Definition 3.1.2:

**Definition 3.1.5.** For A an arena, an **alternating strategy** $\sigma : A$, or $\downarrow\uparrow$-strategy for short, is a set $\sigma \subseteq \downarrow\uparrow$-Plays(A) satisfying the following conditions:

non-empty: $\epsilon \in \sigma$,

prefix-closed: $\forall s \sqsubseteq t \in \sigma, s \in \sigma$,

receptive: $\forall s \in \sigma, sa^- \in \downarrow\uparrow$-Plays(A) \Rightarrow sa^- \in \sigma$,

deterministic: $\forall sa^-b_1^+, sa^-b_2^+ \in \sigma, sab_1 = sab_2$

We refer to an alternating strategy simply as a *strategy* when it causes no confusion.

**Copy indices.** We are due for a discussion on the other main solution to the thread indexing problem, *copy indices*. But we prefer to postpone this to Section 3.4, and instead we carry on with the construction of pointer game semantics.

## 3.2 Carving Out Innocent Strategies

Now that we know how to play, we may explore the model and examine its computational meaning – starting from PCF, the core of all languages used in this monograph.

### 3.2.1 The Strategies of PCF

**Interpretation of types.** Following Section 2.2, we consider in this monograph a version of PCF with one constructor $\Rightarrow$ for the function space, and three base types ($U$, $B$ and $N$). Accordingly, there are three *basic arenas* $U$, $B$ and $N$, described in Figures 3.7, 3.8 and 3.9 respectively – ignoring for now the annotation of moves with *Q* and *A*.

In light of the discussion above, these arenas should be rather self-explanatory: Option prompts computation with the initial move $q^-$, and Player answers with a value. One important common point is that all three are *well-opened*:

<footnote n="3">³There have been proposals for a more rigorous handling of pointers, notably resting on nominal sets in [Gabbay and Ghica, 2012]. The issue does not appear in AJM games, where pointers are absent altogether – though this absence limits the expressiveness of AJM games. In the model proposed later in this monograph, *concurrent games*, the issue is avoided as pointers are present, but derived rather primitive.</footnote>
<figure><img src="image_17.png" /><figcaption>Figure 3.7: U</figcaption></figure>

<figure><img src="image_18.png" /><figcaption>Figure 3.8: B</figcaption></figure>

<figure><img src="image_19.png" /><figcaption>Figure 3.9: N</figcaption></figure>

**Definition 3.2.1.** An arena A is **well-opened** if and only if it has exactly one minimal move, called the **initial move** of A, and written init(A).

In fact, arenas arising as the interpretation of types of PCF will always be well-opened. This lets us describe an easy construction for the arrow of two arenas.

**Definition 3.2.2.** Consider $A_1, A_2$ arenas with $A_2$ well-opened.

Then, the (well-opened) **arrow** arena $A_1 \Rightarrow A_2$ is defined via components:

moves: $|A_1 \Rightarrow A_2| = |A_1| + |A_2|$

causality: $(i, a) \le_{A_1 \Rightarrow A_2} (j, a') \Leftrightarrow (i = j \& a \le_{A_i} a') \lor (i = 2 \& a = \text{init}(A_2))$

polarities: $\text{pol}_{A_1 \Rightarrow A_2}(i, a) = (-1)^i \text{pol}_{A_i}(a)$.

In $A \Rightarrow B$, the two arenas are first put side by side, with polarities reversed in A (so that Player and Opponent exchange roles). Then, A is set to depend on the initial move of B. This means that once the initial move is played in $A \Rightarrow B$, Player has two choices: either to play in B (ignoring A), or to play some minimal move in A.

Altogether, this yields an interpretation of types of PCF as arenas, via

$$ \llbracket A \to B \rrbracket = \llbracket A \rrbracket \Rightarrow \llbracket B \rrbracket $$

with $\llbracket U \rrbracket = U, \llbracket B \rrbracket = B$ and $\llbracket N \rrbracket = N$. The reader is invited to check that for instance, $\llbracket (B \to B \to B) \to B \rrbracket$ is indeed the arena shown in Figure 3.6.

**Interpretation of terms.** For each term $\vdash M : A$, there is a strategy

$$ \llbracket M \rrbracket : \llbracket A \rrbracket, $$

its interpretation – it is computed by induction on M following the methodology of denotational semantics, via a cartesian closed category of arenas and strategies. This will appear in due course but we postpone it for now: it takes a while to set up this machinery, which is not needed to build up an intuition for what game semantics do.

Though the strategy of a term is computed denotationally, an experienced game semanticist will be able to directly list its plays, without going through the intricate definition of the interpretation. This is because plays are executions: rather than denotationally, they can be obtained directly from the term by operational means<fnref n="4" />. This is

<footnote n="4">⁴Though making this formal is not easy, and has been the topic of an active line of work around operational game semantics [Danos et al., 1996, Jaber, 2015, Ghica and Tzevelekos, 2012, Levy and Staton, 2014].</footnote>
<figure><img src="image_20.png" /><figcaption>Figure 3.10: Illustration of the operational content of game semantics</figcaption></figure>

illustrated in Figure 3.10. As before, Opponent moves trigger the evaluation of a subterm, which is highlighted. The following Player move then corresponds to the head (i.e. leftmost) variable occurrence (or constant) of the subterm being evaluated. The pointers from Player moves correspond to the stage where the variable in head position was abstracted, or to the function call being returned by the value in head position.

The standard way of stating that the model reflects computation is:

**Proposition 3.2.3.** *The interpretation is computationally adequate for PCF:*

For each $\vdash M : \mathcal{X}$, we have $M \Downarrow \text{iff } [M]$ has an answer to the initial move.

Plays give a mathematically, syntax-independent notion of interactive execution. In principle, a play may be realized by many different programs, but are all plays realizable by some program? By a program from PCF, or from a more expressive language?

### 3.2.2 Well-Bracketing

For instance, is the following play a possible execution of a term?

<figure><img src="image_21.png" /></figure>

We argue informally why this *cannot* be an execution in PCF. The first action of the term is to ask its argument, so within PCF it must have the form $\lambda f^{U \to U} . f M$; we
annotate the figure with the corresponding operational state as in Figure 3.10. In the last line, **tt** at toplevel indicates the overall computation has terminated to **tt**. This is confusing, since in the third line, only the argument of *f* was under evaluation. How can evaluating the argument of *f* cause the whole computation to terminate?

Nevertheless, this play is indeed a realistic execution, for the term

$$ \lambda f^{U \to U} . \mathbf{callcc} (\lambda k^{\mathbb{B} \to U} . f(k \mathbf{tt}); \perp) : (U \to U) \to \mathbb{B} $$

where **callcc** is the *call-with-current-continuation* primitive originating in *Scheme*, and which famously may be typed with Peirce's law [Griffin, 1990]. We shall not need the precise operational semantics of **callcc**, but informally **callcc** *M* immediately calls *M*, feeding it a special function *k*, the “continuation”. When the continuation is called with value *v*, **callcc** interrupts *M* and returns *v* at toplevel, breaking the call stack discipline.

Can the play above be realised without **callcc** (or some other analogous *control operator*)? We can show that the answer is no, by capturing those plays that “respect the call stack discipline”, and refining the whole interpretation to show that the interpretation of terms only yields such plays. This is the goal of the notion of *well-bracketing*.

First we enrich arenas:

**Definition 3.2.4.** *A Question/Answer labeling on arena A is a function*

$$ \lambda_A : |A| \to \{Q, A\} $$

which satisfies the following conditions:

question-opening: if $a \in |A|$ is minimal, then $\lambda_A(a) = Q$,
answer-closing: if $\lambda_A(a) = A$, then $a$ is maximal for $\le_A$,

*Questions* intuitively correspond to variable calls, while *Answers* correspond to returns. From now on, we assume that all **arenas** have a **Question/Answer labeling**. For basic arenas **U**, **B** and **N**, the labelling is as indicated in Figures 3.7, 3.8 and 3.9: the initial Opponent move is a **Question**, and the different values are **Answers**. This is extended to the arrow arena with $\lambda_{A \Rightarrow B}(1, a) = \lambda_A(a)$ and $\lambda_{A \Rightarrow B}(2, b) = \lambda_B(b)$.

If $s \in \downarrow\uparrow$-Plays($A$) and $s_i$ is an answer, it cannot be minimal in $A$ by question-opening. Its antecedent in $A$ appears in $s$ as some $s_j$ with $j < i$, and is a question by answer-closing. We say that $s_i$ **answers** $s_j$. If a question in $s$ has an answer in $s$ we say it is **answered** in $s$. The last unanswered question of $s$, if any, is the **pending question**.

We now capture executions respecting the call stack discipline:

**Definition 3.2.5.** *Consider A an arena, and $s \in \downarrow\uparrow$-Plays($A$) an alternating legal play. It is well-bracketed if for all prefix $ta^A \subseteq s$, a answers the pending question of t.*

All plays encountered in the monograph until now are well-bracketed, with the exception of the example at the beginning of Section 3.2.2. We can then define:

**Definition 3.2.6.** Let $\sigma: A$ be a strategy on $A$.
It is **well-bracketed** iff for all $sa^+ \in \sigma$, if $s$ is well-bracketed then so is $sa$.
<figure><img src="image_22.png" /><figcaption>Figure 3.11: A play for a strategy with references</figcaption></figure>

Thus, a well-bracketed strategy is never the first to break the call stack discipline.

We shall see that all the operations on strategies used in the interpretation of PCF (notably, composition) preserve well-bracketing. In the execution at the start of Section 3.2.2, Player is the first to break well-bracketing; so this execution cannot occur in a well-bracketed strategy, and is therefore – as expected – unrealizable in PCF.

### 3.2.3 Visibility and Innocence

Likewise, is this play a possible execution of a term?

<figure><img src="image_23.png" /></figure>

This also seems unfeasible in PCF. Again, on the rhs we show, assuming a term realising this play, its corresponding operational states. At the third and fifth moves, the *same* subterm is being evaluated; yet we get two distinct answers. In an extension of PCF with a primitive $\otimes$ for non-deterministic choice, this play would be realisable by $\lambda f^{\mathbb{B} \to \mathbb{U}}. f(\mathbf{tt} \otimes \mathbf{ff})$. But does it make computational sense in a *deterministic* language?

Once more, the answer is yes: the play above describes a valid execution of the term

$$ \lambda f^{\mathbb{B} \to \mathbb{U}}. \mathbf{newref} r \text{ in } f (\mathbf{let } x =!r \text{ in } r := 1; (x > 0)) : (\mathbb{B} \to \mathbb{U}) \to \mathbb{U} $$

in IA (see Section 2.2), i.e. PCF extended with references: **newref r in M** allocates a reference *r* initialized to 0. We show in Figure 3.11 an operational description.

Yet, again, this play cannot be realised in PCF. To show this, we give a version of *innocence* [Hyland and Ong, 2000], formalizing that without state, independent evaluations of the same subterm must yield the same response. The first step is a mathematical way to state that two Opponent-ending plays “evaluate the same subterm”, like the two prefixes of the play of Figure 3.11 terminating with a $q^-$ on the left.
<figure><img src="image_24.png" /><figcaption>Figure 3.12: A non P-visible play</figcaption></figure>

The operation computing (a mathematical notion of) “current subterm” is:

**Definition 3.2.7.** Let $s \in \upharpoonright \mathcal{P}^\mathcal{A}(A)$. Its P-view is the subsequence defined by:

$$ 
\begin{align*}
\lceil \epsilon \rceil &= \epsilon \\
\lceil sa^+ \rceil &= \lceil s \rceil a^+ \\
\lceil sa_1^+ s' a_2^- \rceil &= \lceil s \rceil a_1^+ a_2^- \quad \text{if } a_2 \text{ points to } a_1, \\
\lceil sa_2^- \rceil &= a_2^- \quad \text{if } a_2 \text{ is minimal,}
\end{align*}
$$

where pointers are preserved if their target remains in the subsequence.

We take the immediate prefix for P-ending plays and follow the pointer for O-ending plays. For instance, the prefixes of length 3 and 5 of the play on Figure 3.11 have the same P-view, capturing that they correspond to the same subterm. This is a fundamental definition – really, one of the cornerstones of HO games [Hyland and Ong, 2000].

But in order to use this definition it better be a well-defined operation on plays, which is not yet the case: for instance, in Figure 3.12 we gray out moves not selected in computing the P-view of $s \in \upharpoonright \mathcal{P}^\mathcal{A}(A)$ for $A = [(\cup \to \cup) \to \cup]$. The subsequence of $\lceil s \rceil$ in black is an alternating sequence of moves as needed, but it does not contain the justifier of $\checkmark^+$. So $\checkmark^+$ has no justifier in $\lceil s \rceil$, which means that $\lceil s \rceil \notin \upharpoonright \mathcal{P}^\mathcal{A}(A)$ as $\checkmark^+$ is not minimal in A. Accordingly, we focus on those plays where $\lceil - \rceil$ is defined:

**Definition 3.2.8.** A play $s \in \upharpoonright \mathcal{P}^\mathcal{A}(A)$ is **P-visible** if $\forall t \sqsubseteq s$, $\lceil t \rceil \in \upharpoonright \mathcal{P}^\mathcal{A}(A)$. Likewise, a strategy $\sigma$: A is **P-visible** (or just **visible**) iff all its plays are P-visible. We write **Vis(A)** for the set of P-visible strategies on arena A.

So, “computing P-views never drops pointers”, or “Player always points in the P-view”. On P-visible $s \in \upharpoonright \mathcal{P}^\mathcal{A}(A)$, the P-view always yields a (P-visible) play. We now define innocent strategies as those that behave the same in any situation where the same subterm is being evaluated, i.e. whose behaviour only depends on the P-view:

**Definition 3.2.9.** A P-visible strategy $\sigma$: A is innocent if it satisfies:

innocence: for all $sa^+ \in \sigma$ and $t \in \sigma$, if $\lceil s \rceil = \lceil t \rceil$ then $ta^+ \in \sigma$ with $\lceil sa \rceil = \lceil ta \rceil$.

We write **Inn(A)** for the set of innocent strategies on arena A.
The clause ⌜sa⌝ = ⌜ta⌝ serves to ensure that *a* has the “same” justifier in *s* and in *t*. Again we shall see that innocence is preserved by all operations involved in the interpretation of PCF so that any term of PCF is interpreted by an innocent strategy.

The play at the beginning of Figure 3.2.3 contains a direct failure of innocence – hence, it cannot appear in an innocent strategy and thus cannot be realised in PCF.

**O-visibility.** Whenever a condition constrains the behaviour of Player, one may consider the dual concerning Opponent. As a short digression we consider *O-visibility*, which will be technically helpful later on in this chapter. First we define:

**Definition 3.2.10.** Let $s \in \downarrow\uparrow-\mathcal{P}\mathcal{A}\mathcal{Y}s(A)$. Its *O-view* is the subsequence defined by:

$$ 
\begin{align*}
\llcorner \varepsilon \urcorner &= \varepsilon \\
\llcorner s a^- \urcorner &= \llcorner s \urcorner a^- \\
\llcorner s a^- s' a_2^+ \urcorner &= \llcorner s \urcorner a_1^- a_2^+ \quad \text{if } a_2 \text{ points to } a_1,
\end{align*}
$$

where pointers are preserved if their target remains in the subsequence.

The definition mirrors that of the P-view, with one missing clause for the initial move: this mirrors an asymmetry in the definition of arenas/plays, where initial moves must always be negative. As for P-views, this operation is well-defined only for:

**Definition 3.2.11.** A *play* $s \in \downarrow\uparrow-\mathcal{P}\mathcal{A}\mathcal{Y}s(A)$ is **O-visible** if $\forall t \sqsubseteq s, \llcorner t \urcorner \in \downarrow\uparrow-\mathcal{P}\mathcal{A}\mathcal{Y}s(A)$.

O-visibility captures those plays where the external environment acts in a P-visible way, i.e. does not have access to effects that break P-visibility, see Section 3.3.3. We say that $s \in \downarrow\uparrow-\mathcal{P}\mathcal{A}\mathcal{Y}s(A)$ is **visible** when it is both P-visible and O-visible.

One can also apply the same principle to innocence and define O-innocence capturing these plays where Opponent acts innocently, but this turns out less useful.

### 3.2.4 Finite Definability and Full Abstraction

At this point, via well-bracketing and innocence we have effectively eliminated all PCF non-definable behaviour. The theorem making this formal is called *finite definability*; we show the main steps of its proof as well as how it entails *intensional full abstraction*.

**Meager innocent strategies.** We have used the P-view operation as a mathematical attempt to capture the “current subterm” of a term reached in a play. Accordingly, it makes sense to attempt recovering syntax by examining those plays obtained by ⌜¬⌝. Clearly, for any P-visible $s \in \downarrow\uparrow-\mathcal{P}\mathcal{A}\mathcal{Y}s(A)$, we have ⌜rs⌝ = ⌜s⌝, so the plays obtained by ⌜¬⌝ are exactly those invariant under ⌜¬⌝, easily characterized as those P-visible plays where *Opponent always points to the previous move* – call these the **P-views**.

Following this discussion, it should be no surprise that the P-views are the key to reconstructing a term from a strategy. If $\sigma : A$ is P-visible, we define

$$ \mathcal{P}\sigma\mathcal{P} = \{\mathcal{P}s\mathcal{P} | s \in \sigma\} $$
the set of **P-views** of $\sigma$. If $\sigma$ is innocent, it is a simple fact that $\Gamma\sigma\Gamma' \subseteq \sigma$. Moreover, $\sigma$ can then be recovered as the set of P-visible plays $s$ such that for all $t \sqsubseteq s$, we have $\Gamma t \Gamma' \in \Gamma\sigma\Gamma'$. Thus, sets of P-views are an equivalent representation of innocent strategies.

It is informative to examine those sets of P-views matching innocent strategies:

**Definition 3.2.12.** A meager innocent strategy on A is a set V of P-views on A, s.t.:

non-empty: $\varepsilon \in V$,

prefix-closed: for all $s \in V$ and $t \sqsubseteq s$, then $t \in V$

receptive: for all $s \in V$, if $sa^-$ is a P-view then $sa \in V$,

deterministic: for all $sa_1^+, sa_2^+ \in V$ we have $sa_1 = sa_2$.

Finally, V is **well-bracketed** if all its plays are well-bracketed.

We write **Meager**(A) for the set of meager strategies on arena A.

From the above and routine verification, we obtain:

**Proposition 3.2.13.** Consider A an arena. Then we obtain a bijection:

$$ \Gamma - \Gamma' : \text{Inn}(A) \simeq \text{Meager}(A), $$

and moreover $\sigma$ is well-bracketed iff $\Gamma\sigma\Gamma'$ is.

*Proof.* The only subtlety is that is $\Gamma\sigma\Gamma'$ is well-bracketed, then $\sigma$ is well-bracketed. This follows from the preliminary observation, proved by induction on $s$, that if $s$ is well-bracketed then its pending question (if any) always appears in the P-view $\Gamma s \Gamma'$. $\square$

In a certain sense, meager innocent strategies are syntax – or at least, each finite meager innocent strategy may be equivalently written in the syntax of PCF:

**Finite definability.** Let us say that an innocent strategy $\sigma : A$ is **finite** if the corresponding meager strategy $\Gamma\sigma\Gamma'$ has finitely many even-length plays. The **size** of finite $\sigma$ is then the cardinal of the set of $s \in \Gamma\sigma\Gamma'$ of even length.

**Theorem 3.2.14.** Let A be a PCF type, and $\sigma : [[A]]$ be finite well-bracketed innocent.

Then, there is a PCF term $\vdash M : A$ s.t. $[[M]] = \sigma$.

*Sketch.* For more details than this sketch, see [Hyland and Ong, 2000].

W.l.o.g., the type A has the form $A_1 \to \dots \to A_n \to \mathcal{X}$ where for each $1 \le i \le n$,

$$ A_i = A_{i,1} \to \dots \to A_{i,p_i} \to \mathcal{X}_i. $$

We reason by induction on the size of $\sigma$. If $\sigma$ has no reaction to the (unique) minimal $\mathbf{q}^-$ in $\mathcal{X}$ (i.e. $\sigma = \{\varepsilon, \mathbf{q}^-\}$), any diverging term will do. Otherwise, by determinism there is exactly one move $a^+$ s.t. $\mathbf{q}^- a^+ \in \sigma$. If $a^+$ is an answer $v^+$ on $\mathcal{X}$, then M is the matching constant. Otherwise, $a^+$ is the initial $\mathbf{q}_{i_0}^+$ in some $A_{i_0}$. The situation is

<figure><img src="image_25.png" /></figure>
with, in grey, the possible extended P-views. For each, there is a residual substrategy.

We extract those – first, if $\mathbf{q}_{i_0}^+$ immediately returns. For each value $v$ in $\mathcal{X}_i$, we form

$$ \Gamma \sigma_v \Gamma' = \{ \mathbf{q}^{-} s \mid \mathbf{q}^{-} \mathbf{q}_{i_0}^{+} v^{-} s \in \Gamma \sigma' \}, $$

a meager innocent strategy on $\llbracket A \rrbracket$ of size strictly lesser than $\sigma$. By IH there is $\vdash M_v : A$ with $\llbracket M_v \rrbracket = \sigma_v$. As $\sigma$ is finite, there are finite many $v$ s.t. $\sigma_v$ is non-diverging.

Alternatively, for all $1 \le j \le p_{i_0}$, we consider P-views $\mathbf{q}^{-} \mathbf{q}_{i_0}^{+} \mathbf{q}_{i_0,j}^{-} s \in \Gamma \sigma^{\Gamma'}$ where as a P-view, $s$ answers neither $\mathbf{q}_{i_0}^{+}$, nor $\mathbf{q}^{-}$ by well-bracketing. Such a P-view yields

$$ \mathbf{q}_{i_0,j}^{-} s \in \upharpoonright \text{-Play} \mathfrak{S}(\llbracket A_1 \to \dots \to A_n \to A_{i_0,j} \rrbracket) $$

a P-view where moves in $s$ formerly depending on $\mathbf{q}^{-}$ in $\llbracket A \rrbracket$ are set to depend on $\mathbf{q}_{i_0,j}^{-}$. Considering all such P-views generates a meager innocent strategy of size strictly lesser than $\sigma$, hence by induction hypothesis there is $\vdash M_{i_0,j} : A_1 \to \dots \to A_n \to A_{i_0,j}$ s.t. $\llbracket M_{i_0,j} \rrbracket = \sigma_{i_0,j}$. Finally, with all this data we may form $\vdash M : A$ as

$$ \lambda x_1^{A_1} \dots x_n^{A_n} \text{ case } x_{i_0} (M_{i_0,1} x_1 \dots x_n) \dots (M_{i_0,p_{i_0}} x_1 \dots x_n) \text{ of } \\ v_1 \mapsto M_{v_1} \\ \dots \\ v_p \mapsto M_{v_p} $$

where $p$ is such that every $\sigma_{v_i}$ with $i > p$ is diverging. We get, as needed $\llbracket M \rrbracket = \sigma$. $\square$

This final statement is conceptually straightforward (if one has access to the definition of the interpretation, which we save for the next chapter), but technically challenging as reasoning concretely on the categorical definition of the interpretation and on the (forthcoming) composition of strategies is unwieldy. In the author's opinion, there is still room for improvement in finding a conceptually clean, fully detailed and human-readable proof of this that makes it as easy technically as it is conceptually.

Here, **case** is the syntax introduced in Section 2.2, involving the **let** construct. Without that, simply iterating **if** constructs would yield a strategy that re-computes

$$ x_{i_0} (M_{i_0,1} x_1 \dots x_n) \dots (M_{i_0,p_{i_0}} x_1 \dots x_n) $$

each time it matches it against a value. This is what is done in [Hyland and Ong, 2000] as the historical presentation of PCF does not include a **let** construct. This yields a term that is not quite $\sigma$, but is nonetheless observationally equivalent.

We conclude this discussion on definability with the statement:

**Conjecture 3.2.15 (Intensional Universality).** Consider a PCF type A. For any computable well-bracketed innocent $\sigma : \llbracket A \rrbracket$, there is $\vdash M : A$ s.t. $\llbracket M \rrbracket = \sigma$.

Hyland and Ong [Hyland and Ong, 2000] prove universality up to contextual equivalence (with a similar independent result in AJM games [Abramsky et al., 2000]). Their
construction fails to achieve intensional universality because their version of PCF lacks a “let” construct, making them unable to avoid repeated computation. There is strong confidence that their construction yields intensional universality in the presence of let (intensional universality does hold in call-by-value [Murawski and Tzevelekos, 2013]), but as far as we know the details have not been properly checked.

**Intensional Full Abstraction.** Recall from Section 2.3 that a model is *intensionally fully abstract* for a language when its observational quotient is fully abstract.

The famous *full abstraction for PCF* follows by a fairly typical argument, once one has an adequate model with sufficient definability properties.

**Theorem 3.2.16 (Intensional Full Abstraction for PCF).** *Innocent well-bracketed strategies form an intensionally fully abstract model for PCF.*

*Sketch.* Consider $\vdash M, N : A$ observationally equivalent, and assume $[M]$ and $[N]$ are not, i.e. there is a test $\alpha$ which distinguishes them. One may easily prove (see [Hyland and Ong, 2000]) that it suffices to consider $\alpha$ finite. By Theorem 3.2.14, $\alpha$ is defined by a PCF term, which we present as a context $C[-]$. By Proposition 3.2.3, it then follows that $C[-]$ distinguishes $M$ and $N$, contradiction. □

We have seen that by imposing well-bracketing and innocence, we have successfully banned all non PCF-definable behaviour. But dually, are references and control operators *complete*, are they sufficient to express unrestricted strategies?

## 3.3 Non-Innocence and Effects

Though Hyland-Ong games were originally designed as a model of plain PCF, what is in hindsight one of their most striking feature is that a crisp description of a few computational effects already hide in the definitions seen so far.

### 3.3.1 Non-Local State

As before, we start the discussion by looking at an example:

$\mathbb{B}$

$q^-$

$\vdash$

$\mathfrak{tt}^+$

$q^-$

$\vdash$

$\mathfrak{ff}^+$

Clearly, this play is not realizable in PCF since it breaks innocence. But unlike the play of Section 3.2.3, it is not realizable either in IA, the extension of PCF with local state. Indeed, if this is to be realized by a deterministic program, some state must be
shared – or some information must flow – between the two calls. In contrast, a closed term with access to local state may initialize variables only once computation has begun, and thus separate calls cannot enjoy any shared state.

Concretely, an hypothetical $\vdash$ **bad** : $\mathbb{B}$ acting as above would break $\beta$-equivalence:

$$ (\lambda x. \mathbf{if} x x x) \mathbf{bad} $$

should evaluate to **ff**, as all calls are routed to **bad**. Yet, **if bad bad bad** should evaluate to **tt**: we now have three separate instances of **bad**, so only the first call matters. In this monograph we deem this pathological: we are concerned with call-by-name languages, which must hence enjoy the call-by-name equational theory, including $\beta$-equivalence.

We ban **bad** via the notion of single-threadedness: a single-threaded strategy only depends on the current thread, so that it cannot pass information between distinct instances. For the next definition, in a play $s \in \downarrow\uparrow$-Plays($A$), we say that $s_i$ is hereditarily justified by $s_j$ (with $j < i$) if following the pointers from $s_i$ eventually hits $s_j$. If $s_j$ is initial, we say that $s_j$ is the (necessarily unique) initial hereditary justifier of $s_i$.

**Definition 3.3.1.** Consider A an arena, and $s \in \downarrow\uparrow$-Plays($A$).

The current thread of non-empty $s$, written $\lceil s \rceil$, is the subsequence of $s$ comprising all moves with the same initial hereditary justifier as the last move of $s$; and $\lceil \varepsilon \rceil = \varepsilon$.

The definition of single-threaded strategies then mimics that of innocent strategies:

**Definition 3.3.2.** Consider $\sigma$: A any strategy. It is single-threaded if it satisfies:

well-threaded: for all $sa^+ \sqsubseteq t \in \sigma$, the justifier of a appears in $\lceil s \rceil$,

single-threaded: for all $sa^+, t \in \sigma$, if $\lceil s \rceil = \lceil t \rceil$ then $ta^+ \in \sigma$ with $\lceil sa \rceil = \lceil ta \rceil$.

This bans pathological strategies such as **bad**. On the other hand, single-threadedness is preserved under all operations involved in the interpretation of IA so that the interpretation of any term of IA yields a single-threaded strategy.

### 3.3.2 Higher-Order State

Finally, for our last example, consider the following play:

<figure><img src="image_26.png" /></figure>
As shown in the indicative term on the right hand side, and following the intuitions on the operational content of game semantics so far, the last Player move corresponds to calling variable y. But how can that make sense, since y is not even in the scope!

Yet, again, this play is computationally meaningful – it witnesses *higher-order state*:

$$ \lambda F. \mathbf{newref}_A r \mathbf{in} F (\lambda xy. r := y; x) (!r) $$

Though we borrow the notation from IA, this must be read completely differently. Here A can be an arbitrary type, i.e. potentially a function. Whereas in IA, references store *values*, here they store *computations*; so that when the reference is read, the control flow *jumps* accordingly, giving control to arbitrary program phrases.

Higher-order state is a sensible programming feature, found in the wild in call-by-value languages such as ML. In call-by-value game semantics, a games model with morphisms set to comprise all well-bracketed single-threaded strategies is fully abstract model for a version of ML with higher-order store [Abramsky et al., 1998]. Semantic investigations have also been conducted in call-by-name [Laird, 2002, Goyet, 2013], but this is somewhat less natural from a programming language point of view. Either way, we leave higher-order state out of the scope of this monograph.

So how should one get rid of (the behaviours generated by) higher-order state? Without higher-order state, only information can flow through shared state, not control. So Player can only pass control (i.e. call variables) within the *scope*, i.e. the current syntactic branches. The same sentence, translated in game semantics terminology along the dictionary elaborated so far, reads: *Player can only point within the P-view*. But we have already seen this: this is *P-visibility* (Definition 3.2.8). So P-visibility, originally imposed as a preliminary construction just to make P-views well-defined, is actually also the condition we need to allow ground state but ban higher-order state!

P-visibility is preserved by all constructions used in the interpretation of IA (including ground type references), while the play above clearly is not P-visible.

### 3.3.3 The “Semantic Cube”

It is striking that almost, if not all, strategies in Hyland-Ong games correspond to existing programming features, for a framework originally designed for plain PCF only! From now on we assume that all strategies are single-threaded and P-visible, the canvas for the celebrated “semantic cube” that we shall present now.

**Idealized Algol.** Well-bracketed strategies support an adequate interpretation of IA:

**Proposition 3.3.3.** There is an interpretation $\llbracket - \rrbracket$ sending types of IA to arenas, and terms $\vdash M : A$ to well-bracketed, single-threaded, P-visible $\llbracket M \rrbracket : A$.

Moreover, for all $\vdash M : U$, $M \vdash \text{iff in } \llbracket M \rrbracket$, the initial move has an answer.

The interpretation of IA will be detailed in Section 4.2.

It turns out that well-bracketed strategies support “only” the interpretation of IA: we have a finite definability property similar to Theorem 3.2.14. We state:
**Theorem 3.3.4.** Consider A an IA type.

For any $\sigma : [[A]]$ visible, well-bracketed, single-threaded, and finite (i.e. with finitely many even-length plays) there is $\vdash M : A$ a term of IA such that $[[M]] = \sigma$.

We shall not give the detailed proof of this as their statement relies on the compositional structure, but the key arguments appear in Section 4.3.2.

As for PCF, from those definability properties follow:

**Theorem 3.3.5 (Intensional Full Abstraction for IA).** *P-visible well-bracketed single-threaded strategies form an intensionally fully abstract model for IA.*

The reasoning for that is the same as for Theorem 3.2.16.

Recall that intensional full abstraction means that the observational quotient of the model is fully abstract; in other words, visible well-bracketed single-threaded strategies have the same distinguishing power as terms of IA. As for PCF this makes the quotiented fully abstract model hard to reason with, but for IA something much more interesting happens: we can characterize concretely observational equivalence.

**Complete plays.** This is achievable by understanding which parts of a P-visible, well-bracketed strategy can be explored by a P-visible, well-bracketed Opponent – and among those, which lead to an observable result at toplevel. This is done via:

**Definition 3.3.6.** *Consider A an arena. A play $s \in \mathcal{L}\text{-Plays}(A)$ is complete iff it is well-bracketed, O-visible, P-visible, and every question has an answer.*

If $\sigma : A$, we write $comp(\sigma)$ for the set of its complete plays. Complete plays indeed characterize observational equivalence for P-visible well-bracketed strategies:

**Proposition 3.3.7.** *Consider $\sigma, \tau : A$ two P-visible, well-bracketed strategies. Then,*

$$ \sigma \approx \tau \Leftrightarrow \mathrm{comp}(\sigma) = \mathrm{comp}(\tau). $$

Again we omit the (rather simple) details which rely on the compositional structure introduced in the next chapter only, but the idea is the following. If a strategy $\alpha : A \Rightarrow \mathcal{U}$ distinguishes $\sigma$ and $\tau$, then it is straightforward to read from that a complete play in one but not the other. Reciprocally, if $s$ is a complete play in $\sigma$ but not in $\tau$, then $q^-s\check{=}^+$ (with adequate pointers) is a play in $A \Rightarrow \mathcal{U}$. The set of all prefixes of $q^-s\check{=}^+$, closed under receptivity, is then a valid strategy that distinguishes $\sigma$ and $\tau$.

From Proposition 3.3.7 and Theorem 3.3.5, it shall be clear that we get:

**Theorem 3.3.8.** *Consider A a type, and $\vdash M, N : A$ two terms of IA. Then,*

$$ M \approx N \Leftrightarrow \mathrm{comp}([M]) = \mathrm{comp}([N]). $$

This entails that the fully abstract model is *effectively presentable*: it can be phrased as a computable function into an effective domain [Plotkin, 1981]; concretely this means that observational equality is decidable between finite strategies (those with finitely
many even-length plays; forming the compact elements of the domain of strategies). This is remarkable: in the theory of programming languages, situations like that where one has a concrete characterization of observational equivalence, are rare!

This comes from the ability to write a context $C[-]$ reproducing one complete play $s$ and only $s$; so that $C[M] \Downarrow$ is exactly equivalent to $s \in [[M]]$. This is impossible for an innocent context, because if an innocent strategy includes one play, it also includes all plays with the same P-views. In fact, we know that the observational quotient in the model of PCF cannot be characterized concretely, because of Loader's result that the (unique) fully abstract model of PCF is not effectively presentable [Loader, 2001].

**Full abstraction with control.** We now drop well-bracketing. We also consider temporarily the extensions CIA and CPCF respectively of IA and PCF with

$$ \mathrm{calcc}_{A,B} : ((A \to B) \to A) \to A, $$

a control operator with behaviour described informally in Section 3.2.2. We shall not cover its behaviour or interpretation in detail as it plays no role in this monograph beyond painting the big picture. But we do mention two main results, first for CIA:

**Theorem 3.3.9.** *Visible single-threaded strategies form a fully abstract model for CIA.*
Moreover, if $\vdash M, N : A$ are two terms of CIA, then

$$ M \simeq N \quad \Leftrightarrow \quad \mathrm{O-vis}([M]) = \mathrm{O-vis}([N]), $$

with $\mathrm{O-vis}(\sigma)$ the set of $\mathrm{O}-\mathrm{visible}$ plays of a strategy $\sigma$.

This is proved again via an adequate definability result. This theorem was surely known long before it was published<fnref n="5" /> in [Murawski, 2007]. Here again, the fully abstract model is also effectively presentable. Note that contexts from CIA can observe more than contexts from IA: $\mathrm{calcc}$ lets us observe plays that cannot be completed, and hence would never have led to an observable behaviour within IA.

Finally, we mention one last fully abstract model:

**Theorem 3.3.10.** *Visible innocent strategies form a fully abstract model for CPCF.*

This is due to [Laird, 1997], proved again via an adequate definability property. In this case also, the fully abstract model is effectively presentable, but not as concretely as above: instead, one shows that equality between compact elements is decidable, by reducing equivalence checking to a finite number of tests. The fully abstract model can also be described concretely – and in fact was described concretely, before even the fully abstract games model for PCF were developed [Cartwright et al., 1994]!

**The “semantic cube”.** We have, so far, seen the following full abstraction results:

<footnote n="5">⁵Murawski uses a different primitive for control, but the difference is superficial within IA.</footnote>
<figure><img src="image_27.png" /><figcaption>Figure 3.13: The Semantic Cube</figcaption></figure>

**Theorem 3.3.11 (Semantic Cube).** We have four intensional full abstraction results:

<table><tr><td>G</td><td>is fully abstract for</td><td>PCF + state + control</td></tr><tr><td>G + innocence</td><td>is fully abstract for</td><td>PCF + control</td></tr><tr><td>G + well-bracketing</td><td>is fully abstract for</td><td>PCF + state</td></tr><tr><td>G + innocence + well-bracketing</td><td>is fully abstract for</td><td>PCF</td></tr></table>

where G denotes the model formed of visible, single-threaded strategies.

This “Semantic Cube”, drawn in Figure 14.2, expresses that the conditions on strategies capture the behaviour generated by certain computational effects; or rather the absence of certain effects. The achievement is noteworthy, as it is famously difficult to combine semantic accounts of effects. But independently of purely semantic purposes, this gives us a microscope to study behaviourally interactions between effects in programming languages. We demonstrate this with the following orthogonality property<fnref n="6" /> between state and control which nicely illustrates the strength of game semantics. We only state it as a conjecture, because it relies on intensional universality for PCF.

**Conjecture 3.3.12.** Let $\vdash M : A$ a term of CIA with $A$ a PCF type. Assume that

(1) $M \simeq N_1$ where $N_1$ does not use `callee`,

(2) $M \simeq N_2$ where $N_2$ does not use `newref`,

then there is $\vdash N : A$ in pure PCF such that $M \simeq N$.

*Proof.* We have $N_1 \simeq N_2$. By Theorem 3.3.9, they have the same O-visible plays. The P-views of $[[N_2]]$ are O-visible, so they must be in $[[N_1]]$, so they must be well-bracketed. But $[[N_2]]$ is innocent, so if its P-views are well-bracketed, then it must be well-bracketed (Proposition 3.2.13). Summing up, $[[N_2]]$ is an innocent well-bracketed strategy. But it is also computable, since the interpretation is computable. Hence, by Conjecture 3.2.15, there is $\vdash N : A$ in pure PCF such that $[[N]] = [[N_2]]$. In particular, it has the same O-visible plays as $M$, hence $M \simeq N$ by Theorem 3.3.9 again. $\square$

We finish this section with two concluding notes.

Firstly, game semantics has the reputation that its full abstraction results are unsatisfactory, because they consist in constraining strategies until they are essentially syntax,

<footnote n="6">⁶We learnt of it from a talk by Paul Levy in 2014 [Levy, 2014].</footnote>
followed by the same quotient that one could have done already in the syntax. This
criticism holds for PCF, and even then seems short-sighted: without the fully abstract
model for PCF, we would not have the semantic cube. But furthermore, beyond PCF,
*all fully abstract models in the semantic cube can be effectively presented!*

Secondly, unfortunately the semantic cube holds only for sequential deterministic languages. Beyond that we still have models (we shall see one in Chapter 5), but they do not fit in the same unified landscape as the cube above. What can be done about that? This is one of the leading questions behind this monograph.

## 3.4 An Alternative to Pointers: Copy Indices

As the final section of this chapter, we briefly present an alternative to the use of pointers for thread indexing: *copy indices*, used in particular in the other major family of traditional game semantics models, called AJM games for Abramsky, Jagadeesan and Malacaria [Abramsky et al., 2000]. We do this, on the one hand, to account for the large part of the game semantics literature that depends on it; and on the other hand, to help prepare the reader for concurrent games, which use copy indices.

The idea of copy indices is that rather than explicitly authorizing repetitions (and adding pointers to disambiguate the relationships between copies), we keep the invariant that each move must appear *at most once* in a play. So as to allow players to perform duplications, we create explicit copies of duplicable moves, which are kept apart by adjoining to each a unique identifier, a natural number called a *copy index*.

Copy indices must be added by an explicit construction on games. To that end, games with copy indices typically follow linear logic [Girard, 1987] and decompose the arrow construction in two steps $A \Rightarrow B = !A \dashv B$. Here, $\dashv$ is a *linear* or *affine* arrow that does not allow replication of the argument; and $!A$ is the *bang* construction from linear logic, which creates countably many copies of a game by adjoins copy indices:

**Definition 3.4.1.** Consider A a simple game. Then, the simple game !A has:

$$ 
\begin{align*}
|!A| &= \mathbb{N} \times |A| \\
\mathrm{pol}_{!A}(i, a) &= \mathrm{pol}_A(a) \\
P_{!A} &= \{s \in |!A|^* \mid s \text{ alternating, } \forall i \in \mathbb{N}, s \upharpoonright i \in P_A\}
\end{align*}
$$

where $s \upharpoonright i \in |A|^*$ is the obvious operation only keeping moves of the form $(i, a)$.

From here and throughout this monograph, we adopt the convention that copy indices are typeset in grey: this helps in easily distinguishing them from other indices, and is in line with the intuition that though their presence is needed to give copies an identity, their precise value is in general irrelevant. Now we have, for instance:

$$ P_{!\mathbb{B}}^{i} ::= \varepsilon \mid \mathbf{q}_{i}^{-} \mid \mathbf{q}_{i}^{-} \mathbf{t}_{i}^{+} P_{!\mathbb{B}}^{i \upharpoonright \{i\}} \mid \mathbf{q}_{i}^{-} \mathbf{f}_{i}^{+} P_{!\mathbb{B}}^{i \upharpoonright \{i\}} \quad i \notin I $$

and $P_{!\mathbb{B}} = P_{!\mathbb{B}}^{i}$; so plays in $!\mathbb{B}$ is any sequence of plays in $\mathbb{B}$, each with a copy index, in any order but such that each copy index is used at most once.
<figure><img src="image_28.png" /></figure>

<figure><img src="image_29.png" /><figcaption>Figure 3.14: Two plays with copy indices disambiguating Figure 3.3.</figcaption></figure>

As mentioned above, the usual call-by-name arrow is defined in linear logic by “Girard’s translation”. Accordingly, the interpretation of types include an occurrence of ! each time we cross the left of an arrow. Now, we saw that each move corresponds to a precise occurrence of a ground type in the type/typing judgment; so in the scope of a fixed number of !. Accordingly, each move carries a *sequence* of copy indices, once for each ambiant ! – by convention, we write first the copy index for the outermost !.

With this convention, the two plays corresponding to Figure 3.5 may be drawn<fnref n="7" /> with copy indices in Figure 3.14. This shows how copy indices carry implicitly the hierarchical relationship between moves expressed by pointers. Yet, plays are still straightforward sequences of moves, without unwieldy additional structure.

But if the information expressed by pointers can be recovered on mere plays with such a small technical overhead, why bother with pointers at all? In fact, we have yet to see the main subtlety – and technical hurdle – arising from copy indices.

**Equality up to copy indices.** The issue is that there are now many more strategies, as when playing a positive move, Player may seemingly arbitrarily choose a copy index – which does not seem to carry any relevant computational information.

In fact, this has the concrete consequence that simple games with replication as in Definition 3.4.1 fail to be a model of the simply-typed $\lambda$-calculus. Indeed we have

$$ x : \mathbb{B} \vdash (\lambda f. f x x)(\lambda y z. y) \cong_{\beta} (\lambda f. f x x)(\lambda y z. z) : \mathbb{B} \quad (3.2) $$

yet, following the usual definition of the interpretation (which we shall not present right now), the left hand side calls $x$ with copy index $0$ while the right hand side calls $x$ with copy index $1$. Copy indices trace back which occurrence of $x$ was selected in $\lambda f. f x x$, but remembering this is incompatible with $\beta$-equivalence.

To address this, AJM games add to simple games an equivalence relation on plays:

<footnote n="7">⁷Again, the play on the right hand side is not accepted by the usual definitions of simple games or AJM games as it is not locally alternating. But it is nevertheless illustrative of the real phenomenon.</footnote>
**Definition 3.4.2.** An AJM game comprises a simple game $A = (|A|, \text{pol}_A, \mathbf{P}_A)$, together with an equivalence relation $\cong_A$ on $\mathbf{P}_A$ satisfying the following conditions:

(1) if $s_1 \dots s_n \cong_A t_1 \dots t_p$, then $n = p$ and for all $1 \le i \le n$, $\text{pol}_A(s_i) = \text{pol}_A(t_i)$,

(2) if $s_1 \dots s_n \cong_A t_1 \dots t_n$, then for all $1 \le i \le n$, $s_1 \dots s_i \cong_A t_1 \dots t_i$,

(3) if $s \cong_A t$ and $sa \in \mathbf{P}_A$, then there is $tb \in \mathbf{P}_A$ such that $sa \cong_A tb$.

We think of the equivalence relation $\cong_A$ as formalizing *reindexings*, i.e. we have $s \cong_A t$ iff $s$ and $t$ are the same play, but with a different choice of copy indices. For ground types such as $\mathbb{B}$ the equivalence relation is restricted to reflexive pairs, but:

**Definition 3.4.3.** Consider A an AJM game. We set $!$ A following Definition 3.4.1, plus:

$$s_1 \dots s_n \cong_{!A} t_1 \dots t_n \iff \begin{array}{l} \text{there is a permutation } \pi : \mathbb{N} \cong \mathbb{N} \text{ such that} \\ \quad \left\{ \begin{array}{l} \text{for all } 1 \le i \le n, \text{ if } s_i = (k, a) \text{ then } t_i = (\pi(k), a'), \\ \text{and for all } k \in \mathbb{N}, s \upharpoonright k \cong_A t \upharpoonright \pi(k). \end{array} \right. \end{array}$$

In other words, an equivalence $s \cong_{!A} t$ follows a global reindexing on copy indices introduced by $!$, and local reindexings on each individual copy.

These reindexings on plays induce a partial equivalence relation on strategies:

**Definition 3.4.4.** Consider A an AJM game.

For $\sigma, \tau$: A strategies on the underlying simple game, we write $\sigma \approx \tau$ iff:

- $\rightarrow$-simulation: $\forall sa^+ \in \sigma, t \in \tau, s \cong_A t \Rightarrow \exists b^+, tb^+ \in \tau \& sa^+ \cong_A tb^+$

- $\leftarrow$-simulation: $\forall s \in \sigma, tb^+ \in \tau, s \cong_A t \Rightarrow \exists a^+, sa^+ \in \sigma \& sa^+ \cong_A tb^+$

- $\rightarrow$-receptive: $\forall sa^- \in \sigma, t \in \tau, sa^- \cong_A tb^- \Rightarrow tb^- \in \tau$

- $\leftarrow$-receptive: $\forall s \in \sigma, tb^- \in \tau, sa^- \cong_A tb^- \Rightarrow sa^- \in \sigma$

We say that $\sigma$: A is *uniform* iff $\sigma \approx \sigma$.

This allows us to consider equal strategies behaving the same up to their choice of copy indices – for instance, it identifies the two strategies corresponding to the terms of (3.2). But it does more: it select the *uniform* strategies, which are unable to observe the copy indices chosen by Opponent; i.e. with respect to which $\approx$ is a congruence.

When setting up a game semantics based on copy indices, the idea is that one only considers strategies which are uniform, and those are considered up to $\approx$.

**Pointers or Copy Indices?** In designing a game semantics supporting replication, one must use one or the other of these two structures. Which one should be chosen?

Beyond thread indexing, pointers also import into plays relevant semantical structures. In Hyland-Ong games, pointers are key to defining *P-visibility* and *innocence* [Hyland and Ong, 2000], the conditions that eventually gave rise to the semantic cube. On the other hand, pointers are hard to manipulate in a rigorous yet unobtrusive way.

In contrast, the AJM model has simpler plays, and enjoys a clean linear decomposition in the sense of Linear Logic [Girard, 1987]. However, terms are interpreted as
≈-equivalence classes rather than concrete strategies and all constructions come with a
sometimes challenging proof obligation that it preserves ≈. Conditions which rely on
pointers such as visibility and innocence are beyond reach without further structure.

Much of the literature in game semantics for programming languages has been devel-
oped based on pointers and Hyland-Ong games. However, in this monograph, we shall
see that *concurrent games* are based on copy indices. This is for two reasons: firstly,
their finer intensional structure seems to require it. Secondly, despite using copy in-
dices and unlike in AJM games, the *pointers* of Hyland-Ong games which have proved
so fruitful in studying program behaviour are retained as derived structures.

**3.5 Conclusions and Historical Notes**

Much of the basic definitions presented in this chapter originate (though with minor variations) in Hyland and Ong's original paper [Hyland and Ong, 2000], including the definitions of *visibility*, of *innocence* and of *well-bracketing* (on plays). The realization that lifting these constraints yielded fully abstract models for richer languages came very quickly: full abstraction for IA is due to [Abramsky and McCusker, 1996], full abstraction for CPCF is due to Laird in [Laird, 1997]. To our knowledge, the full abstraction result for the missing corner of the cube (CIA) was only developed in detail significantly later by Murawski [Murawski, 2007] – though it was certainly well-known.

It might seem confusing that apart from this latter paper, all the works cited here,
which build on Hyland and Ong's framework, date from *before* the publication of the
original Hyland and Ong paper. In fact, though the Hyland and Ong paper was published
only in 2000, preliminary versions of it circulated from the earlier 90s<fnref n="8" />, in parallel with
versions of the AJM model. These developments, and announcements by the two com-
peting groups, were closely followed by the broader denotational semantics community,
feeling that the resolution of the problem of “full abstraction for PCF” was close.

In hindsight, rather than the full abstraction result for PCF *per se*, what had the most
impact was definitely the nice surprised that many different effects could be captured in a
unified framework; justifying the 2017 *Alonzo Church Award* awarded to the founders
of game semantics. Game semantics has since then grown to a broad topic; and this
monograph shall cover some of its most recent developments.

<footnote n="8">⁸The workshop celebrating the 25 years of game semantics was held in 2018 as part of the federated logic conference (FLoC), which places the birth of game semantics – somewhat arbitrarily – in 1993.</footnote>
# Chapter 4

# The Category of Alternating Strategies

In this chapter, we continue our introduction to sequential game semantics, filling the gap left open in the previous chapter: the compositional structure. We show how to compose alternating strategies, forming a cartesian closed category $↓↑-Strat$. Then, we define the interpretation of IA into $↓↑-Strat$, and conclude with some complements.

## 4.1 The Ambient Cartesian Closed Category $↓↑-Strat$

We organize arenas and P-visible strategies into a cartesian closed category $↓↑-Strat$. Its objects will be arenas, already presented in Section 3.1.3. But the cartesian structure requires more arena constructions beyond the well-opened case shown in Chapter 3.

### 4.1.1 More Arena Constructions

We start with the *product arena*, used for interpreting contexts:

**Definition 4.1.1.** Consider $A_1, A_2$ arenas. Their *product* $A_1 \& A_2$ has components:

$$
\begin{array}{rcl@{\hspace{2em}}rcl}
\text{moves:} & |A_1 \& A_2| & = & |A_1| + |A_2| & \\
\text{causality:} & (i, a) \le_{A_1 \& A_2} (j, a') & \Leftrightarrow & i = j \ \& \ a \le_{A_i} a' & \\
\text{polarities:} & \mathrm{pol}_{A_1 \& A_2}(i, a) & = & \mathrm{pol}_{A_i}(a), & \\
\text{Q/A-labeling:} & \lambda_{A_1 \& A_2}(i, a) & = & \lambda_{A_i}(a), &
\end{array}
$$

generalizing to an *n-ary* construction $\&_{i \in I} A_i$ in the obvious way (for I a finite set).

This construction puts arenas $A_1$ and $A_2$ side-by-side, without interaction – Opponent may start evaluation in either component. Like a forest is formed of trees, any arena is – up to isomorphism – a product of well-opened arenas:
<figure><img src="image_30.png" /><figcaption>Figure 4.1: The arena $U \Rightarrow (U \& U)$</figcaption></figure>

**Lemma 4.1.2.** Consider A an arena.

Then there is $(A_i)_{i \in I}$ of well-opened arenas, unique up to iso, s.t. $A \cong \&_{i \in I} A_i$.

Here, an **isomorphism** of arenas is any forest-isomorphism preserving polarities and $Q/A$-labeling – likewise, two families $(A_i)_{i \in I}$ and $(B_j)_{j \in J}$ are **isomorphic** if there is a bijection $\pi: I \simeq J$ and for each $i \in I$, an isomorphism $A_i \cong B_{\pi(i)}$.

Recall that in Definition 3.2.2, we defined the **arrow** $A \Rightarrow B$ of two arenas $A$ and $B$ with $B$ well-opened. Building a cartesian closed category requires us to extend $A \Rightarrow B$ to the case where $B$ may not be well-opened. However, $A \Rightarrow -$ shall be the right adjoint to $A \times $, and so must preserve products; so we know that we must have:

$$A \Rightarrow (B \times C) \cong (A \Rightarrow B) \times (A \Rightarrow C),$$

and via Lemma 4.1.2 we may take that as a definition:

**Definition 4.1.3.** For $A, B = \&_{i \in I} B_i$ any two arenas, we set:

$$A \Rightarrow B = \bigoplus_{i \in I} A \Rightarrow B_i.$$

This has the effect of creating one copy of $A$ for each minimal move in $B^1$ – in particular, if $B$ is the empty arena, then so is $A \Rightarrow B$. In Figure 4.1 we show an example illustrating the arrow construction on non well-opened arenas.

## 4.1.2 Composition of Strategies

**Restrictions.** We first require notations for restrictions of plays of an arena to a sub-component. We will actually define the restriction of a play along an embedding:

**Definition 4.1.4.** Consider A, B arenas.

An embedding $f: A \hookrightarrow B$ is any injection $f: |A| \to |B|$.

<footnote n="1">¹This definition is equivalent to the original one [Hyland and Ong, 2000]. One may alternatively avoid the duplication of $A$ by considering arenas to be directed acyclic graphs rather than forests, and having minimal moves of $A$ depend on all the minimal moves in $B$: this is done for instance in [Harmer, 2004]. This is fine in the sense that the two constructions generate the same set of plays (see Definition 3.1.4), but arenas then no longer characterize types up to isomorphism, and the connection with thin concurrent games is blurred out.</footnote>
We use embeddings to address specific components inside arenas: for instance, there is a canonical embedding $A \hookrightarrow A \times B$, etc. The embeddings we use in practice satisfy many additional properties, but it is not useful to require them explicitly.

We can restrict a play along an embedding:

**Definition 4.1.5.** Consider A, B arenas, $f: A \hookrightarrow B$, and s a pointing sequence on B. The restriction of s along f, denoted by $s \upharpoonright f$, has moves the sequence defined by

$$ 
\begin{align*}
\varepsilon \upharpoonright f &= \varepsilon \\
sb \upharpoonright f &= (s \upharpoonright f)a \quad \text{if } b = f(a), \\
sb \upharpoonright f &= s \upharpoonright f \quad \text{otherwise.}
\end{align*}
$$

Moreover, in $s \upharpoonright f$, $s_i$ points to $s_j$ iff there is a sequence of pointers

$$ \dots s_j \dots \dots s_i \dots $$

in s, with all intermediary points not selected in $s \upharpoonright j$.

The restriction $s \upharpoonright f$ is a pointing sequence on A, but there is no guarantee that it is a legal play on A, even if $s \in \downarrow\uparrow$-Plays(B). However, that will often be the case when using this notion. This overly general definition has two use cases in practice:

Firstly, situations like restrictions along the canonical embedding $A \hookrightarrow A \times B$, where the transitive clause for pointers is not used at all. For $s \in \downarrow\uparrow$-Plays($A \times B$), we write $s \upharpoonright A \in \downarrow\uparrow$-Plays($A$) for the restriction along the (implicit) canonical embedding, which the reader should always be able to disambiguate easily. Secondly, situations like restrictions along the canonical embedding $A \Rightarrow C \hookrightarrow (A \Rightarrow B) \Rightarrow C$. In that case we write $s \upharpoonright A, C$, which may not always be a valid play on $A \Rightarrow C$ (it may not be alternating). As here, in general we never explicitely specify the embedding used in the restriction, but it should hopefully always be clear from the context.

**Interactions.** Consider $\sigma: A \Rightarrow B$ and $\tau: B \Rightarrow C$ two strategies. Observe that $\sigma$ and $\tau$ have dual perspectives on the polarities in B: when $\sigma$ plays a Player move in B, it is an Opponent move for $\tau$, and reciprocally. The first step in defining composition, is to plug $\sigma$ and $\tau$, letting them synchronize on B: this is called the *parallel interaction* of $\sigma$ and $\tau$. Then we hide the synchronized events, leaving a strategy on $A \Rightarrow C$.

We first focus on *parallel interaction*. An interaction between $\sigma$ and $\tau$, resulting of the synchronization of plays of $\sigma$ and $\tau$, is a pointing sequence that spans A, B and C:

**Definition 4.1.6.** Consider A, B and C arenas.

An interaction on A, B, C is a legal pointing sequence u on $(A \Rightarrow B) \Rightarrow C$ s.t.:

left-legal: $u \upharpoonright A, B \in \downarrow\uparrow$-Plays($A \Rightarrow B$),
right-legal: $u \upharpoonright B, C \in \downarrow\uparrow$-Plays($B \Rightarrow C$),
outer-legal: $u \upharpoonright A, C \in \downarrow\uparrow$-Plays($A \Rightarrow C$).

We write I(A, B, C) the set of all interactions on A, B, C.
<figure><img src="image_31.png" /><figcaption>Figure 4.2: State diagram for sequential interactions</figcaption></figure>

In interactions, moves in A, C are said to be **visible** while moves in B are **hidden** or **synchronized**. One may regard an interaction $u \in I(A, B, C)$ as involving three players: player $\ell$ plays in A, B; player $\tau$ plays on B, C. Finally, the **external Opponent** plays Opponent on A, C, i.e. plays moves that have negative polarity on $A \Rightarrow C$. Positive moves in $A \Rightarrow C$ may be due to $\ell$ or $\tau$; we say that they are due to the **global Player**, which we think of as $\ell$ and $\tau$ working together as a team.

The conditions *outer-legal*, *left-legal* and *right-legal* have a strong impact on how interactions may unfold. Indeed, recall from below Definition 3.1.4 that each alternating play has a *state*: O if it is Opponent's turn to play (if the play has even length), and P otherwise. The three conditions of Definition 4.1.6 involve three restrictions

$$u \uparrow A, B \in \downarrow\uparrow-\text{Plays}(A \Rightarrow B),$$

$$u \uparrow B, C \in \downarrow\uparrow-\text{Plays}(B \Rightarrow C),$$

$$u \uparrow A, C \in \downarrow\uparrow-\text{Plays}(A \Rightarrow C)$$

for $u \uparrow A, C \in \downarrow\uparrow-\text{Plays}(A \Rightarrow C)$. Accordingly, where the polarity state of a play is summarized by a single letter O or P, the polarity state of an interaction is summed up by three letters, keeping track of the state of these three restrictions, in order. There are strong constraints as to how we can jump between these states: for instance, in state OOO no move can be played in B, as no polarity in B can simultaneously satisfy the two constraints that the next move should be an Opponent move in both $A \Rightarrow B$ and $B \Rightarrow C$. Overall, it is fairly easy to show that only three states are reachable from the empty interaction: OOO, OPP, and POP; and the possible transitions between those are cleanly summarized in the **state diagram for interactions** in Figure 4.2.

We are often interested by interactions ending with a visible move from the global Player (which yield even-length plays of the composition). Those always have the shape

$$e^-(b \dots b)e^+ \dots e^-(b \dots b)e^+,$$

i.e. sequences of synchronized moves in b sandwiched by a pair of visible moves from the external Opponent, and global Player – this immediately follows from the diagram.

**Composition.** It is now time to define the composition of two strategies:

**Definition 4.1.7.** Consider $\sigma: A \Rightarrow B$ and $\tau: B \Rightarrow C$ two strategies.

An interaction between $\sigma$ and $\tau$ is any $u \in I(A, B, C)$ such that $u \uparrow A, B \in \sigma$ and
<figure><img src="image_32.png" /><figcaption>Figure 4.3: $u \in [x : U \vdash \lambda y. y; x : U \to U] \parallel [f : U \to U \vdash \lambda x. f(f x) : U \to U]$.</figcaption></figure>

$u \upharpoonright B, C \in \tau$. We write $\sigma \parallel \tau$ for the set of all interactions between $\sigma$ and $\tau$.

We may then define the **composition** $\tau \odot \sigma = \{u \upharpoonright A, C \mid u \in \sigma \parallel \tau\} : A \Rightarrow C$.

The process that to an interaction $u \in \sigma \parallel \tau$ associates $u \upharpoonright A, C \in \tau \odot \sigma$ is called **hiding**, hence completing the *parallel interaction plus hiding* paradigm. If $s \in \tau \odot \sigma$, we call any $u \in \sigma \parallel \tau$ such that $s = u \upharpoonright A, C$ a **witness** for $s$.

We give in Figure 4.3 an example interaction between two innocent strategies. In the diagram, moves are annotated with the player responsible: — if it is the external Opponent, + if it is the global Player, and then $\ell$ or $\nu$. This interaction is a witness to the play of the composition keeping the moves in black only.

When composing alternating strategies, the following property is crucial:

**Lemma 4.1.8 (Unique witness).** Consider $\sigma : A \Rightarrow B$ and $\tau : B \Rightarrow C$ strategies.

For all $s \in \tau \odot \sigma$, there is a unique $u \in \sigma \parallel \tau$ such that $u \upharpoonright A, C = s$.

*Proof*. Direct via the state diagram for interactions and determinism of $\sigma$ and $\tau$. $\square$

The next proposition states that composition is well-defined; and that all the conditions on strategies introduced in the previous chapter are stable under composition.

**Proposition 4.1.9.** Take $\sigma : A \Rightarrow B, \tau : B \Rightarrow C$ strategies as in Definition 3.1.5.
Then, $\tau \odot \sigma : A \Rightarrow C$ is a strategy in the sense of Definition 3.1.5. Moreover,

if $\sigma$ and $\tau$ are P-visible, then so is $\tau \odot \sigma$,

if $\sigma$ and $\tau$ are well-bracketed, then so is $\tau \odot \sigma$,

if $\sigma$ and $\tau$ are single-threaded, then so is $\tau \odot \sigma$,

if $\sigma$ and $\tau$ are innocent, then so is $\tau \odot \sigma$.

*Proof.* For Definition 3.1.5, non-empty and prefix-closed are clear, while receptive and determinism are direct via Lemma 4.1.8 and the state diagram of interactions.

For some of the further conditions, the proof of stability under composition can be fairly elaborate – we omit them, but give references. Composition of P-visibility is proved e.g. in [Clairambault, 2010, Proposition 2.2.6]; composition of well-bracketing is proved e.g. in [Clairambault, 2010, Proposition 2.3.3]; for single-threadedness, it follows from Harmer's theorem [Harmer, 1999, Proposition 3.5.5] that those are exactly the comonoid morphisms; and finally, a nice detailed proof of stability of innocence under composition appears in [Harmer, 2004, Proposition 3.3.2]. □

### 4.1.3 A Category of Arenas and Strategies

We now provide the categorical structure. Though we shall not give details for any of the required proofs, we shall still review the main arguments and provide references.

**Associativity.** For associativity, one first introduces the set $I(A, B, C, D)$ of ternary interactions: those legal pointing sequences $u$ on $((A \Rightarrow B) \Rightarrow C) \Rightarrow D$ such that

$$u \upharpoonright A, B \in \downarrow\upharpoonright\text{-Plays}(A \Rightarrow B),$$

$$u \upharpoonright B, C \in \downarrow\upharpoonright\text{-Plays}(B \Rightarrow C),$$

$$u \upharpoonright C, D \in \downarrow\upharpoonright\text{-Plays}(C \Rightarrow D),$$

$$u \upharpoonright A, D \in \downarrow\upharpoonright\text{-Plays}(A \Rightarrow D).$$

The key argument is the so-called “zipping lemma” ([Harmer, 2004, Lemma 2.6.1]):

**Lemma 4.1.10.** Consider $u \in I(A, C, D)$ and $v \in I(A, B, C)$ s.t. $u \upharpoonright A, C = v \upharpoonright A, C$. There is a unique $w \in I(A, B, C, D)$ s.t. $w \upharpoonright A, C, D = u, w \upharpoonright A, B, C = v$.

This is proved by induction on $u$. As the name suggests, the idea is to “zip” $u$ and $v$ together, using subsequences from $v$ to provide the moves in $B$ missing from $u$. There is also a mirror lemma zipping $u \in I(A, B, D)$ and $v \in I(B, C, D)$.

Associativity of composition follows:

**Proposition 4.1.11.** Consider $\sigma : A \Rightarrow B, \tau : B \Rightarrow C$ and $\nu : C \Rightarrow D$. Then, $\nu \odot (\tau \odot \sigma) = (\nu \odot \tau) \odot \sigma$.

*Proof.* Consider $s \in v \odot (\tau \odot \sigma)$. By definition, there is a witness $u \in (\tau \odot \sigma) \parallel v$, i.e. $u \in I(A, C, D)$ s.t. $u \upharpoonright A, C \in \tau \odot \sigma, u \upharpoonright C, D \in v$, and $u \upharpoonright A, D \in \downarrow\upharpoonright\text{-Plays}(A \Rightarrow D)$. By definition of composition again, there is $v \in \sigma \parallel \tau$ s.t. $v \upharpoonright A, C = u \upharpoonright A, C$. By the
zipping lemma, we can find $w \in I(A, B, C, D)$ s.t. $w \uparrow A, C = v$ and $w \uparrow A, C, D = u$; and $w \uparrow A, B \in \sigma, w \uparrow B, C \in \tau$ and $w \uparrow C, D \in v$.

One can then show that $w \uparrow B, D$ is alternating (this follows from a state diagram for ternary interactions extending that for interactions in Section 4.1.2). Hence $w \uparrow B, C, D \in \tau \parallel v$, hence $w \uparrow B, D \in v \odot \tau$. Since we also have $w \uparrow A, B \in \sigma$, we have $w \uparrow A, B, D \in \sigma \parallel (v \odot \tau)$, so $w \uparrow A, D \in (v \odot \tau) \odot \sigma$ as required.

The other inclusion is symmetric, using the mirror zipping lemma. $\square$

**Identities.** Identities in game semantics are given by *copycat strategies*.

The intuitive behaviour of copycat is very simple: it copies whatever move Opponent plays on either side, to the matching Player move on the other side, maintaining the invariant that we have the same play on A on both sides. More concretely:

**Definition 4.1.12.** *Consider A any arena.*

A copycat play on A is any P-visible $s \in \downarrow\uparrow$-Plays($A_1 \Rightarrow A_2$) which is:

$$ \text{balanced: } \forall ta^+ \sqsubseteq s, ta \uparrow A_1 = ta \uparrow A_2, $$

and we define $\mathfrak{c}_A : A \Rightarrow A$ as the set of copycat plays on A.

Copycat is a strategy: most conditions are direct, save for determinism that is a bit subtle. The issue is easy to miss as we tend to leave the management of pointers implicit: by *balanced*, an initial move on the left hand side can only immediately follow an initial move on the right hand side. But its *pointer* is not uniquely determined by *balanced*: if there are several initial moves on the right hand side, each can receive the pointer in a way compatible with *balanced*. This is however banned by the P-visible requirement, as in that case only the previous move appears in the P-view.

Copycat is indeed an identity for composition:

**Lemma 4.1.13.** *Consider $\sigma : A \Rightarrow B$ any strategy. Then, $\mathfrak{c}_B \odot \sigma = \sigma \odot \mathfrak{c}_A = \sigma$.*

*Proof.* By *receptive*, it suffices to prove the equality for even-length plays, i.e. Player-ending plays. Consider $s \in \mathfrak{c}_B \odot \sigma$ with even length – write $\mathfrak{c}_B : B_1 \Rightarrow B_2$ – and consider its witness $u \in \sigma \parallel \mathfrak{c}_B$. By the state diagram for interactions, $u$ is in state OOO, therefore $u \uparrow B_1, B_2$ is in state OO and is Player-ending, so $u \uparrow B_1 = u \uparrow B_2$. It follows that $u \uparrow A, B_1 = u \uparrow A, B_2 = s$, but $u \uparrow A, B_1 \in \sigma$, hence $s \in \sigma$.

Reciprocally, from $s \in \sigma$ with even length it is direct to construct by induction on $s$ an interaction $u \in \sigma \parallel \mathfrak{c}_B$ such that $u \uparrow A, B_1 = u \uparrow A, B_2 = s$, so that $s \in \mathfrak{c}_B \odot \sigma$ as required. Symmetrically, we have $\sigma \odot \mathfrak{c}_A = \sigma$ as well. $\square$

We conclude from all of the above:

**Corollary 4.1.14.** *There is a category $\downarrow\uparrow$-Strat (respectively $\downarrow\uparrow$-WB, $\downarrow\uparrow$-Inn, $\downarrow\uparrow$-InnWB) with arenas as objects, and as morphisms from A to B all P-visible single-threaded strategies (respectively all P-visible well-bracketed strategies, all innocent strategies, all innocent well-bracketed strategies) on A $\Rightarrow$ B.*
### 4.1.4 Cartesian Closed Structure

Next, we show that $\downarrow\uparrow$-Strat, $\downarrow\uparrow$-WB, $\downarrow\uparrow$-Inn and $\downarrow\uparrow$-InnWB are cartesian closed.

**Cartesian structure.** The empty arena 1 is terminal in all four categories: for all arena A, A $\Rightarrow$ 1 = 1, inhabited with a unique, empty, strategy. The product of A and B was defined in Definition 4.1.1. For arenas A, B, the two projections

$$ \pi_A : A \times B \Rightarrow A, \qquad \pi_B : A \times B \Rightarrow B $$

are the copycat strategies defined with the obvious adaptation of Definition 4.1.12.

To define the pairing, we prove:

**Lemma 4.1.15.** Consider $\Gamma$, A, B arenas, and $\sigma : \Gamma \Rightarrow A, \tau : \Gamma \Rightarrow B$ single-threaded. There exists a unique (necessarily) single-threaded strategy

$$ \langle \sigma, \tau \rangle : \Gamma \Rightarrow A \times B $$

comprising all $s \in \downarrow\uparrow$-Plays($\Gamma \Rightarrow A \times B$) such that for all $t \sqsubseteq s$, $[t] \in \sigma$ or $[t] \in \tau$.

*Proof.* Analogously to innocent strategies and P-views, single-threaded strategies are uniquely determined by their set of threads, see e.g. [Harmer, 2004, Section 2.8]. $\square$

Notice, in this definition, the implicit renaming of $[t] \in \downarrow\uparrow$-Plays($\Gamma \Rightarrow A \times B$) to $\downarrow\uparrow$-Plays($\Gamma \Rightarrow A$) or $\downarrow\uparrow$-Plays($\Gamma \Rightarrow B$) depending whether the initial move is in A or B.

This data satisfies the required equations for cartesian products:

**Lemma 4.1.16.** Consider $\sigma : \Gamma \Rightarrow A, \tau : \Gamma \Rightarrow B$, and $\nu : \Delta \Rightarrow \Gamma$ single-threaded. Then, the following equations hold:

$$ \begin{align*} \pi_A \odot \langle \sigma, \tau \rangle &= \sigma \\ \pi_B \odot \langle \sigma, \tau \rangle &= \tau \\ \langle \pi_A, \pi_B \rangle &= \mathfrak{c}_{A \times B} \\ \langle \sigma, \tau \rangle \odot \nu &= \langle \sigma \odot \nu, \tau \odot \nu \rangle. \end{align*} $$

*Proof.* The first two equations are direct variations of Lemma 4.1.13. The third is direct from the definition, and the fourth immediate on threads, using again that single-threaded strategies are uniquely determined by their sets of threads. $\square$

From the equations above, the following fact follows immediately.

**Corollary 4.1.17.** The categories $\downarrow\uparrow$-Strat, $\downarrow\uparrow$-WB and $\downarrow\uparrow$-Inn are cartesian.
**Cartesian closed structure.** Now, we describe the cartesian closure.

For any two arenas A and B, we have already defined their arrow $A \Rightarrow B$. We have:

**Lemma 4.1.18.** Consider $\Gamma, A$, and $B$ three arenas. Then we have

$$ \Xi_{\Gamma,A,B} : (\Gamma \times A) \Rightarrow B \cong \Gamma \Rightarrow (A \Rightarrow B) $$

an isomorphism of arenas, i.e. a bijection preserving and reflecting all structure.

*Proof.* Straightforward from the definition. $\square$

Up to renaming, $\Gamma \times A \Rightarrow B$ and $\Gamma \Rightarrow A \Rightarrow B$ are the same. Thus this means that the currying of $\sigma : \Gamma \times A \Rightarrow B$ can be described by applying $\Xi_{\Gamma,A,B}$ move-by-move:

**Lemma 4.1.19.** Consider $\Gamma, A$ and $B$ three arenas. Then, there is a bijection

$$ \Lambda_{\Gamma,A,B} : \downarrow\uparrow\text{-Strat}(\Gamma \times A, B) \cong \downarrow\uparrow\text{-Strat}(\Gamma, A \Rightarrow B) $$

preserving and reflecting innocence, and preserving composition in the sense that

$$ \Lambda_{\Gamma,A,B}(\sigma) \odot \gamma = \Lambda_{\Delta,A,B}(\sigma \odot (\gamma \times A)) \quad (4.1) $$

for all $\sigma \in \downarrow\uparrow\text{-Strat}(\Gamma \times A, B)$ and $\gamma \in \downarrow\uparrow\text{-Strat}(\Delta, \Gamma)$.

*Proof.* A routine manipulation on interactions. $\square$

In turn, this bijection lets us define the evaluation strategy simply as

$$ \mathbf{ev}_{A,B} = \Lambda_{A,A,B}^{-1}(\mathbf{c}_{A \Rightarrow B}) \in \downarrow\uparrow\text{-Strat}((A \Rightarrow B) \times A, B) $$

and from the above, it becomes routine to prove cartesian closure:

**Proposition 4.1.20.** $\downarrow\uparrow\text{-Strat}, \downarrow\uparrow\text{-WB}, \downarrow\uparrow\text{-Inn}$ and $\downarrow\uparrow\text{-InnWB}$ are cartesian closed.

*Proof.* We need the two equalities for the universal property of cartesian closure, for $\sigma \in \downarrow\uparrow\text{-Strat}(\Gamma \times A, B)$, $\gamma \in \downarrow\uparrow\text{-Strat}(\Delta, \Gamma)$ and $\tau \in \downarrow\uparrow\text{-Strat}(\Gamma, A \Rightarrow B)$:

$$ \mathbf{ev}_{A,B} \odot (\Lambda(\sigma) \times A) = \sigma \quad (4.2) $$

$$ \Lambda(\mathbf{ev}_{A,B} \odot (\tau \times A)) = \tau, \quad (4.3) $$

but those follow from elementary computation using definition of $\mathbf{ev}_{A,B}$, (4.1), neutrality of copycat for composition and the fact that $\Lambda$ is a bijection. $\square$

Since $\Lambda(-)$ preserves and reflects innocence and well-bracketing, the cartesian closed structure automatically holds for our four categories of interest.
**Internal language.** This cartesian closed structure allows us to use notations from the $\lambda$-calculus to manipulate strategies: these may be unfolded to primitive operations of cartesian closed categories in the standard way [Lambek and Scott, 1988]. For instance, the application of $\sigma \in \downarrow\uparrow$-Strat($\Gamma$, $A \Rightarrow B$) to $\tau \in \downarrow\uparrow$-Strat($\Gamma$, $A$) unfolds to

$$ \sigma \tau = ev_{A,B} \odot \langle \sigma, \tau \rangle, $$

likewise we will sometimes in the sequel use $\lambda$-abstraction on expressions for strategies.

### 4.1.5 Recursion

To handle recursion we must provide a fixpoint operator, i.e. an innocent strategy

$$ \mathcal{Y}_A : (A \Rightarrow A) \Rightarrow A $$

for each arena $A$ such that for every $\sigma \in \downarrow\uparrow$-Strat($\Gamma$, $A \Rightarrow A$), we have

$$ \mathcal{Y}_A \sigma = \sigma (\mathcal{Y}_A \sigma) $$

a fixpoint equation. It is solved as usual in denotational semantics, by constructing $\mathcal{Y}_A$ as a least upper bound for an adequate order on strategies – the following is direct:

**Proposition 4.1.21.** For arenas $A$ and $B$, $\downarrow\uparrow$-Strat($A$, $B$), $\downarrow\uparrow$-WB($A$, $B$), $\downarrow\uparrow$-Inn($A$, $B$) and $\downarrow\uparrow$-InnWB($A$, $B$) are partially ordered by inclusion, yielding pointed dcpos.

All operations on strategies involved in the cartesian closed structure are continuous, making $\downarrow\uparrow$-Strat, $\downarrow\uparrow$-WB, $\downarrow\uparrow$-Inn and $\downarrow\uparrow$-InnWB enriched over pointed dcpos.

Using this, we can obtain the fixpoint operator as the least upper bound of

$$ \begin{array}{rcl} F : & \downarrow\uparrow\text{-Strat}(A \Rightarrow A, A) & \rightarrow \downarrow\uparrow\text{-Strat}(A \Rightarrow A, A) \\ & \sigma & \mapsto \lambda f^{A \Rightarrow A} \cdot f(\sigma f) \end{array} $$

which unfolds to the following, for $\perp$ the minimal strategy just closed under receptivity:

$$ \mathcal{Y}_A = \bigcup_{n \in \mathbb{N}} F^n(\perp) \quad \in \quad \downarrow\uparrow\text{-Strat}(A \Rightarrow A, A) \qquad (4.4) $$

satisfying $\mathcal{Y}_A = F \mathcal{Y}_A$ by construction – we may then prove the fixpoint equation:

$$ \begin{align*} \mathcal{Y}_A \sigma &= F(\mathcal{Y}_A) \sigma \\ &= (\lambda f^{A \Rightarrow A} \cdot f(\mathcal{Y}_A f)) \sigma \\ &= \sigma(\mathcal{Y}_A \sigma) \end{align*} $$

using $\beta$-equivalence on the $\lambda$-calculus notation [Lambek and Scott, 1988].

## 4.2 Interpretation of IA

Following [Lambek and Scott, 1988], the cartesian closed structure developed above yields an interpretation of the simply-typed $\lambda$-calculus; we also showed the interpretation of the fixpoint combinator. In order to obtain the interpretation of PCF and IA, it remains to provide strategies matching the primitives of our programming languages.