Strict Geometry of Interaction Graph Models

We study a class of "wave-style" Geometry of Interaction (Gol) λ-models based on the category Rel of sets and relations. Wave Gol models arise when Abramsky's Gol axiomatization, which generalizes Girard's original Gol, is applied to a traced monoidal category with the categorical product as tensor, using "countable power" as the traced strong monoidal functor!. Abramsky hinted that the category Rel is the basic setting for traditional denotational "static semantics". However, Rel, together with the cartesian product, apparently escapes Abramsky's original GoI construction. Here we show that Rel can be axiomatized as a strict GoI situation, i.e. a strict variant of Abramsky's Gol situation, which gives rise to a rich class of strict graph models. These are models of restricted λ-calculi in the sense of [HL99], such as Church's λ-I-calculus and the AβKN-calculus.