We introduce a calculus of extensional resource terms. These are resource terms \`a la Ehrhard-Regnier, but in infinite $\eta$-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 $\lambda$-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 $\beta$-reduction of $\lambda$-terms; the extensional nature of expansion shows in that we are also able to simulate $\eta$-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\"ohm-trees. Indeed, 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. Taylor expansion has profoundly renewed the approximation theory of the $\lambda$-calculus by providing a quantitative alternative to order-based approximation techniques, such as Scott continuity and B\"ohm 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 $\lambda$-theory induced by a well-chosen reflexive object in the relational model of the $\lambda$-calculus.
翻译:我们提出一种外延资源项演算。这些资源项继承Ehrhard-Regnier的风格,但采用无穷η-长形式,同时保留有限语法与动态特性:特别地,我们证明了强汇合性与归一化性质。随后定义外延版本的泰勒展开,将普通λ-项映射为外延资源项的集合(或无穷线性组合):与普通泰勒展开类似,资源演算的动态性质可模拟λ-项的β-归约;展开的外延特性体现在我们还能模拟η-归约。从某种意义上说,外延资源项构成了中岛树(非必要正规)有限近似项的语言,正如普通资源项是Böhm树的近似项。事实上,我们证明外延泰勒展开归一化在λ-项上诱导的等价关系正是H*——最大的一致可感λ-理论。泰勒展开通过为基于序的近似技术(如斯科特连续性与Böhm树)提供定量替代方案,深刻革新了λ-演算的近似理论。外延泰勒展开具有类似优势:例如,为展示H*的模型,只需提供外延资源演算的模型。我们应用此策略给出Manzonetto定理的一个全新初等证明:H*是由λ-演算关系模型中精心选取的自反对象所诱导的λ-理论。