基于 Schwartz $\varepsilon$-积的线性逻辑模型

从将线性逻辑乘法析取解释为 Laurent Schwartz 所定义的 $\varepsilon$-积出发，我们基于通常的光滑映射数学概念构造了微分线性逻辑的若干模型。这改进了 R. Blute、T. Ehrhard 和 C. Tasson 先前基于便利光滑性仅构建直觉主义模型的结果。我们分离出一个完备性条件，称为 k-拟完备性，以及其对偶下稳定的相关概念 k-自反性，从而得到一个由 k-自反空间构成的 $*$-自洽范畴，其中张量积的对偶是 $\varepsilon$ 积的反射版本。我们将 Meise 的光滑映射定义改造为微分线性逻辑的首个模型，该模型由 k-自反空间组成。我们还在分别由 Mackey 完备 Schwartz 空间和带额外自反条件的 Mackey 完备核空间构成的范畴上，构建了两个使用便利光滑映射的线性逻辑新模型。略微改变光滑性概念，也可在同一 $*$-自洽范畴上恢复出 DiLL 的模型。全文工作中，我们处于对话范畴的框架内，其中张量积恰为 $\varepsilon$-积（无反射化）。