Linear Recursion
Sandra Alves (1), Maribel Fern\'andez (2), M\'ario Florido (1), Ian, Mackie (3) ((1) University of Porto, (2) King's College London, (3) \'Ecole, Polytechnique)

TL;DR
This paper introduces two minimal, Turing-complete extensions of the typed linear lambda-calculus using unbounded and bounded recursion, maintaining linearity and typeability, with applications to programming languages like PCF.
Contribution
It presents novel minimal linear lambda-calculus systems with recursion that are Turing-complete and compatible with linearity constraints, and demonstrates their application to language compilation.
Findings
Both extensions are Turing-complete and minimal.
Compatibility with linearity and typeability is maintained.
Application to compiling PCF into linear lambda-calculus.
Abstract
We define two extensions of the typed linear lambda-calculus that yield minimal Turing-complete systems. The extensions are based on unbounded recursion in one case, and bounded recursion with minimisation in the other. We show that both approaches are compatible with linearity and typeability constraints. Both extensions of the typed linear lambda-calculus are minimal, in the sense that taking out any of the components breaks the universality of the system. We discuss implementation techniques that exploit the linearity of the calculi. Finally, we apply the results to languages with fixpoint operators: we give a compilation of the programming language PCF into a linear lambda-calculus with linear unbounded recursion.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Formal Methods in Verification · Logic, Reasoning, and Knowledge
