Strong Normalizability as a Finiteness Structure via the Taylor Expansion of {\lambda}-terms

TL;DR

This paper establishes a formal connection between strong normalization of non-deterministic lambda-terms and finiteness structures derived from their Taylor expansions, providing a new semantic perspective on normalization.

Contribution

It introduces a finiteness structure on resource terms that characterizes strong normalization via the support of Taylor expansions.

Findings

Strongly normalizing lambda-terms have finitary Taylor supports.

Existence of a normal form for Taylor expansions of strongly normalizable terms.

Finiteness structures reflect the normalization property in non-deterministic lambda calculus.

Abstract

In the folklore of linear logic, a common intuition is that the structure of finiteness spaces, introduced by Ehrhard, semantically reflects the strong normalization property of cut-elimination. We make this intuition formal in the context of the non-deterministic {\lambda}-calculus by introducing a finiteness structure on resource terms, which is such that a {\lambda}-term is strongly normalizing iff the support of its Taylor expansion is finitary. An application of our result is the existence of a normal form for the Taylor expansion of any strongly normalizable non-deterministic {\lambda}-term.