Samuel Mimram (CEA Saclay), A polygraphic presentation of first-order causality
Schedule
- Feb. 28, 2012, 15:00 - 16:00
Abstract
Game semantics aims at describing the interactive behaviour of proofs (for instance in first-order logic) by interpreting formulas as games on which proofs induce strategies. One of the main difficulties that has to be faced when constructing such semantics is to make them precise by characterizing definable strategies - that is strategies which actually behave like a proof. This characterization is usually done by restricting to the model to strategies satisfying subtle combinatory conditions such as innocence, whose preservation under composition is difficult to show. Here, we present an original methodology to achieve this task which requires to combine tools from game semantics, rewriting theory and categorical algebra. We introduce a diagrammatic presentation of definable strategies by the means of generators and relations: those strategies can be generated from a finite set of ``atomic'' strategies and that the equality between strategies generated in such a way admits a finite axiomatization, which is a variation of bialgebra laws.
Game semantics aims at describing the interactive behaviour of proofs (for instance in first-order logic) by interpreting formulas as games on which proofs induce strategies. One of the main difficulties that has to be faced when constructing such semantics is to make them precise by characterizing definable strategies - that is strategies which actually behave like a proof. This characterization is usually done by restricting to the model to strategies satisfying subtle combinatory conditions such as innocence, whose preservation under composition is difficult to show. Here, we present an original methodology to achieve this task which requires to combine tools from game semantics, rewriting theory and categorical algebra. We introduce a diagrammatic presentation of definable strategies by the means of generators and relations: those strategies can be generated from a finite set of ``atomic'' strategies and that the equality between strategies generated in such a way admits a finite axiomatization, which is a variation of bialgebra laws.