Finitary Simulation of Infinitary $β$-Reduction via Taylor Expansion, and Applications

TL;DR

The paper addresses extending Taylor expansion to the infinitary lambda-calculus in the 001 variant, where Böhm trees are the normal forms. It introduces a mixed inductive–coinductive framework and defines a Taylor expansion into a resource calculus to simulate infinitary beta-reduction by finite resource-term reductions, culminating in a generalized Commutation theorem. The authors derive new proofs of normalization, confluence, solvability, and the Genericity lemma within this infinitary setting, and they discuss standardisation and diagonal arguments to manage infinite reductions. This work provides a robust foundation for analyzing infinitary computation via finitary semantics and suggests several avenues for extending to other infinitary variants and to quantitative Taylor expansions.

Abstract

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.

Figures (3)

• Figure 1: Two infinitary terms, only the left one of which is 001-infinitary.
• Figure 2: Some derivations corresponding to terms in $lambda-infinity-001$. Notice that the loops are correct because they cross a coinductive rule.
• Figure 3: The terms $(M)N^{(k)}$ and $N^k$.

Theorems & Definitions (115)

• Definition 2.1: 001-infinitary terms
• Definition 2.2: 001-infinitary terms, using a mixed formal system
• Remark 2.3
• Example 2.4
• Definition 2.6: substitution
• Remark 2.7
• Definition 2.8: finitary reduction $\mathrel{\longrightarrow_\beta}$
• Definition 2.10: 001-infinitary reduction $\mathrel{\longrightarrow_\beta^\infty}$
• Example 2.11
• Remark 2.12