一句话：引入以 SMCC 加权的广义 species/profunctor，证明其构成 Lafont 范畴，并统一线性逻辑与多类编程语言的定量模型。
本文受 Joyal 组合 species 与线性逻辑定量模型之间紧密联系的启发，引入加权广义 species（加权 profunctor），其权重取自定义在给定对称幺闭范畴（SMCC）中的态射。作者证明：对任意 SMCC W，W-加权 profunctor 构成的范畴是 Lafont 范畴，即带指数的线性逻辑的范畴模型。作为编程语言模型，该构造通过选择不同的权重 SMCC，给出统一框架，可诱导非确定性、概率、代数与量子编程语言的 adequate 模型。关键贡献是范畴论层面的构造与表示定理，以及对该统一建模框架的建立。
Motivated by a tight connection between Joyal's combinatorial species and quantitative models of linear logic, this paper introduces weighted generalised species (or weighted profunctors), where weights are morphisms of a given symmetric monoidal closed category (SMCC). For each SMCC W, we show that the category of W-weighted profunctors is a Lafont category, a categorical model of linear logic with exponential. As a model of programming languages, the construction of this paper gives a unified framework that induces adequate models of nondeterministic, probabilistic, algebraic and quantum programming languages by an appropriate choice of the weight SMCC.
DOI 原文 ·
@inproceedings{paperbot4369,
title = {Species, Profunctors and Taylor Expansion Weighted by SMCC},
author = {Takeshi Tsukada and Kazuyuki Asada and C.-H. Luke Ong},
booktitle = {LICS},
year = {2018},
doi = {10.1145/3209108.3209157}
}