|Strong Normalizability as a Finiteness Structure via the Taylor Expansion of λ -terms |
Auteur(s): Pagani Michele, Tasson Christine, Vaux L.
Conference: 19th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2016) (Eindhoven, NL, 2016-04-04)
Ref HAL: hal-01292923_v1
Ref Arxiv: 1603.07218
Ref. & Cit.: NASA ADS
Exporter : BibTex | endNote
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 λ-calculus by introducing a finiteness structure on resource terms, which is such that a λ-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 λ-term.