Thomas Seiller (INRIA-Université de Savoie, Chambery)

Interaction Graphs: the geometry behind Geometry of Interaction

Abstract: The Interaction Graphs construction gives a unified vision of the various constructions of GoI defined by Girard, while simplifying them by replacing operators acting on an infinite-dimensional Hilbert space with directed weighted graphs. Moreover, it brings to light a geometrical identity which is the sole property that support the whole construction of a geometry of interaction (GoI) for multiplicative additive linear logic (MALL). I will first define and explain the Interaction Graphs construction. This construction is founded on the cyclic property, a geometrical identity satisfied by the sets of cycles that alternate between two graphs, and is parametrized by the choice of a map that "measures" cycles. I will explain how to define a GoI for MALL in this setting, and how to derive a categorical model of multiplicative linear logic, i.e. a *-autonomous catergory, from it. The framework of interaction graphs however shares with other GoI constructions dealing with additives the issue that the connective & do not define a categorical product in the derived *-autonomous category. I will explain how this problem can be solved by defining a notion of observational equivalence, which turns out to be a congruence, and quotienting the category. I will then show how these constructions are related to Girard's various GoI construction: a first value of the parameter defines a slight refinement of the old GoI constructions (GoI1,GoI2,GoI3), while a second value defines a combinatorial version of the "geometry of interaction in the hyperfinite factor" (GoI5).