Recursion does not always help
Gordon Plotkin

TL;DR
This paper demonstrates that incorporating recursion into certain typed lambda calculi does not expand the set of functions they can define, challenging assumptions about recursion's power in these systems.
Contribution
It proves that adding recursion to typed lambda calculi does not increase the class of definable functions, providing a new understanding of recursion's limitations in these frameworks.
Findings
Recursion does not increase the total functions in typed λ-calculi.
Adding recursion does not expand the class of partial functions on free algebras.
Recursion's power is limited in the context of typed λ-calculi.
Abstract
We show that adding recursion does not increase the total functions definable in the typed -calculus or the partial functions definable in the -calculus. As a consequence, adding recursion does not increase the class of partial or total definable functions on free algebras and so, in particular, on the natural numbers.
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
TopicsComputability, Logic, AI Algorithms · Logic, programming, and type systems · Mathematical and Theoretical Analysis
