驯服模态不可预测性：超惰性约简
Taming Modal Impredicativity: Superlazy Reduction
摘要：
纯的或无类型的线性逻辑证明网是图灵完备的，一旦割消被认为是计算。我们引入模态不可预测性作为不可预测性的一种新形式，从复杂性的角度来看，导致割消的复杂性是有问题的。模态不可预测性发生在当在约简期间，盒子b的残差的结论与属于b的另一个残差内的证明网的节点相互作用时。从技术上讲，超级惰性归约是一种新的归约概念，允许控制模态不可预测性。更具体地说，superlazy reduction仅在所有副本都打开时才复制一个盒子。这使得减少证据网的总成本是有限的和可预测的。具体来说，应用于任何纯证明网的超惰性归约都需要原始递归时间。此外，任何原始递归函数都可以通过超惰性归约由纯证明网计算。
英文摘要：
Pure, or type-free, Linear Logic proof nets are Turing complete once cut-elimination is considered as computation. We introduce modal impredicativity as a new form of impredicativity causing the complexity of cut-elimination to be problematic from a complexity point of view. Modal impredicativity occurs when, during reduction, the conclusion of a residual of a box b interacts with a node that belongs to the proof net inside another residual of b. Technically speaking, superlazy reduction is a new notion of reduction that allows to control modal impredicativity. More specifically, superlazy reduction replicates a box only when all its copies are opened. This makes the overall cost of reducing a proof net finite and predictable. Specifically, superlazy reduction applied to any pure proof nets takes primitive recursive time. Moreover, any primitive recursive function can be computed by a pure proof net via superlazy reduction.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
