Taylor Expansion is Game Semantics
summary
This work shows that the Taylor expansion of a simply-typed λ-term is isomorphic to its interpretation in pointer concurrent games, extending Tsukada and Ong’s Hyland-Ong correspondence to augmentations and homotopy quotients; the isomorphism respects β-reduction and uses augmentations (configurations plus a causal order) as canonical representatives. Composition of augmentations requires summing over isomorphisms of the shared arena, so strategies become formal sums of augmentations, matching Taylor expansion coefficients. Results hold for the typed, η-long setting; an untyped extension is still in progress.
AI-written summary · about