From Qualitative to Quantitative Semantics By Change of Base

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 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 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 R-weighted model, which is fully abstract. We relate this to existing categories of probabilistic games and slot games.