基于索引线性逻辑的MALL交互几何
摘要：多项式加法线性逻辑（MALL）的交互几何构造（GoI：Gentzen风格的cut消除的动态建模）的建立，通过采用Bucciarelli-Ehrhard索引线性逻辑MALL（I）来处理添加项。我们的构造是对Haghverdi-Scott范畴化形式的添加项的扩展，该形式是Girard原始GoI的多项式交互几何情境（在追踪的幺半范畴中）。指标显示不仅在其原始指示级别上起作用，而且在更精细的动态级别上也起作用，以便通过显式使用指标来处理添加项的消去证明的特殊性，例如叠加、子证明抹消和添加（协）收缩。证明在范畴Rel中被解释为具有索引的子集，但没有显式的关系合成；相反，执行公式在每个索引的解释上以点方式运行，与剪切的对称性相关，在具有自反对象和零态射的追踪幺半范畴中运行。当执行公式运行时，索引集总体减少，对应于添加切除消除过程（消去），并允许恢复关系组合。主要定理是执行公式在切消消除过程中的不变性，使得公式收敛到（无切割）证明的指示。
作者：Masahiro Hamano
论文ID：1704.02711
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-22