微分相互作用网的相互作用几何
The Geometry of Interaction of Differential Interaction Nets
摘要：
相互作用几何的目的是给出一个语义的证明或程序占他们的动力学。最初的介绍，翻译为代数加权的路径在proofnets，导致了更好的表征的最佳约简算法。最近Ehrhard和Regnier介绍了线性逻辑的乘法指数片段（MELL）的扩展，它能够表达程序的非确定性行为和一种类似于证明网的演算：差分交互网。本文构造了一个适当的几何相互作用（GoI）的这种扩展。我们认为它既是一个代数理论，也是一个具体的可逆计算。我们在这个GoI和MELL之间建立联系。作为副产品，我们第一次给出了一个方程理论适用于线性逻辑的乘加片段的GoI。
英文摘要：
The Geometry of Interaction purpose is to give a semantic of proofs or programs accounting for their dynamics. The initial presentation, translated as an algebraic weighting of paths in proofnets, led to a better characterization of the lambda-calculus optimal reduction. Recently Ehrhard and Regnier have introduced an extension of the Multiplicative Exponential fragment of Linear Logic (MELL) that is able to express non-deterministic behaviour of programs and a proofnet-like calculus: Differential Interaction Nets. This paper constructs a proper Geometry of Interaction (GoI) for this extension. We consider it both as an algebraic theory and as a concrete reversible computation. We draw links between this GoI and the one of MELL. As a by-product we give for the first time an equational theory suitable for the GoI of the Multiplicative Additive fragment of Linear Logic.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
