paperbot · PL 论文追踪

全部论文 待读 收藏

P2 An Analysis of Symmetry in Quantitative Semantics

定量语义中的对称性分析
LICS Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science2024匹配度 1/10 · 论文属于纯形式语义、范畴论与类型系统,讨论定量语义中的对称性、thin spans、加权关系模型等,与用户关注的静态分析+LLM/Agent、浮点程序分析、贝叶斯程序分析无直接关联。引用 4 inbox
Pierre Clairambault, Simon Forest
crossref: 2026-09-12dblp: 2026-09-12arxiv: 2026-09-12

AI 速览

一句话:在 thin spans of groupoids 中分析定量语义的对称性,并将其与加权关系模型及 generalized species 的计数联系起来。

定量语义把程序及其执行表示为消耗资源袋的见证,资源袋常被商成有限多重集,或在未商结构(如序列)上用对称性描述资源交换。本文基于 Clairambault 与 Forest 最近提出的 thin spans of groupoids 双范畴模型,利用其将对称性分解为正、负两类极化子群胚的结构,构造以序列而非族为基础的指数变体。随后给出简单类型 λ-项在 thin spans 中的句法刻画,使用刚性交类型与刚性资源项。最后,作者将 thin spans 与加权关系模型及 generalized species of structure 形式关联,说明这些模型中的某些量如何反映极化对称性;例如加权关系模型计数的是 generalized species 的见证除以正对称群的基数。

问题
定量语义将程序解释为消耗资源袋的见证,但资源袋的商结构(多重集)与未商结构(序列/对称性)之间的关系,以及对称性如何渗入非范畴化模型并影响计数,仍缺乏清晰理解。
方法
在 thin spans of groupoids 双范畴模型上构造基于序列的指数变体,给出简单类型 λ-项的刚性交类型与刚性资源项句法刻画,并建立其与加权关系模型和 generalized species of structure 的联系。
评估
以理论构造和模型间关系证明为评估方式,展示加权关系模型等模型中的计数可解释为 generalized species 见证数除以正对称群基数。
原文摘要(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 nonidempotent intersection types and the Taylor expansion of λ-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 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 λ-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.

链接与引用

DOI 原文 · arXiv · PDF(开放获取) · DBLP

BibTeX
@inproceedings{ClairambaultF24,
  title = {An Analysis of Symmetry in Quantitative Semantics},
  author = {Pierre Clairambault and Simon Forest},
  booktitle = {LICS},
  year = {2024},
  doi = {10.1145/3661814.3662092}
}