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.

翻译：源自吉拉德线性逻辑的埃哈德与雷尼耶的λ项泰勒展开，已被广泛用作逼近λ演算多种变体的工具。许多结果源于泰勒展开范式与其伯姆树之间的交换定理。这促使我们考虑将该形式系统扩展至无穷λ演算，因为该演算的$\Lambda_{\infty}^{001}$版本以伯姆树为范式，且似乎是重构交换定理的理想框架。我们给出了$\Lambda_{\infty}^{001}$的（余）归纳表示，定义了该演算上的泰勒展开，并论证了无穷β归约可通过该泰勒展开进行模拟。目标语言是通常的资源演算，特别地，资源归约保持有限性、合流性与终止性。最后，我们给出广义交换定理，并利用我们的结果为无穷λ演算中的某些规范性与合流性性质提供简洁证明。