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同伦等价意义下）存在双射对应。外延资源项是非类型化场景中η-长资源项的恰当对应物：我们明确给出了正规外延资源项与通用竞技场中增广结构（同伦等价下玩法的规范表示）同构类之间的双射关系。