From Dynamic to Static Semantics, Quantitatively

TL;DR

This paper establishes a formal connection between dynamic and static semantics through categorical models, introducing interaction graphs as a quantitative bridge related to game semantics and coherence spaces.

Contribution

It defines a categorical framework for interaction graphs models, linking them to weighted relational models and quantitative coherence spaces, thus bridging dynamic and static semantics.

Findings

Interaction graphs models relate to weighted relational models.

A categorical framework for dynamic-static semantics connection.

Interaction graphs serve as quantitative versions of GoI and game semantics.

Abstract

We exhibit a new relationship between dynamic and static semantics. We define the categorical outlay needed to define Interaction Graphs models, a generalisation of Girard's Geometry of Interaction models, which strongly relate to game semantics. We then show how this category is mapped to weighted relational models of linear logic. This brings into vision a new bridge between the dynamic and static approaches, and provides formal grounds for considering interaction graphs models as quantitative versions of GoI and game semantics models. We finally proceed to show how the interaction graphs models relate to a very general notion of quantitative coherence spaces.