The Separation Theorem for Differential Interaction Nets
The Separation Theorem for Differential Interaction Nets
复制标题
微分交互网络的分离定理
DOI：
10.1007/978-3-540-75560-9_29
复制
发表时间：
2007
影响因子：
3.4
通讯作者：
Michele Pagani
中科院分区：
文献类型：
--
作者：
Damiano Mazza;Michele Pagani
微分交互作用网（DIN）是由托马斯·埃哈德（Thomas Ehrhard）和劳伦特·雷尼尔（Laurent Regnier）作为线性逻辑证明网的扩展而提出的。我们证明了DIN具有内部分离性质：给定两个不同的正规网，存在一个对偶网将它们分开，类似于玻姆的λ-演算定理。我们的结果意味着，特别是每一个非平凡的指称模型的DIN（如Ehrhard的有限性空间）的忠实性。我们还观察到，内部分离并不适用于线性逻辑证明网：我们的工作指出，这种失败是由于线性逻辑指数模态的基本不对称性，而不是完全对称的DIN。
Differential interaction nets (DIN) have been introduced by Thomas Ehrhard and Laurent Regnier as an extension of linear logic proof-nets. We prove that DIN enjoy an internal separation property: given two different normal nets, there exists a dual net separating them, in analogy with Bohm's theorem for the λ-calculus. Our result implies in particular the faithfulness of every non-trivial denotational model of DIN (such as Ehrhard's finiteness spaces). We also observe that internal separation does not hold for linear logic proof-nets: our work points out that this failure is due to the fundamental asymmetry of linear logic exponential modalities, which are instead completely symmetric in DIN.