并行削减在乘法线性逻辑中的应用：对证明网络的泰勒展开
摘要：平行切割消除在乘法线性逻辑（MLL）证明网络中具有一些组合特性。我们显示，只要对某些路径施加约束，我们就可以限定满足这一约束且归约为固定结果网络的所有网络的大小。该结果为无限权重和的网络归约为另一和的网络提供了充分条件，同时保持系数有限。此外，我们还显示我们的约束在归约下是稳定的。 我们的方法受到线性逻辑的定量语义的启发：已经提出了许多模型，其结构反映了乘法指数线性逻辑（MELL）证明网络在无限级数差分网络和中的泰勒展开。为了模拟MELL中的一次切割消除步骤，需要归约其泰勒展开的差分网络中的任意数量的切割。 我们的结果适用于差分网络，因为它们的切割消除本质上是乘法的。此外，我们还显示在MELL网络的泰勒展开中出现的差分网络集自动满足我们的约束。 有趣的是，我们的网络没有类型：我们仅依赖线性逻辑网络的按顺序性和切割消除的动力学。我们对其施加约束的路径是与Danos-Regnier顺序性准则相关的切换路径。为了适应乘法单位和弱化，我们的网络带有跳跃：每个弱化节点都与某些其他节点连接。因此，我们的约束可以总结为对切换路径的长度和跳跃到共同节点的弱化数量的限制。
作者：Jules Chouquet and Lionel Vaux Auclair
论文ID：1902.05193
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-22