极大交换子代数与线性逻辑片段之间的对应关系
逻辑
2016-08-03 v2 计算机科学中的逻辑
摘要
我们展示了 Jacques Dixmier 提出的极大交换子代数（MASAs）分类与线性逻辑片段之间的对应关系。为此，我们提出了一种修正的 Girard 超有限相互作用几何构造，该构造将证明解释为冯·诺依曼代数中的算子。在此模型中健全解释的逻辑的表达能力取决于作为解释参数的 MASA 的性质。我们还揭示了 MASAs 在先前相互作用几何构造中所起的关键作用。
引用
@article{arxiv.1408.2125,
title = {A Correspondence between Maximal Abelian Sub-Algebras and Linear Logic Fragments},
author = {Thomas Seiller},
journal= {arXiv preprint arXiv:1408.2125},
year = {2016}
}