We introduce a calculus of extensional resource terms. These are resource terms \`a 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\"ohm 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\`es' 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.

翻译：我们引入了一种外延资源项演算。这些资源项遵循Ehrhard-Regnier的风格，但采用无限η长形式。该演算仍保持有限的语法和动态特性：特别地，我们证明了强合流性和正规化性质。随后，我们定义了泰勒展开的外延版本，将常规λ项映射到（可能无限的）外延资源项的线性组合：与常规情况类似，我们资源演算的动态特性使得能够模拟λ项的β归约；这种展开的外延本质体现在我们同样能够模拟η归约。从某种意义上说，外延资源项包含了中岛树有限逼近元的语言，正如普通资源项可被视为有限贝姆树的更丰富版本。我们证明，通过外延泰勒展开正规化在λ项上诱导的等价关系正是H*——最大一致敏感λ理论，这也是中岛树诱导的理论。这一特征为展示H*模型提供了一种新的简单方法：只需对外延资源演算及其动态特性进行建模即可。此外，外延资源演算使我们在非类型化环境中恢复了泰勒展开与博弈语义之间的联系，而此前该联系仅限于类型化环境。事实上，已知简单类型化、η长、β正规的资源项与Hyland-Ong博弈语义意义下的玩法存在双射对应（直至Melliès同伦等价）。外延资源项是非类型化环境中η长资源项的恰当对应物：我们明确给出了正规外延资源项与通用竞技场中增广结构（同伦等价下玩法的规范表示）的同构类之间的双射关系。