Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

An Analysis of Symmetry in Quantitative Semantics

Pierre Clairambault, Simon Forest

TL;DR

This work develops a polarized, rigid semantic framework for quantitative semantics using Thin spans of groupoids. It introduces a Sym-based exponential, yielding a cartesian closed bicategory Thin_ c, and provides a syntax-directed rigid intersection-type system that characterizes lambda-term interpretations as witnesses up to symmetry. By relating Thin to Rel, Weighted Rel, and generalized species Esp, it explains how coefficients in quantitative models arise from polarized symmetries and how witnesses decompose with respect to positive and negative symmetries. The results offer a bridge from rigid syntax to relational models, enabling a Taylor-like interpretation of simply-typed lambda-terms and paving the way for extensions to non-determinism, probabilistic, and quantum settings. Overall, polarized symmetries are shown to be fundamental in capturing quantitative behavior across multiple semantic frameworks, with Esp providing an interpretable target for coefficients.

Abstract

In this paper, we build on a recent bicategorical model called thin spans of groupoids, introduced by Clairambault and Forest. 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.

An Analysis of Symmetry in Quantitative Semantics

TL;DR

This work develops a polarized, rigid semantic framework for quantitative semantics using Thin spans of groupoids. It introduces a Sym-based exponential, yielding a cartesian closed bicategory Thin_ c, and provides a syntax-directed rigid intersection-type system that characterizes lambda-term interpretations as witnesses up to symmetry. By relating Thin to Rel, Weighted Rel, and generalized species Esp, it explains how coefficients in quantitative models arise from polarized symmetries and how witnesses decompose with respect to positive and negative symmetries. The results offer a bridge from rigid syntax to relational models, enabling a Taylor-like interpretation of simply-typed lambda-terms and paving the way for extensions to non-determinism, probabilistic, and quantum settings. Overall, polarized symmetries are shown to be fundamental in capturing quantitative behavior across multiple semantic frameworks, with Esp providing an interpretable target for coefficients.

Abstract

In this paper, we build on a recent bicategorical model called thin spans of groupoids, introduced by Clairambault and Forest. 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.
Paper Structure (77 sections, 52 theorems, 105 equations, 4 figures)

This paper contains 77 sections, 52 theorems, 105 equations, 4 figures.

Table of Contents

  1. Introduction
  2. Quotients.
  3. Rigid structures
  4. Contributions
  5. Related work
  6. Outline
  7. Thin Spans on Sequences
  8. Reminder on Thin Spans of Groupoids
  9. Uniformity
  10. Spans
  11. Morphisms of spans
  12. Thinness
  13. Thin spans
  14. Positive weak morphisms
  15. The $\mathbf{Sym}$ Exponential on $\mathbf{Thin}$
  16. ...and 62 more sections

Key Result

lemma 1

For any $\theta : a \cong_A a'$ in a thin groupoid $A$, there are unique $a" \in A$ and $\theta^+ : a \cong_A^+ a"$, $\theta^- : a" \cong_A^- a'$s.t.$\theta = \theta^- \circ \theta^+$.

Figures (4)

  • Figure 1: Intersection types and approximation
  • Figure 2: The rules for rigid intersection type morphisms
  • Figure 3: The definition of $\partial^-(\pi)$
  • Figure 4: The definition of composition of intersection type morphism derivations

Theorems & Definitions (58)

  • definition 1: DBLP:conf/lics/ClairambaultF23
  • definition 2: DBLP:conf/lics/ClairambaultF23
  • lemma 1
  • lemma 2
  • lemma 3
  • definition 3
  • theorem 1: DBLP:conf/lics/ClairambaultF23
  • theorem 2
  • theorem 3
  • theorem 4
  • ...and 48 more