基于Hughes-vanGlabbeek证明网的MALL交互几何

本文首次提出了一种受 Hughes-vanGlabbeek (HvG) 乘加线性逻辑 (MALL) 证明网启发的交互几何 (GoI) 解释。我们的 GoI 通过代数算子动态捕捉 HvG 的几何正确性判据——翻转循环条件。我们的新要素是对 Girard 的 *-环中部分等距的 *-代数进行标量扩张，该环建立在以本征权重的文字为不定元的布尔多项式环上。为了捕捉由切割产生的反馈，我们构造了一个更细粒度的执行公式。该执行公式的展开比乘性 GoI 的切片集合更长，因此更难证明终止性。我们的 GoI 对布尔赋值（特别是修剪子证明）、权重转换（特别是 α-转换）以及加性（协）收缩——这些加性证明理论特有的现象——给出了动态的语义说明。我们执行公式的终止性被证明对应于 HvG 的翻转判据。我们执行公式的按切片限制（通过折叠布尔结构）产生了先前乘性 GoI 工作中显式或隐式存在的著名对应关系，即执行公式的收敛与证明网的无环性之间的对应。通过限制到布尔多项式结构由执行公式产生的反馈，给出了切割间本征权重相对于其余本征权重的自主可定义性。