交互图：加法
计算机科学中的逻辑
2015-10-14 v5 逻辑
摘要
几何交互(GoI)是一种线性逻辑证明的语义，旨在解释消割的动态方面。我们在此提出一个参数化的几何交互构造，用于乘法加法线性逻辑(MALL)，其中证明由有向加权图族表示。与以前处理加法连接词的构造相反，我们通过引入观测等价的概念解决了为MALL获得指称语义的已知问题。此外，我们的设置具有第一个处理加法连接词且MALL证明由有限对象解释的构造的优点。我们获得MALL的指称模型依赖于一个单一的几何性质，我们称之为三叶草性质，由此我们为每个参数值获得伴随。然后我们展示这个设置如何与Girard的各种构造相关：参数的特定选择分别给出他最新GoI的组合版本，以及基于幂零性的更早几何交互的改进版本。这表明了三叶草性质在我们构造中的重要性，因为迄今为止所有已知的GoI构造都依赖于它的特例。
引用
@article{arxiv.1205.6557,
title = {Interaction Graphs: Additives},
author = {Thomas Seiller},
journal= {arXiv preprint arXiv:1205.6557},
year = {2015}
}