Thomas Seiller (Chambéry, France), Graphs of Interaction
Schedule
- Feb. 8, 2012, 16:45 - 17:30
Abstract
Graphs of Interaction are a generalization of the very first version of geometry of interaction defined by Girard in his article "Multiplicatives" by replacing permutations with directed weighted graphs. In this setting, it is possible to define a notion orthogonality, parametrized by a "measure" on cycles, by counting the cycles that appear when one plugs two graphs together. With such a notion of orthogonality, one can then construct a denotational model for multiplicative additive linear logic (MALL) and define a notion of truth.
Moreover it can be shown that two particular choices of "measure" maps define either a combinatorial version of Girard's geometry of interaction in the hyperfinite factor (GoI5) or a slightly refined version of the older "Geometry of Interaction I" where orthogonality is defined by nilpotency. Thus, this framework gives a geometrical interpretation to GoI5's orthogonality (which is based on the determinant), and shows how one can relate this new construction with the first versions of geometry of interaction.
Graphs of Interaction are a generalization of the very first version of geometry of interaction defined by Girard in his article "Multiplicatives" by replacing permutations with directed weighted graphs. In this setting, it is possible to define a notion orthogonality, parametrized by a "measure" on cycles, by counting the cycles that appear when one plugs two graphs together. With such a notion of orthogonality, one can then construct a denotational model for multiplicative additive linear logic (MALL) and define a notion of truth.
Moreover it can be shown that two particular choices of "measure" maps define either a combinatorial version of Girard's geometry of interaction in the hyperfinite factor (GoI5) or a slightly refined version of the older "Geometry of Interaction I" where orthogonality is defined by nilpotency. Thus, this framework gives a geometrical interpretation to GoI5's orthogonality (which is based on the determinant), and shows how one can relate this new construction with the first versions of geometry of interaction.