Strong normalizability as a finiteness structure via the Taylor expansion of -terms

DOI10.1007/978-3-662-49630-5_24MaRDI QIDQ2811355zbMATH OpenOpenAlexFDO

Authors Michele Pagani, Christine Tasson, Lionel Vaux

Publication date 10 June 2016

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1603.07218

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Combinatory logic and lambda calculus (03B40)

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.

Recommendations

• A characterization of the Taylor expansion of -terms
• scientific article; zbMATH DE number 7089070
• Taylor expansion, -reduction and normalization
• Uniformity and the Taylor expansion of ordinary lambda-terms
• Geometry of resource interaction and Taylor-Ehrhard-Regnier expansion: \textit{a minimalist approach}

Cites work

• scientific article; zbMATH DE number 482822 (Why is no real title available?)
• A filter lambda model and the completeness of type assignment
• Complete restrictions of the intersection type discipline
• Finiteness spaces
• Logical Approaches to Computational Barriers
• Quantitative domains and infinitary algebras
• The Cut-Elimination Theorem for Differential Nets with Promotion
• The differential lambda-calculus
• Uniformity and the Taylor expansion of ordinary lambda-terms
• Visible acyclic differential nets. I: Semantics
• Weighted relational models of typed lambda-calculi

Cited in

(12)

• scientific article; zbMATH DE number 7089070 (Why is no real title available?)
• scientific article; zbMATH DE number 7566060 (Why is no real title available?)
• scientific article; zbMATH DE number 7003195 (Why is no real title available?)
• Taylor expansion, finiteness and strategies
• Asymptotically almost all \lambda-terms are strongly normalizing
• A characterization of the Taylor expansion of -terms
• scientific article; zbMATH DE number 7471690 (Why is no real title available?)
• scientific article; zbMATH DE number 7533340 (Why is no real title available?)
• Strong normalization of \(\mathsf{ML}^{\mathsf F}\) via a calculus of coercions
• Strong normalization of barrecursive terms without using infinite terms
• On strong standard completeness in some \(\mathrm{MTL}_\Delta\) expansions
• scientific article; zbMATH DE number 7471682 (Why is no real title available?)

This page was built for publication: Strong normalizability as a finiteness structure via the Taylor expansion of \(\lambda\)-terms

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2811355)