论文标题
通过Taylor扩展对无限$β$还原的无限模拟和应用
Finitary Simulation of Infinitary $β$-Reduction via Taylor Expansion, and Applications
论文作者
论文摘要
Ehrhard和Regnier的Taylor扩展$λ$ terms源自Girard的线性逻辑，已广泛用作近似$λ$ -calculus的几个变体的术语的工具。许多结果是由换向定理产生的，该定理将术语的泰勒膨胀的正常形式与其böhm树相关。这导致我们考虑将这种形式主义扩展到无限$λ$ -calculus，因为$λ_ {\ infty}^{001} $版本的这种演算的版本是正常形式的böhm树，并且似乎是重新校准定理的理想框架。 我们给出了$λ_{\ infty}^{001} $的（共同）归纳呈现。我们在该积分上定义了泰勒膨胀，并指出可以通过这种泰勒的扩张来模拟无限$β$还原。目标语言是通常的资源演算，尤其是资源降低仍然有限，汇合和终止。最后，我们陈述了广义的换向定理，并利用我们的结果提供了简单的证据，证明了无限$λ$ -Calculus中某些归一化和汇合属性。
Originating in Girard's Linear logic, Ehrhard and Regnier's Taylor expansion of $λ$-terms has been broadly used as a tool to approximate the terms of several variants of the $λ$-calculus. Many results arise from a Commutation theorem relating the normal form of the Taylor expansion of a term to its Böhm tree. This led us to consider extending this formalism to the infinitary $λ$-calculus, since the $Λ_{\infty}^{001}$ version of this calculus has Böhm trees as normal forms and seems to be the ideal framework to reformulate the Commutation theorem. We give a (co-)inductive presentation of $Λ_{\infty}^{001}$. We define a Taylor expansion on this calculus, and state that the infinitary $β$-reduction can be simulated through this Taylor expansion. The target language is the usual resource calculus, and in particular the resource reduction remains finite, confluent and terminating. Finally, we state the generalised Commutation theorem and use our results to provide simple proofs of some normalisation and confluence properties in the infinitary $λ$-calculus.
