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