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 Résumé: 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. |