The first paper I ever read on game semantics was Samson Abramsky & Guy McCusker’s “Linearity, Sharing and State“. It was included in a great collection of papers on Algol-like Languages by Bob Tennent, my PhD advisor, and Peter O’Hearn and it was the basic background reading for my research. The game semantics paper was intriguing for two reasons. First, it was provably the most precise model of Algol to date, solving a long-standing open problem in theoretical Computer Science. Second, I didn’t understand anything from the paper. Most of the papers in that book are of course highly technical, but beyond the technicalities you could grasp intuitively features of the model which captured elegantly various aspects of the language. The Game Semantics seemed to be a lot of technicalities leading to a technical result, bereft of computational or operational intuitions.
I was in Canada at the time but, luckily, I was about to travel to the UK and had a chance to meet Guy who agreed to meet me and teach me about game semantics, and it turned out it leads to incredibly intuitive models of programming languages. I became fascinated with it and I chose it as my main research topic despite the fact that Bob, my adviser, was not a researcher in the area. Luckily, he was amazingly supportive of my newfound interest.
Why is game semantics so great? The older and more established formalisms are denotational and operational semantics. A denotational model tells you what a program is, by interpreting it as a mathematical object. An operational model tells you what a program does by giving evaluation rules which tell you how the program executes, in the abstract. Each model has its uses. A denotational model is useful if you want to prove equivalences of programs, because equivalent programs have equal models. An operational model is useful as a specification for a compiler or interpreter. Technically, the main feature of a denotational model is its compositionality, which means that the meaning of a larger program is constructed mathematically from the meanings of its sub-programs. The main feature of an operational model is its effectiveness, which means that it can be encoded algorithmically — it is an executable specification for an interpreter. Conversely, a denotational semantics is not necessarily executable and an operational semantics is not usually compositional.
Game semantics manages to be both a denotational and an operational semantics: it is defined compositionally and it can be made executable. So it can tell you in one neat package both what a program is and what a program does. But the way in which describes the operation of a program is quite unusual. Conventional operational semantics shows how a program transforms in the course of execution. For example, the sequential composition of two commands will be modeled as follows.
Denotationally, a command is a function and sequential composition is compositions of functions, resulting in a new function modeling the composite command. This is written concisely like this:
Operationally, what a sequential composition does, is this: if the first command in the composition executes on computational step then the composite command executes a computational step.
If then .
You will find a large number of variations on this general pattern, depending on the language. A great tutorial on operational semantics is Andy Pitts’s.
Game semantics gives an interactive account of computation which, for historical reasons, it is called a game. First we need to establish that for a command the observable actions are starting the execution and finishing the execution. Lets call these actions R and D an emphasise that there is nothing else that a command can do.
Sequential composition has the following signature: it takes two commands as arguments and produces a command as a result. Therefore there are six actions involved in its behaviour:
- R1 – running the first command
- D1 – finishing the first command
- R2 - running the second command
- D2 - finishing the second command
- R - running the sequential composition
- D - finishing the sequential composition
I have added the tags 1-2 to distinguish different actions of the same kind. It should be now quite clear that this particular interaction is the operational meaning of sequential composition:
It reads as follows:
- start the sequential composition
- start the first command
- wait for the first command to finish
- start the second command
- wait for the second command to finish
- report the end of the sequential composition operation.
This is denotational because meanings of larger programs are constructed compositionally and can be compared as objects. This is operational because these trace-like objects can be seen as specifications of automata, which can be derived from them.
For more information see my invited tutorial paper Applications of Game Semantics: From Software Analysis to Hardware Synthesis, which appeared at LICS’09.