一句话:首次为经典形式的微分线性逻辑建立博弈语义,并揭示其与同伦论的意外联系。
该论文研究微分线性逻辑(DiLL)的语义模型,特别是为其经典形式构造博弈语义,这是博弈语义中长期未决的问题。作者将其此前的乘法加性线性逻辑(MALL)模板博弈模型扩展到含指数模态的情形,指数模态由自由对称幺半范畴的标准构造 Sym 导出。构造过程中,作者与 Fiore、Gambino、Hyland 和 Winskel 十年前提出的广义物种(generalised species)模型进行了细致比较。结果不仅首次给出了 DiLL 经典形式的博弈语义,解决了旧开问题,还意外揭示出线性逻辑与同伦理论之间富有前景的收敛。
We extend our recent template game model of multiplicative additive linear logic (MALL) with an exponential modality of linear logic (LL) derived from the standard categorical construction Sym of the free symmetric monoidal category. We obtain in this way the first game semantics of differential linear logic (DiLL) in its classical form. The construction of the model relies on a careful and healthy comparison with the model of generalised species designed ten years ago by Fiore, Gambino, Hyland and Winskel. Besides the resolution of an old open problem of game semantics, the study reveals an unexpected and promising convergence between linear logic and homotopy theory.