Drawing inspiration from linear logic, quantitative semantics aim at representing quantitative information about programs and their executions: they include the relational model and its numerous extensions, game semantics, and syntactic approaches such as non-idempotent intersection types and the Taylor expansion of lambda-terms. The crucial feature of these models is that programs are interpreted as witnesses which consume bags of resources.

Bags are often taken to be finite multisets, i.e. quotiented structures. Another approach typically seen in categorifications of the relational model is to work with unquotiented structures (e.g. sequences) related with explicit morphisms referred to here as symmetries, which express the exchange of resources. Symmetries are obviously at the core of these categorified models, but we argue their interest reaches beyond those --- notably, symmetry leaks in some non-categorified quantitative models (such as the weighted relational model, or Taylor expansion) under the form of numbers whose combinatorial interpretation is not always clear.

In this work, we build on a recent bicategorical model called thin spans of groupoids. Notably, thin spans feature a decomposition of symmetry into two sub-groupoids of polarized --- positive and negative --- symmetries. We first construct a variation of the original exponential of thin spans, based on sequences rather than families. Then we give a syntactic characterisation of the interpretation of simply-typed lambda-terms in thin spans, in terms of rigid intersection types and rigid resource terms. Finally, we formally relate thin spans with the weighted relational model and generalized species of structure. This allows us to show how some quantities in those models reflect polarized symmetries: in particular we show that the weighted relational model counts witnesses from generalized species of structure, divided by the cardinal of a group of positive symmetries.

This is joint work with Simon Forest.