Polarized Games

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 [2]. We carefully analyze Laurent’s polarized proof-nets (which for the game semantics is full and faithful [8]) 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.

• Type: Conference
• Year: 2002
• Where: LICS
• Authors: Olivier Laurent
• Keywords: Automated Reasoning, Laurent’s Polarized Proof-nets, LICS 2002, Polarized Proof-net, Semantics