We study the connections between graph models and “wave-style” Geometry of Interaction (GoI) λ-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 !. 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 λ-theories induced by wave-style GoI models is richer than that induced by game models.
“Wave-Style” Geometry of Interaction Models in Rel Are Graph-Like Lambda-Models
HONSELL, Furio;LENISA, Marina
2004-01-01
Abstract
We study the connections between graph models and “wave-style” Geometry of Interaction (GoI) λ-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 !. 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 λ-theories induced by wave-style GoI models is richer than that induced by game models.File | Dimensione | Formato | |
---|---|---|---|
types03.pdf
non disponibili
Tipologia:
Documento in Pre-print
Licenza:
Non pubblico
Dimensione
4.16 MB
Formato
Adobe PDF
|
4.16 MB | Adobe PDF | Visualizza/Apri Richiedi una copia |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.