Recursion does not always help

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 $\lambda\beta\eta$-calculus or the partial functions definable in the $\lambda\Omega$-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.