F.Honsell and M. Lenisa. Wave-style geometry of interaction models in rel are graph-like lambda models. In Proceedings of TYPES'03, Lecture Notes in Computer Science. Springer Verlag, 2003.

We study the connections between graph models and ``wave-style'' Geometry of Interaction (GoI) lambda-models. The latters 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 a countable power as the traced strong monoidal functor bang. Abramsky hinted that the category Rel of sets and relations is the basic setting for traditional denotational ``static semantics''. However, the category Rel together with the cartesian product apparently escapes original Abramsky's axiomatization. Here we show that, by moving to the category Rel* of pointed sets and relations preserving the distinguished point, and by sligthly relaxing Abramsky's GoI axiomatization, we can recover a large class of graph-like models as wave models. Furthermore, we show that the class of untyped lambda-theories induced by wave-style GoI models is richer than that induced by game models.

[ bib | http ]

Back