Anzeige
Erschienen in:
2009 | OriginalPaper | Buchkapitel
Thick Subtrees, Games and Experiments
verfasst von : Pierre Boudes
Erschienen in: Typed Lambda Calculi and Applications
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
We relate the dynamic semantics (games, dealing with interactions) and the static semantics (dealing with results of interactions) of linear logic with polarities, in the spirit of Timeless Games [1].
The polarized game semantics is full and faithfull for polarized proof-nets [2]. We detail the correspondence between cut free proof-nets and innocent strategies, in a framework related to abstract Böhm trees.
A notion of thick subtree allows us to reveal a deep relation between plays in games and Girard’s experiments on proof-nets. We then define a desequentializing operation, forgetting time in games which coincides with the usual way of computing a result of interaction from an experiment. We then obtain our main result: desequentializing the game interpretation of a polarized proof-net yields its standard relational model interpretation (static semantics).