We introduce a calculus of extensional resource terms. These are resource terms à la Ehrhard-Regnier, but in infinite η-long form, while retaining a finite syntax and dynamics: in particular, we prove strong confluence and normalization.

Then we define an extensional version of Taylor expansion, mapping ordinary λ-terms to sets (or infinite linear combinations) of extensional resource terms: just like for ordinary Taylor expansion, the dynamics of our resource calculus allows to simulate the β-reduction of λ-terms; the extensional nature of expansion shows in that we are also able to simulate η-reduction. In a sense, extensional resource terms form a language of (non-necessarily normal) finite approximants of Nakajima trees, much like ordinary resource terms are approximants of Böhm-trees. Indeed, we show that the equivalence induced on λ-terms by the normalization of extensional Taylor-expansion is nothing but H∗, the greatest consistent sensible λ-theory.

Taylor expansion has profoundly renewed the approximation theory of the λ-calculus by providing a quantitative alternative to order-based approximation techniques, such as Scott continuity and Böhm trees. Extensional Taylor expansion enjoys similar advantages: e.g., to exhibit models of H∗, it is now sufficient to provide a model of the extensional resource calculus. We apply this strategy to give a new, elementary proof of a result by Manzonetto: H∗ is the λ-theory induced by a well-chosen reflexive object in the relational model of the λ-calculus.

This is joint work with Lison Blondeau-Patissier and Pierre Clairambault.

https://arxiv.org/abs/2305.08489