pith. sign in

arxiv: 2305.08489 · v6 · submitted 2023-05-15 · 💻 cs.LO

Extensional Taylor Expansion

Lison Blondeau-Patissier , Pierre Clairambault , Lionel Vaux Auclair This is my paper

Pith reviewed 2026-05-24 08:55 UTC · model grok-4.3

classification 💻 cs.LO
keywords extensional Taylor expansionresource calculuslambda calculusH* theoryNakajima treesgame semanticseta reductionbeta reduction
0
0 comments X

The pith

The equivalence induced by normalizing extensional Taylor expansions of lambda-terms is exactly H*, the greatest consistent sensible lambda-theory.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper defines extensional resource terms, which are resource terms in infinitely eta-long form but retain finite syntax and dynamics with strong confluence and normalization. It introduces an extensional Taylor expansion mapping lambda-terms to linear combinations of these terms, where the dynamics simulate both beta-reduction and eta-reduction. Normalization under the expansion induces an equivalence on lambda-terms that coincides with H*, the greatest consistent sensible theory also induced by Nakajima trees. This supplies a new route to models of H* by modeling the resource calculus and its dynamics. It further yields a bijection between normal extensional resource terms and isomorphism classes of augmentations in the universal arena, extending game semantics to the untyped setting.

Core claim

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. Extensional resource terms contain a language of finite approximants of Nakajima trees, and the dynamics of the extensional resource calculus simulate both beta-reduction and eta-reduction of the source lambda-terms.

What carries the argument

The extensional resource calculus of terms in infinitely eta-long form, whose normalization dynamics induce the H* equivalence via extensional Taylor expansion.

If this is right

  • Modeling the extensional resource calculus and its dynamics is sufficient to exhibit models of H*.
  • Extensional resource terms serve as finite approximants of Nakajima trees.
  • The normalization equivalence matches the theory induced by Nakajima trees.
  • Normal extensional resource terms stand in bijection with isomorphism classes of augmentations in the universal arena.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The untyped bijection with augmentations may support new proofs of properties of H* by importing techniques from game semantics.
  • The finite syntax could enable algorithmic approximations or decision procedures for membership in H* via resource-term normalization.
  • Similar extensional expansions might be definable for other lambda-theories to obtain resource-based characterizations.

Load-bearing premise

The dynamics of the extensional resource calculus correctly simulate both beta-reduction and eta-reduction of the source lambda terms.

What would settle it

A pair of lambda-terms equivalent under H* whose extensional Taylor expansions normalize to distinct normal forms, or a pair inequivalent under H* whose expansions normalize to the same form.

Figures

Figures reproduced from arXiv: 2305.08489 by Lionel Vaux Auclair, Lison Blondeau-Patissier, Pierre Clairambault.

Figure 1
Figure 1. Figure 1: Shape of a (non-⊥) Böhm tree • λx1. · · · λxk.y A1 Al · · · [PITH_FULL_IMAGE:figures/full_fig_p003_1.png] view at source ↗
Figure 3
Figure 3. Figure 3: Depiction of m n¯ • λx1. · · · λxk.y n¯1 · · · n¯l [PITH_FULL_IMAGE:figures/full_fig_p004_3.png] view at source ↗
Figure 5
Figure 5. Figure 5: Infinite η-expansion of a variable • λz1. · · · λzk.λ⃗y. M N1 Nl y η 0 y η 1 · · · · · · [PITH_FULL_IMAGE:figures/full_fig_p009_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: Shape of an infinitely η-long λ-term or even nested η-expansions of fresh variables: x ←η λz1.x z1 ←η λz1.x (λz2.z1 z2) ←η · · · ←η λz1.x (λz2.z1 (· · · λzk.zk−1 zk · · ·)). We can nonetheless consider the limit of iterating the combination of those two processes, as given by an infinite tree x η that we depict in fig. 5, where ⃗y is a sequence ⟨y0, y1, . . .⟩ of fresh variables, and each y η i is recursiv… view at source ↗
Figure 7
Figure 7. Figure 7: Shape of an extensional resource term 1.3 Our contributions In the present paper, we introduce a variant of Taylor expansion for pure, untyped λ-terms, in such a way that reduction in the associated resource calculus allows us to simulate both β- and η-reduction. We characterize the equational theory induced via normalization as the maximal consistent and sensible λ-theory, and apply this result to a parti… view at source ↗
Figure 8
Figure 8. Figure 8: Rules for constructing extensional resource terms [PITH_FULL_IMAGE:figures/full_fig_p015_8.png] view at source ↗
Figure 9
Figure 9. Figure 9: Rules of fine-step extensional resource reduction (choosing [PITH_FULL_IMAGE:figures/full_fig_p022_9.png] view at source ↗
Figure 10
Figure 10. Figure 10: Rules of full-step extensional resource reduction [PITH_FULL_IMAGE:figures/full_fig_p026_10.png] view at source ↗
Figure 11
Figure 11. Figure 11: Definition of copycat terms (assuming y ̸= x, and choosing x ̸∈ ⃗y whenever relevant; and choosing l such that no ⃗x(i) with i ≥ l is free in u in the definition of c −⟨⃗x, u⟩) A straightforward induction allows to check that #c −⟨x, u⟩ = |u|x: in particular, if x ̸∈ V(u), then c −⟨x, u⟩ = [ ]. Moreover, if ⃗x ̸∈ Vs(u) then c −⟨⃗x, u⟩ = ι directly by definition. Example 5.5. The reader may check that c⟨x,… view at source ↗
Figure 12
Figure 12. Figure 12: The universal arena U Constructions. We shall use some other constructions on arenas: the atomic arena o has just one (negative) move q. The tensor A1 ⊗ A2 of arenas A1 and A2 has events the tagged disjoint union |A1 ⊗ A2| = |A1| + |A2| = {1} × |A1| ⊎ {2} × |A2|, and other components inherited. The hom-arena A1 ⊢ A2 is A⊥ 1 ⊗A2, where the dual A⊥ of A has the same components but the polarity reversed. If … view at source ↗
Figure 13
Figure 13. Figure 13: A configuration on U For x ∈ C(A) and y ∈ C(B), x ⊢ y ∈ C(A ⊢ B) is defined like x ⊗ y. If B and y are pointed, then x ⇒ y ∈ C(A ⇒ B) is defined as x ⊢ y where additionally, all events of x are set to depend on the unique initial move of y. If x ∈ C(A) and y ∈ C(AN), we moreover define x ⦂⦂ y ∈ C(AN) from x ⊗ y ∈ C(A ⊗ AN) by applying the isomorphism of arenas packA : A ⊗ AN ≃ AN: in other words, events a… view at source ↗
Figure 15
Figure 15. Figure 15: The same augmentation following the dynamic causality 8.4 Augmentations and isogmentations 8.4.1 Definitions Augmentations. From the above, we have seen that positions are exactly points of the relational model (or intersection types), and that configurations are concrete representations for positions. Now augmentations are configurations augmented with causal links reminiscent from terms. Definition 8.11… view at source ↗
Figure 16
Figure 16. Figure 16: A correspondence between Taylor expansion and game semantics [PITH_FULL_IMAGE:figures/full_fig_p068_16.png] view at source ↗
read the original abstract

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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 2 minor

Summary. The manuscript introduces an extensional resource calculus extending Ehrhard-Regnier resource terms to infinitely eta-long forms while retaining finite syntax. It proves strong confluence and normalization. An extensional Taylor expansion maps lambda-terms to (possibly infinite) linear combinations of these terms and is shown to simulate both beta- and eta-reduction. The central result is that the equivalence on lambda-terms induced by normalization of the extensional Taylor expansions coincides with H*, the greatest consistent sensible lambda-theory (equivalently, the theory induced by Nakajima trees). Normal extensional resource terms serve as finite approximants of Nakajima trees. The paper also recovers a bijection, in the untyped setting, between normal extensional resource terms and isomorphism classes of augmentations (plays up to homotopy) in the universal arena of Hyland-Ong game semantics.

Significance. If the central claims hold, the work supplies a new, direct characterization of H* via models of the extensional resource calculus and its dynamics, simplifying the construction of models of this theory. It extends the Taylor-expansion/game-semantics connection from the typed to the untyped setting via the explicit bijection with augmentations. The finite syntax for eta-long terms and the explicit simulation of eta-reduction are technical strengths. The manuscript does not mention machine-checked proofs or reproducible code, but the finite-approximant view of Nakajima trees is a clear contribution.

minor comments (2)
  1. [Abstract / extensional Taylor expansion section] The abstract states the simulation of eta-reduction but the corresponding theorem statement (likely in the section on extensional Taylor expansion) would benefit from an explicit reference to the eta-rule being simulated, to make the claim easier to locate.
  2. [Preliminaries] Notation for the linear combinations in the extensional Taylor expansion (e.g., the coefficients and the infinite sums) should be introduced with a short example in the preliminaries to aid readability for readers unfamiliar with the ordinary Taylor expansion.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive summary of the manuscript, recognition of its contributions, and recommendation to accept.

Circularity Check

0 steps flagged

No significant circularity

full rationale

The derivation introduces definitions for the extensional resource calculus and its dynamics, proves strong confluence and normalization internally, defines the extensional Taylor expansion mapping, and establishes via stated theorems that normalization induces exactly H* (equivalently Nakajima-tree equality). These steps are self-contained within the paper's own constructions and proofs; no central claim reduces by the paper's equations to a fitted parameter, a self-citation chain, or an ansatz imported from prior author work. External references (Ehrhard-Regnier, Hyland-Ong, Melliès) supply background but are not load-bearing for the equivalence result.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The work rests on standard lambda-calculus reduction theory and the known definition of H* and Nakajima trees; no free parameters or new postulated entities are introduced in the abstract.

axioms (2)
  • standard math Standard confluence and normalization properties of beta- and eta-reduction in lambda calculus
    Invoked to establish that the resource dynamics simulate the source reductions.
  • domain assumption Existence and uniqueness properties of Nakajima trees and the theory H*
    Used to identify the induced equivalence as H*.

pith-pipeline@v0.9.0 · 5867 in / 1186 out tokens · 26885 ms · 2026-05-24T08:55:09.334668+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

2 extracted references · 2 canonical work pages

  1. [1]

    Finiteness spaces

    url: https://doi.org/10.4230/LIPIcs.FSCD.2024.29. [Ehr05] Thomas Ehrhard. “Finiteness spaces”. In: Math. Struct. Comput. Sci. 15.4 (2005), pp. 615–646.doi: 10.1017/S0960129504004645. url: https://doi.org/10.1017/ S0960129504004645. [Eil74] Samuel Eilenberg. Automata, Languages, and Machines. Vol. 59-A. Pure and Applied Mathematics. Academic Press, 1974. [...

    work page doi:10.4230/lipics.fscd.2024.29 2024

  2. [2]

    Infinite normal forms for the lambda-calculus

    Ed. by Bart Jacobs, Alexandra Silva, and Sam Staton. Vol. 308. Electronic Notes in Theoretical Computer Science. Elsevier, 2014, pp. 245–272.doi: 10.1016/J.ENTCS. 2014.10.014. url: https://doi.org/10.1016/j.entcs.2014.10.014. [Nak75] Reiji Nakajima. “Infinite normal forms for the lambda-calculus”. In:Lambda-Calculus and Computer Science Theory, Proceeding...

    work page doi:10.1016/j.entcs 2014