Extensional Taylor Expansion

TL;DR

This work develops an extensional variant of Taylor expansion for pure λ-calculus by introducing an extensional resource calculus that supports infinitely η-long forms while retaining finite syntax and confluence. It defines two intertwined extensional Taylor expansions, maps λ-terms to vectors of extensional resource terms, and shows that normalization of these expansions captures the greatest consistent sensible theory $H^*$ (Nakajima trees). The paper also connects this framework to game semantics via a relational model, and establishes a precise correspondence between normal extensional resource terms and isogmentations on the universal arena, providing a new, untyped bridge between Taylor expansion and semantic models. The results yield a principled method to model $H^*$ using extensional resource calculus and offer a new perspective on the interaction between Taylor expansion and game semantics in an untyped setting.

Abstract

We introduce a calculus of extensional resource terms. These are resource terms à la Ehrhard-Regnier, but in infinitely eta-long form. The calculus still retains a finite syntax and dynamics: in particular, we prove strong confluence and normalization. Then we define an extensional version of Taylor expansion, mapping ordinary lambda-terms to (possibly infinite) linear combinations of extensional resource terms: like in the ordinary case, the dynamics of our resource calculus allows us to simulate the beta-reduction of lambda-terms; the extensional nature of this expansion shows in the fact that we are also able to simulate eta-reduction. In a sense, extensional resource terms contain a language of finite approximants of Nakajima trees, much like ordinary resource terms can be seen as a richer version of finite Böhm trees. We show that the equivalence induced on lambda-terms by the normalization of extensional Taylor-expansion is nothing but H*, the greatest consistent sensible lambda-theory -- which is also the theory induced by Nakajima trees. This characterization provides a new, simple way to exhibit models of H*: it becomes sufficient to model the extensional resource calculus and its dynamics. The extensional resource calculus moreover allows us to recover, in an untyped setting, a connection between Taylor expansion and game semantics that was previously limited to the typed setting. Indeed, simply typed, eta-long, beta-normal resource terms are known to be in bijective correspondence with plays in the sense of Hyland-Ong game semantics, up to Melliès' homotopy equivalence. Extensional resource terms are the appropriate counterpart of eta-long resource terms in an untyped setting: we spell out the bijection between normal extensional resource terms and isomorphism classes of augmentations (a canonical presentation of plays up to homotopy) in the universal arena.

Figures (18)

• Figure 1: Shape of a (non-$\bot$) Böhm tree
• Figure 2: Shape of a (non-$\bot$) approximant
• Figure 3: Depiction of $m\,\bar{n}$
• Figure 4: Shape of a normal resource term
• Figure 5: Infinite $η$-expansion of a variable

Theorems & Definitions (170)

• lemma 1.4
• proof
• example 3.1
• definition 3.2
• example 3.3
• lemma 3.4
• proof
• lemma 3.5
• proof
• lemma 3.6