Sequentiality vs. Concurrency in Games and Logic

Samson Abramsky

We use games and Logic as a mirror to understand an aspect of the
sequentiality/concurrency distinction. We begin with the simple,
intuitive notion of *polarized games* due to Blass, which prefigured
many of the ideas in Linear Logic, and which can be seen as a polarized
version of ideas familiar from process calculi (synchronization trees,
prefixing, summation, the Expansion theorem). We analyze the `shocking'
fact that this very clear and intuitive idea leads to a non-associative
composition; a kind of incompatibility between a purely sequential model
and logic in a classical format. Two ways of addressing this issue have
been found. One is to add an explicit (`non-logical') polarity-flipping
operation, and use the resulting model to interpret a
`hyper-sequentialized' version of sequent calculus, in which the current
focus of attention in the proof is explicitly represented. This is the
approach taken in Girard's Ludics. The other is to broaden the notion of
game to encompass `truly concurrent games'. In such games there is no
longer a global polarization (we can have positions in which both papers
can move concurrently), although there are still local polarizations
(each local decision is made by just one of the players). This idea of
concurrent games was used by Abramsky and Mellies to give a fully
complete model for Linear Logic in its original form (i.e. not
`hyper-sequentialized'), and indeed the correspondence is with
proof-nets, the `parallel syntax for proof theory' in Girard's phrase.