微分线性逻辑的同伦跨度模型的显式洗牌构造
An explicit shuffle construction of the homotopy span model of differential linear logic
- CNRS, Université Paris Cité, Inria（法国国家科学研究中心、巴黎西岱大学、法国国家信息与自动化研究所）
- Aix Marseille Univ, CNRS, LIS（艾克斯-马赛大学、法国国家科学研究中心、信息系统实验室）
- Aix Marseille Univ, CNRS, I2M（艾克斯-马赛大学、法国国家科学研究中心、数学与建模研究所）
机构由 AI 辅助整理，请以论文原文为准。
AI总结：
该研究在奎伦范畴Cat中显式构造了微分线性逻辑的同伦跨度模型，将证明的解释放宽为独立纤跨，以洗牌结构捕获指数模态对称性，简化了模型描述。
AI中文摘要：
我们使用配备自然模型结构的小范畴的奎伦范畴Cat中的抽象同伦论，给出了Melliès最初提出的线性逻辑的同伦跨度模型的直接且显式的构造。遵循同伦论的原理，线性逻辑的公式和证明在该模型中被解释为小范畴（相对于范畴等价，这是Cat上自然奎伦模型结构下的弱同伦等价概念）。在此，我们解释如何将证明作为纤跨的原始解释替换为更宽松的证明作为独立纤跨的解释。这种从纤跨到独立纤跨的放宽，使我们能够给出同伦跨度模型的简单直观描述：公理和切连被解释为恒等跨度，指数模态的对称性由证明解释上的洗牌结构捕获。
英文摘要：
We give a direct and explicit construction of the homotopy span model of linear logic originally formulated by Melliès using abstract homotopy theory in the Quillen category Cat of small categories equipped with its natural model structure. Following the principles of homotopy theory, the formulas and proofs of linear logic are interpreted in the model as small categories up to categorical equivalence, the notion of weak homotopy equivalence underlying the natural Quillen model structure on Cat. Here, we explain how the original interpretation of proofs as fibrant spans can be replaced by a more liberal interpretation of proofs as separately fibrant spans. This relaxation from fibrant spans to separately fibrant spans enables us to give a simple and intuitive description of the homotopy span model, where the axiom and cut links are interpreted as identity spans, and where the symmetries of the exponential modality are captured by a shuffle structure on the interpretation of proofs.
