Project Topics
Get Complete Project Material File(s) Now! »
The Birth of Game Semantics
Game semantics was first born in the realm of logic, in the form of dialogical logic [75]. Dialogical logic expresses proofs of a formula as two entities debating whether a formula is true or not: Proponent, who tries to prove that the formula is true, and Opponent, who tries to prove that it is false. This formal game is the description of a dialogue between two (rational) individuals would have when debating whether a mathematical proposition holds or not: they both defend their case until one of them is convinced they were wrong. A formula is true when Proponent has a winning strategy in a certain game played on the formula, which amounts to always managing to convince Opponent that the formula is true, no matter the objections that are raised.
It was then introduced into the world of programming languages under the name game semantics by a long series of authors, notably Berry and Curien [13] (under the name of sequential algorithms), who were the first to use the idea of interaction in semantics and gave a sequential, denotational semantics of a higher-order language, Blass [14, 15], who exhibited links between game se-mantics and linear logic [41], Joyal [58], who was the first to build a category of games and strategies, Coquand [23]; who linked game semantics to the dynamics of cut elimination (and thus to evaluation of programs), Abramsky, Jagadeesan, and Malacaria [6], and Hyland and Ong [56] and Nickau [87], who built the most well-known frameworks for game semantics today: AJM and HON games.
The most basic idea comes straight from dialogical logic: types are inter-preted as formal games (formulas) and programs as the interactions they may have with the environment (proofs of the formulas). In slightly more detail, types are interpreted as games (sometimes called arenas) on which notions of plays are built. Plays represent all the possible interactions an element of a given type may have with its environment. Programs of a certain type are then interpreted as strategies in that game, i.e., sets of plays satisfying some con-straints. These plays are the interactions the programs may actually have with the environment: if σ is the interpretation of a program P , then a play p belongs to σ if and only if P may interact with its environment according to p. Here, however, strategies are only used to compute values, and there are no “winning” strategies.
For example, the plays for natural numbers could be sequences of the form q N ∗, where q is a move in the game representing the environment asking (q stands for “question”) for the value of the number, and N is any natural number, which represents the program answering the value of the number. The strategy corresponding to a counter that increases by 1 each time it is called would consist of all plays of the form q 1 q 2 . . . q n. For functions of type int → int, the set of plays could be of the form qr ql Nl ∗ Nr ∗, where qr is a move that represents the environment asking the function for the result (r stands for “right”, as in the right-hand side of int → int) of its computation, Nr represents the function returning the value of its result to the environment, ql represents the function asking for the value of its argument (l stands for “left”), and Nl represents the environment giving the function the value of its argument. Such a sequence corresponds to the environment asking the function for the value of its result a certain number of times, and each time the function asks for the value of its argument a certain number of times before returning its result. For example, the strategy associated to the successor function would be the set of plays of the form qr ql nl1 n1 1 r . . . qr ql nlk nk 1 r. The exact structure of plays depends on the type of game semantics that we are considering, but this gives a good idea of what plays and strategies look like.
Two other ideas are also present in most game models today. The first one is innocence, which is that pure programs (those programs that only use purely functional features) are interpreted as innocent strategies. The behaviour of these strategies is based on limited information about what has happened in the play until now. This information basically encodes the part of the interaction between the program and its environment that has led to the current situation. In particular, a function may only rely on the current function call. For example, the strategy for the counter program above is not innocent because it needs to know what it answered last time, and that the only part an innocent strategy would be allowed to rely on is qr (and the counter is indeed impure). On the other hand, the strategy associated to the successor function is innocent because its answer nk + 1 r only depends on nkl, and nothing else.
Finally, an important aspect of game semantics is how strategies are com-posed. Indeed, game models are compositional, and there is in particular a no-tion of composition of strategies that corresponds to composition of programs. It is defined in two steps called parallel composition and hiding. Parallel com-position lets both strategies interact. To define it, we need to define a notion of “plays” on three games: assume that σ is a strategy on the games A and B and τ a strategy on the games B and C, then we want the parallel composite σ τ to be a strategy on the games A, B, and C. The parallel composite then accepts a play on A, B, C if and only if its projection to A, B is accepted
by σ and its projection to B, C is accepted by τ . The idea is that σ and τ communicate on the B game. The second step, hiding, consists in erasing the B game to make the composite a strategy only on the games A and C.
As we have already mentioned, game models may be considered denotational because they interpret programs as strategies, which are subsets of general struc-tures. On the other hand, they are operational because strategies are often in bijection with normal forms, and the interpretation of a program is exactly the interactions it may have with the environment, which makes these models close to the dynamics execution.
The Rich World of Game Models
Today, there are many game semantical models based on various ideas that make the game semantical landscape very diverse. What is probably considered the first game semantical model was built by Blass [14, 15]. In this setting, a game is described as the tree of its positions, and plays are branches of that tree. In the case of functions of type A → B, plays may be seen as a branch in A and a branch in B. A strategy is basically a choice of move to play at each node. Composition of strategies is defined by playing on three trees at the same time (then hiding what happens on the middle tree). However, composition is not associative (because of a technical problem with polarity of moves).
The first game semantical models that have become popular and whose vari-ants are still used today are AJM games [6] and HON games [56], which were both invented in the 1990s. AJM games define games as sets of moves together with a condition that tells when a sequence of moves is a valid play. HON games define games as a structured set of moves and plays as structured sequences (the exact structure is beyond the point here). Both models then define strategies as prefix-closed sets of plays and composition of strategies as parallel composition plus hiding, where both operations are defined in similar ways in both models.
Today, there are many variants of HON and AJM games, invented for differ-ent purposes. First of all, a number of variations on these games (that impose further conditions on sequences to be valid plays) are described in Harmer’s PhD thesis [46]. Some variations are not covered by the reference above, for example [52], in which polarity is reversed. Other variations enrich games with more structure, such as “copycat links” [70], group actions [79, 7, 86], or “co-herence” [68]. There are also other models based on the same ideas, but where games can be plugged into other games, such as polymorphic games [53], vari-able games [4], open games [22], or context games [71]. There are other variants that are neither really HON nor AJM, but use the very same ideas, such as the sequoidal category built in [66]. Some models define games as trees (somewhat like Blass games) and strategies as morphisms of games [54, 47].
Furthermore, there are many concurrent game models. This is not surprising in the sense that a fundamental point of concurrency is the interaction between agents, and interaction is precisely at the heart of game semantics. These models may be based on HON games [67, 69, 40, 97] or more exotic structures. One such structure is event structures [88], which are more focused on conflict between events than the game models above (thus possibly more suited for concurrency) and which have given many successful game models [92, 20, 21]. Basically, they describe positions as sets of compatible events, moves as adding an event to a position, and strategies as morphisms of games. Melliès has done significant work to give efficient proofs in particular game models with his asynchronous games [80, 82, 81, 84], which are also based on event structures.
Another exotic structure is playgrounds [50, 29, 30], which spawned the approach used in this thesis. To simplify, they are double categories (basic-ally categories with horizontal and vertical morphisms, and composition is only defined on both classes of morphisms) whose objects are positions of a game, horizontal morphisms are inclusions of positions, and vertical morphisms are plays. They must satisfy a number of properties for this to make sense as a game. From a playground, there is an abstract definition of a category E X of plays starting from the position X. Strategies are then defined as presheaves over E X , the idea being that this definition is a generalisation of the tradi-tional notion of prefix-closed sets of plays. The problem is that, to this day, it is still unknown how to compose strategies as parallel composition plus hiding. All known examples of playgrounds are part of a more general framework where plays are defined as string diagrams (which are basically formalisations of intu-itive drawings used in game semantics). In this framework, moves are defined as basic string diagrams, and plays are defined as pastings of moves. Most of the work described in this thesis is done in this string diagrammatic framework. There have been very few attempts to understand the world of game models globally. There are however a few notable exceptions. In [18], Bowler defines a general construction of game models and composition of strategies. However, he seems to be more interested in mathematical games than the ones that arise as models of programming languages. In particular, the examples he treats are those of simple games and Conway games, and he does not consider the problem of defining innocent strategies. Finally, in [48], the authors define a general framework of game models in a very close spirit to Chapter 6 of this thesis and composition of strategies abstractly, but the frameworks differs with ours on a number of fundamental points: first, the notion of morphism used there can only model prefix ordering, and second, they do not treat the case of innocent strategies.
Motivation and Contributions
The main motivation for this work was to understand the landscape of game models better. More precisely, there are many game models, some of them are very similar while others are based on completely different ideas, but there is very little literature that provides insight about the links between all these different games. Our goal was to provide insight about game models, mainly through abstraction: we have tried to find properties that are verified in different game models and abstract them away to create classes of models that verify these properties, and to prove properties for all models of that class. A characteristic feature of our approach, other than abstraction, is our extensive use of advanced categorical tools, which makes constructions and proofs more streamlined and efficient. In this matter, we have benefited from previous work in the same spirit, namely the recent recasting of strategies as presheaves, and of innocence as a sheaf condition, enabled by Melliès’s notion of morphisms between plays. A key tool that we introduce for the first time in game semantics is the theory of exact squares [45], which proves very efficient in Chapters 5 and 6.
Main Contributions
We here give the main results of each of the contributions that will be discussed in this thesis. Each contribution is given a longer section dedicated to detailing its results and the methods developed to prove them just below.
Fibred Models Our first contribution follows the pattern of abstraction ex-plained above and is discussed in Chapter 4. All known instances of string diagrammatic models (one for CCS [50], one for the π-calculus [29], one for HON games, which we study in Chapter 5, and an unpublished one for the join-calculus [36]) follow the same construction: they first define positions as some kind of graphs, then moves as higher-dimensional arrows, and finally plays as composites of moves. We call such positions and plays string diagrams, because they formalise the drawings physicists call so. A crucial property to be able to define a category of plays starting from a fixed position is fibredness, which basically states that plays can be canonically restricted to sub-positions. We first give an abstract way to build string diagrammatic models from an oper-ational description of a language that generalises previous constructions. We then give a necessary and sufficient criterion for the fibredness property to hold, and another sufficient criterion that is easier to prove. This contribution is based on [25].
A Bridge Between Models Our second main contribution is a connection between two variations on HON games, as discussed in Chapter 5. The first one [97] is based on the standard notion of justified sequence, while the second one follows the string diagrammatic approach developed in our previous contri-bution. There is an obvious, yet informal link between both models in the sense that they both define innocent strategies as sheaves for a Grothendieck topo-logy induced by embedding views into plays. We show that this relationship can actually be tightened: they are equivalent in the sense that they yield equi-valent categories of innocent strategies. We first try to give a slightly informal argument, based on derivation trees in an ad hoc sequent calculus describing HON games, and then give a direct, formal proof, without using derivation trees. This contribution is based on [26] (which explains the argument using derivation trees) and its extended version [25] (which gives the direct proof).
A Core of Game Models Our last main contribution, which we discuss in Chapter 6, is the development of a general framework to study game models. The idea is to try to boil down game models to a few basic properties about their plays, and to derive the main constructions of game models from these basic properties. Starting from a structure that represents plays, we show how to define a notion of concurrent strategy and how to compose them by parallel composition plus hiding. We show that, under some mild conditions, composi-tion of strategies is associative and unital. Under further assumptions, we show how to define a category of innocent concurrent strategies. We also show that this framework encompasses many existing game models. This contribution is based on [28].
Contributions Not Discussed in This Thesis
Let us finally mention a few contributions that will either not be detailed in this thesis or only used as examples.
String Diagrams for Concurrent Traces and Unfolding The first such contribution is Chapter 3, which is based on [24], and which we use as an introduction to string diagrams, which are extensively used in Chapters 4 and 5. We show how they can be used to model concurrent traces in a simple way, give a few examples this construction applies to, and illustrate it on the example of Petri nets. A Game Model of the π-calculus In [29] and its extended version [30], we build a model for the π-calculus that is intensionally fully abstract for fair test-ing equivalence (intensional full abstraction is simply denotational completeness, with the idea that an extensional collapse of the model gives a fully-abstract model, which is necessary in some cases as some abstract models have no re-cursively enumerable presentation [74]). We first define a notion of play based on string diagrams for the π-calculus (this is actually the example we use in Chapter 4) and show how to interpret terms as strategies. To show that this interpretation is intensionally fully abstract, we appeal to the theory of play-grounds, from which we abstractly derive an LTS for our notion of strategy and relate it to that of the π-calculus. Many ideas present in Chapter 4 come from this paper, in particular the use of factorisation systems to prove fibredness.
Interpreting Terms as Strategies Abstractly In [27], we study the in-terpretation of terms into strategies in game models from an abstract point of view. The idea is to define a broad notion of paraterm into which views, plays, and terms can all be embedded. We can then abstractly define the inter-pretation of terms as innocent strategies as a singular functor, which abstracts some previous interpretations. We then recover a fundamental result of game semantics, known as definability (which states that all finite innocent strategies are isomorphic to the image of a value), under the form of geometric realisation.
Fibred Models
In Chapter 4, we show how to create string diagrammatic models and show that they are fibred under some conditions. We start from a base category C describing the operational semantics of a language. This base category comes with a notion of dimension. Objects of lower dimensions are called players and channels and describe positions of the game, which are basically graphs of players and channels. Players are the agents of the game and channels are the means by which they can communicate. For example, in the π-calculus, a position simply represents the topology of communication between agents, as in: which represents a position with two players x and y who can communicate through the channel a, and x knows a private channel c. Objects of higher dimension describe the dynamics of the game. For example, in the π-calculus, a synchronisation where x sends c on a and y receives it is drawn as on the left below.
Here, the initial position of the synchronisation is drawn at the bottom, the final position at the top, and we can see that, in the final position, the avatar y′ of y knows the channel c that x has sent them. For the π-calculus, synchronisation corresponds to an object of higher dimension in the category C. Each object of higher dimension of C is assigned such a drawing, which we call a move. We further call the assignment of all these moves a signature. A play is a composite (pasting) of such moves. Formally, positions are presheaves over the first two dimensions of C (this is formal because the drawings represent the categories of elements of the objects of C). Moves are cospans Y → M ← X of presheaves over C, where X is the initial position, Y is the final position, and M represents the move. For example, the cospan corresponding to the synchronisation in the π -calculus is drawn next to it, with X at the bottom, Y at the top, M in the middle, and the morphisms are inclusions.
From any signature S, we build a pseudo double category DS, which, to simplify, is a gadget that has a set of objects (here, positions), and for all objects X and Y , a set of horizontal morphisms X → Y (here, inclusions of X into Y ) and a set of vertical morphisms Y X (here, plays starting from X and ending in Y ). It also has, for all perimeters as below, a set of cells α (which here represents the fact that u embeds into u′ in a certain sense).
A Bridge Between Models
In Chapter 5, we start by building a string diagrammatic approach to HON games as explained in 1.3.1 and then exhibit links between this model and an-other one (based on the standard notion of justified sequence) both at the level of plays and at the level of strategies. We start from a sequent calculus that de-scribes arena games, strongly reminiscent of a focalised calculus for intuitionistic logic. From this sequent calculus, we derive a signature SHON that describes HON games. Here, channels are games on which two players play. We draw channels as edges and players as nodes, and the positions typically look like A x B y C , where, in this particular position, x plays as Proponent on B and Opponent on A, and y as Proponent on C and Opponent on B. The dangling arrows represent interaction with the environment. This could typically model the composition of a function of type A → B, modelled by x, and one of type B → C, modelled by y. Players that have only incoming edges are morally the program fragments that are currently computing something, while the ones with an outgoing edge are waiting for another program fragment to call them (on that outgoing edge).
Table of contents :
1 Introduction
1.1 Semantics of Programming Languages
1.1.1 An (Outdated) Map of Semantics
1.1.2 Semantics Today
1.2 Game Semantics
1.2.1 The Birth of Game Semantics
1.2.2 The Rich World of Game Models
1.3 Motivation and Contributions
1.3.1 Fibred Models
1.3.2 A Bridge Between Models
1.3.3 A Core of Game Models
2 Preliminaries
2.1 Game Semantics
2.1.1 Hyland-Ong/Nickau Games
2.1.2 Variations on HON Games
2.1.3 Tsukada and Ong’s Model
2.1.4 Abramsky-Jagadeesan-Malacaria Games
2.1.5 Blass Games
2.2 Categorical Preliminaries
2.2.1 Comma and Cocomma Categories
2.2.2 Fibrations
2.2.3 Ends and Coends
2.2.4 Kan Extensions
2.2.5 Presheaf Categories
2.2.6 Exact Squares
2.2.7 Sheaves
2.2.8 Factorisation Systems
2.2.9 Pseudo Double Categories
3 Presheaves and Concurrent Traces
3.1 Introduction
3.2 From Signatures to Pseudo Double Categories
3.2.1 Signatures and Positions
3.2.2 Execution Steps and Traces
3.2.3 Organising Traces into a Pseudo Double Category
3.2.4 The Category of Execution Traces
3.3 Unfolding
3.4 Perspectives
4 Pseudo Double Categories and Concurrent Game Models
4.1 Motivation
4.2 Preliminaries
4.3 Signatures for Pseudo Double Categories
4.3.1 A Signature for the -Calculus
4.3.2 Signatures
4.3.3 From Signatures to Pseudo Double Categories
4.3.4 Fibredness and Categories of Plays
4.4 Fibredness
4.4.1 Fibredness through Factorisation Systems
4.4.2 A Little Theory of 1D-Pullbacks and 1D-Injectivity
4.4.3 A Necessary and Sufficient Fibredness Criterion
4.4.4 Cartesian Lifting of Seeds
4.5 Perspectives
5 Justified Sequences in String Diagrams
5.1 Motivation
5.2 HON Games as String Diagrams
5.2.1 Building the Pseudo Double Category
5.2.2 Categories of Views and Plays
5.2.3 Characterisations of Views and Plays
5.3 The Level of Plays: Intuition
5.3.1 Illustration on an Example
5.3.2 From String Diagrams to Proof Trees
5.3.3 From Proof Trees to Justified Sequences
5.4 The Level of Plays: Formal Proof
5.4.1 Constructing the Functor
5.4.2 Full Faithfulness
5.4.3 Restriction to Views
5.5 The Level of Strategies
5.6 Perspectives
6 Composing Non-Deterministic Strategies
6.1 Motivation
6.1.1 The Main Ideas
6.1.2 A Technical Point
6.2 Polynomial Functors for Abstract Game Semantics
6.2.1 Plays as a Category-Valued Presheaf
6.2.2 Copycats and Composition as Polynomial Functors
6.2.3 Game Settings, Associativity and Unitality
6.2.4 The Boolean Case
6.3 Applications
6.3.1 Hyland-Ong/Nickau Games
6.3.2 Constraining Strategies
6.3.3 AJM Games: a Partial Answer
6.3.4 A Non-Example: Blass Games
6.4 Innocence
6.4.1 Concurrent Innocence
6.4.2 Prefix-Based Innocence
6.4.3 Boolean Innocence
6.5 Perspectives
A A Proof of View-Analyticity in Tsukada and Ong’s Model
