代数总体性，走向完备性
Algebraic totality, towards completeness
摘要：
线性空间构成了线性逻辑的范畴模型，其对象可以被看作线性拓扑空间（Lefschetz在1942年引入的一类拓扑向量空间）和连续线性映射的态射。首先，我们回顾有限性空间的定义，并描述其基本性质推导出的一般理论的线性拓扑空间。然后，我们给出了一个基于线性代数的解释LL。其次，由于分离性质，我们可以在线性拓扑空间的框架中引入一个代数概念的总体候选：一个总体候选是一个不包含0的闭仿射子空间。我们表明，有限性空间的总体候选人构成一个模型的经典LL。最后，我们给出了一个重心简单类型的布尔型演算${\mathcal{B}}$和一个条件算子，它可以在这个模型中解释。我们证明了完备性类型${\mathcal{B}}^n\to{\mathcal{B}}$的任何n的代数方法。
英文摘要：
Finiteness spaces constitute a categorical model of Linear Logic (LL) whose objects can be seen as linearly topologised spaces, (a class of topological vector spaces introduced by Lefschetz in 1942) and morphisms as continuous linear maps. First, we recall definitions of finiteness spaces and describe their basic properties deduced from the general theory of linearly topologised spaces. Then we give an interpretation of LL based on linear algebra. Second, thanks to separation properties, we can introduce an algebraic notion of totality candidate in the framework of linearly topologised spaces: a totality candidate is a closed affine subspace which does not contain 0. We show that finiteness spaces with totality candidates constitute a model of classical LL. Finally, we give a barycentric simply typed lambda-calculus, with booleans ${\mathcal{B}}$ and a conditional operator, which can be interpreted in this model. We prove completeness at type ${\mathcal{B}}^n\to{\mathcal{B}}$ for every n by an algebraic method.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
