| Summary: | 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.
|
|---|