Linear Recursion

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.