交互图：完全线性逻辑
计算机科学中的逻辑
2016-05-10 v2 逻辑
摘要
交互图是作为线性逻辑动态模型的一种通用、统一的构造而引入的，它包含了迄今为止所有提出的 "Geometry of Interaction" (GoI) 构造。这一系列工作受 Girard 的超有限 GoI 启发，并发展了一种量化方法，应被理解为加权关系模型的动态版本。迄今为止，交互图框架已被证明能处理约束系统 ELL（初等线性逻辑）的指数，同时保持其量化方面。通过改编 Girard 较早的构造，可以清晰地定义 "full" 指数，但代价是失去这些量化特征。我们在此表明，允许证明的解释使用连续的（但在测度论意义下有限的）状态集，而非早期交互图构造中离散（且有限）的状态集，为带二阶量词的完全线性逻辑提供了一个模型。
引用
@article{arxiv.1504.04152,
title = {Interaction Graphs: Full Linear Logic},
author = {Thomas Seiller},
journal= {arXiv preprint arXiv:1504.04152},
year = {2016}
}