The geometry of linear higher-order recursion

DOI10.1145/1462179.1462180MaRDI QIDQ2946566zbMATH OpenOpenAlexFDO

Authors Ugo Dal Lago

Publication date 17 September 2015

Published in ACM Transactions on Computational Logic (Search for Journal in Brave)

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

zbMATH Keywords

geometry of interactionhigher-order recursionimplicit computational complexitylambda calculustype systems

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Complexity of computation (including implicit computational complexity) (03D15) Recursive functions and relations, subrecursive hierarchies (03D20) Proof-theoretic aspects of linear logic and other substructural logics (03F52)

Abstract: Linearity and ramification constraints have been widely used to weaken higher-order (primitive) recursion in such a way that the class of representable functions equals the class of polytime functions. We show that fine-tuning these two constraints leads to different expressive strengths, some of them lying well beyond polynomial time. This is done by introducing a new semantics, called algebraic context semantics. The framework stems from Gonthier's original work and turns out to be a versatile and powerful tool for the quantitative analysis of normalization in presence of constants and higher-order recursion.

Recommendations

• Higher type recursion, ramification and polynomial time
• Types for Proofs and Programs
• scientific article; zbMATH DE number 2006627
• scientific article; zbMATH DE number 1531370
• scientific article; zbMATH DE number 1223626

Cited in

(7)

• Implicit computational complexity of subrecursive definitions and applications to cryptographic proofs
• Interaction graphs: graphings
• A correspondence between maximal abelian sub-algebras and linear logic fragments
• scientific article; zbMATH DE number 5587879 (Why is no real title available?)
• Towards a geometry of recursion
• Types for Proofs and Programs
• Implicit computation complexity in higher-order programming languages

This page was built for publication: The geometry of linear higher-order recursion

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