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

DOI10.1007/978-3-662-49630-5_24zbMATH Open1476.03009arXiv1603.07218OpenAlexW2305850023MaRDI QIDQ2811355FDOQ2811355

Authors: Michele Pagani, Christine Tasson, Lionel Vaux 

Publication date: 10 June 2016

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

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.

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

Recommendations

• A characterization of the Taylor expansion of \(\lambda\)-terms
• scientific article; zbMATH DE number 7089070
• Taylor expansion, \(\beta\)-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}

Mathematics Subject Classification ID

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

Cites Work

• Logical Approaches to Computational Barriers
• Uniformity and the Taylor expansion of ordinary lambda-terms
• The differential lambda-calculus
• A filter lambda model and the completeness of type assignment
• Title not available (Why is that?)
• Finiteness spaces
• Complete restrictions of the intersection type discipline
• Visible acyclic differential nets. I: Semantics
• Quantitative domains and infinitary algebras
• Weighted Relational Models of Typed Lambda-Calculi
• The Cut-Elimination Theorem for Differential Nets with Promotion

Cited In (11)

• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Taylor expansion, finiteness and strategies
• Asymptotically almost all \lambda-terms are strongly normalizing
• Title not available (Why is that?)
• Title not available (Why is that?)
• 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
• Title not available (Why is that?)

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)