Lison Blondeau-Patissier, Pierre Clairambault, Lionel Vaux Auclair
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.