Game semantics

In the early 90s, I adapted Lorenzen's game semantics of logic to give a "geometrical" description of what is going on during cut elimination (interaction between two strategies), obtaining a proof of termination which I believe is essentially different from the one of Gentzen. This introduced the notion of pointer sequence and visibility, which was used later in game semantics of simply typed lambda calculus. The termination argument, published in the proceeding of CLICS 92, was used in P.-L. Curien's paper Abstract Bohm trees , MSCS 8 (1998), to present a general termination argument about abstract machine evaluation of lambda terms (it is not known yet if there is a more direct argument for this termination result). The same argument was then used later in a paper of P. Clairambault and R. Harmer on Totality in Arena Games.

I tried to present a general survey in this talk; in particular, I mention S. Berardi's discovery that the notion of visibility can be extended for infinite games.

Stefano Berardi wrote also some description of this approach with more references.

One can also generalize the game to allow the strategy to play with functions, that are thought of as stating general laws that can be refined by interaction. One gets in this way a natural computational interpretation of dependent choice with classical logic. This was actually Spector's starting point, and similar attempts can be found in the notebooks of Gödel. Using this game semantics, I suggested a realizability interpretation of countable choice. The following paper is an example of what can be done in this direction.

This interpretation has been used by F. Aschieri in this paper where he provides a remarkable refinement of Gentzen's bounds for cut-elimination: the complexity depends on the depth of backtracking of the two interacting strategies.


Last modified: Fri Sep 13 22:08:32 MET DST 2002