Mackey 完备空间与幂级数——微分线性逻辑的一个拓扑模型
计算机科学中的逻辑
2015-07-14 v1
摘要
本文描述了一个直觉主义线性逻辑的指称模型，该模型同时也是一个微分范畴。公式被解释为 Mackey 完备的拓扑向量空间，线性证明被解释为有界线性函数。为了解释线性逻辑的非线性证明，我们使用了 Mackey 完备空间之间的幂级数概念，推广了 C 中的整函数概念。最终，我们得到了直觉主义微分线性逻辑的一个量化模型，其中语法上的微分对应于通常的微分，且证明的解释满足 Taylor 展开分解。
引用
@article{arxiv.1507.03262,
title = {Mackey-complete spaces and power series -- A topological model of Differential Linear Logic},
author = {Marie Kerjean and Christine Tasson},
journal= {arXiv preprint arXiv:1507.03262},
year = {2015}
}