一句话：在乘法线性逻辑证明网中给出并行切消的路径约束，刻画 Taylor 展开无限和可归约的充分条件。
本文研究乘法线性逻辑（MLL）证明网中并行切消的组合性质。作者对 Danos–Regnier 切换路径施加约束：限制切换路径长度，并限制跳向同一结点的 weakening 数量。在此约束下，证明归约到固定结果网的网规模有界，从而给出无限加权和归约后系数保持有限的充分条件，并证明约束在归约下稳定。该工作受线性逻辑定量语义与 Taylor 展开启发：为模拟 MELL 的一步切消，需在差分网中归约多步切消；由于差分网切消本质上是乘性的，上述结果适用，且 MELL 网 Taylor 展开中的差分网自动满足约束。构造不依赖类型，仅依赖线性逻辑网的序列性与切消动态。
We examine some combinatorial properties of parallel cut elimination in multiplicative linear logic (MLL) proof nets. We show that, provided we impose a constraint on some paths, we can bound the size of all the nets satisfying this constraint and reducing to a fixed resultant net. This result gives a sufficient condition for an infinite weighted sum of nets to reduce into another sum of nets, while keeping coefficients finite. We moreover show that our constraints are stable under reduction. Our approach is motivated by the quantitative semantics of linear logic: many models have been proposed, whose structure reflect the Taylor expansion of multiplicative exponential linear logic (MELL) proof nets into infinite sums of differential nets. In order to simulate one cut elimination step in MELL, it is necessary to reduce an arbitrary number of cuts in the differential nets of its Taylor expansion. It turns out our results apply to differential nets, because their cut elimination is essentially multiplicative. We moreover show that the set of differential nets that occur in the Taylor expansion of an MELL net automatically satisfies our constraints. Interestingly, our nets are untyped: we only rely on the sequentiality of linear logic nets and the dynamics of cut elimination. The paths on which we impose bounds are the switching paths involved in the Danos--Regnier criterion for sequentiality. In order to accommodate multiplicative units and weakenings, our nets come equipped with jumps: each weakening node is connected to some other node. Our constraint can then be summed up as a bound on both the length of switching paths, and the number of weakenings that jump to a common node.
@article{paperbot1253,
title = {An application of parallel cut elimination in multiplicative linear logic to the Taylor expansion of proof nets},
author = {Jules Chouquet and Lionel Vaux Auclair},
journal = {Logical Methods in Computer Science},
volume = {Volume 17, Issue 4},
year = {2021},
doi = {10.46298/lmcs-17(4:22)2021}
}