We study a class of ``wave-style'' Geometry of Interaction (GoI) lambda-models based on the category Rel of sets and relations. Wave GoI models arise when Abramsky's GoI axiomatization, which generalizes Girard's original GoI, is applied to a traced monoidal category with the categorical product as tensor, using ``countable power'' as the traced strong monoidal functor bang. 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 GoI situation, which gives rise to a rich class of strict graph models. These are models of restricted lambda-calculi in the sense of [HL99], such as Church's lambda-I-calculus and the lambda-beta-KN-calculus.
[ bib | http ]