线性逻辑中直觉主义与经典极化交叉点处的连通性
Connectivity at the crossroad of intuitionistic and classical polarizations in linear logic
浏览论文内容
中文总结 AI 辅助
研究扩展线性逻辑证明结构正确性标准的性质，提出对证明结构的几何限制使其成为充分性质，引入VMELL片段，将!演算项翻译为证明网，分解λ演算翻译，证明消去切割模拟!归约并给出!演算项的证明网特征。
中文摘要 AI 辅助
我们研究了一种扩展线性逻辑证明结构的达诺斯 - 雷吉耶正确性标准的性质。该性质适用于证明结构的正确性图：即任何此类图都是无环的，且其连通分量的数量恰好比底部或弱化节点的数量多一个。在乘法指数线性逻辑（MELL）中，已知此性质对于从证明结构恢复相继式演算证明是必要但不充分的。我们提出了对证明结构的几何限制，使这一必要性质变为充分性质，且计算效率高：从而能引入MELL的显著片段VMELL，此性质对其确实是正确性标准。片段VMELL融合了经典和直觉主义极化。我们将!演算项翻译成VMELL的证明网，分解了按名调用和按值调用λ演算在线性逻辑中的常用翻译，证明了消去切割模拟!归约，并给出了!演算项作为证明网的明确特征。
英文摘要
We investigate a property that extends the Danos-Regnier correctness criterion for linear logic proof-structures. The property applies to the correctness graphs of a proof-structure: it states that any such graph is acyclic and the number of its connected components is exactly one more than the number of nodes bottom or weakening. This is known to be necessary but not sufficient in multiplicative exponential linear logic (MELL) to recover a sequent calculus proof from a proof-structure. We present a geometric restriction on proof-structures allowing us to turn this necessary property into a sufficient one, computationally efficient: we can thus introduce the notable fragment VMELL of MELL for which the property is indeed a correctness criterion. The fragment VMELL brings together the classical and intuitionistic polarizations. We translate the bang calculus terms into proof-nets of VMELL, factorize the usual translations in linear logic of the call-by-name and call-by-value lambda-calculi, prove that cut elimination simulates bang reduction, and provide an explicit characterization of the bang calculus terms as proof-nets.
