From Qualitative to Quantitative Semantics

We give a general description of the transition from qualitative models of programming languages to quantitative ones, as a change of base for enriched categories. This is induced by a monoidal functor from the category of coherence spaces to the category of modules over a complete semiring $${\mathcal {R}}$$. Using the properties of this functor, we characterise the requirements for the change of base to preserve the structure of a Lafont category model of linear type theory with free exponential, and thus to give an adequate semantics of erratic PCF with scalar weights from $${\mathcal {R}}$$. Moreover, this model comes with a meaning-preserving functor from the original, qualitative one, which we may use to interpret side-effects such as state. As an example, we show that the game semantics of Idealized Algol bears a natural enrichment over the category of coherence spaces, and thus gives rise by change of base to a $${\mathcal {R}}$$-weighted model, which is fully abstract. We relate this to existing categories of probabilistic games and slot games.