一句话：为无穷 λ-演算 Λ∞^{001} 建立 Taylor 展开，用资源演算的有限归约模拟无穷 β-归约并证明广义交换定理。
本文把 Ehrhard-Regnier 的 Taylor 展开从通常 λ-演算推广到无穷 λ-演算。作者选取 Λ∞^{001} 作为框架，因为其范式正是 Böhm 树，适合重新表述将 Taylor 展开的范式与 Böhm 树联系起来的交换定理。文章给出 Λ∞^{001} 的（余）归纳呈现，并在该演算上定义 Taylor 展开，证明无穷 β-归约可由该展开模拟。目标语言是通常的资源演算；关键性质是资源归约仍然有限、合流且终止，从而以有限重写刻画无穷归约。作者进一步陈述广义交换定理，并利用这些结果给出无穷 λ-演算中若干正规化与合流性质的简单证明。
Originating in Girard's Linear logic, Ehrhard and Regnier's Taylor expansion of $\lambda$-terms has been broadly used as a tool to approximate the terms of several variants of the $\lambda$-calculus. Many results arise from a Commutation theorem relating the normal form of the Taylor expansion of a term to its B\"ohm tree. This led us to consider extending this formalism to the infinitary $\lambda$-calculus, since the $\Lambda_{\infty}^{001}$ version of this calculus has B\"ohm trees as normal forms and seems to be the ideal framework to reformulate the Commutation theorem. We give a (co-)inductive presentation of $\Lambda_{\infty}^{001}$. We define a Taylor expansion on this calculus, and state that the infinitary $\beta$-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 $\lambda$-calculus.
@article{paperbot2160,
title = {Finitary Simulation of Infinitary $\beta$-Reduction via Taylor Expansion, and Applications},
author = {Rémy Cerda and Lionel Vaux Auclair},
journal = {Logical Methods in Computer Science},
volume = {Volume 19, Issue 4},
year = {2023},
doi = {10.46298/lmcs-19(4:34)2023}
}