## Pierre Clairambault (LIS, Marseille), An Analysis of Symmetry in Quantitative Semantics

### Schedule

- June 27, 2024, 10:30 - 12:00

### Abstract

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.