de Mathématiques de Luminy
Desequentialization of games and experiments on proof-nets.
We study the comparison of dynamic semantics (games, dealing with interactions) with static semantics (dealing with results of interactions), in the spirit of Timeless Games.
We carefully analyze Laurent's polarized proof-nets (which for the game semantics is full and faithful) and we detail the precise correspondence between cut free proof-nets and innocent strategies, in a framework related to Böhm trees. We then introduce a notion of thick subtree that is used to define a desequentializing operation, forgetting time in games. This allows use to show a deep relation between plays in games and Girard's experiments on proof-nets. We then prove our main result: desequentializing the game interpretation of a polarized proof-net gives its generic static interpretation.