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.

翻译：源于Girard的线性逻辑，Ehrhard与Regnier提出的$\lambda$-项泰勒展开已被广泛用作逼近$\lambda$-演算多种变体项的工具。诸多结果源自一项交换定理，该定理将项泰勒展开的范式与其Böhm树相关联。这促使我们考虑将这一形式体系扩展至无穷$\lambda$-演算，因为该演算的$\Lambda_{\infty}^{001}$版本以Böhm树作为范式，且似乎是重构交换定理的理想框架。我们给出$\Lambda_{\infty}^{001}$的（共）归纳表示，在该演算上定义泰勒展开，并指出无穷$\beta$-归约可通过该泰勒展开模拟。目标语言为通常的资源演算，其中资源归约始终保持有限、合流且终止。最后，我们陈述广义交换定理，并利用所得结果为无穷$\lambda$-演算中的某些归一化与合流性质提供简洁证明。