An Elementary Fragment of Second-Order Lambda Calculus

TL;DR

This paper introduces a simplified fragment of second-order lambda calculus (System F) that characterizes elementary recursive functions, with a stratified type quantification system.

Contribution

It defines a restricted, stratified version of System F with non-interleaved quantification, capturing elementary recursive functions.

Findings

Characterizes elementary recursive functions

Defines a stratified, non-interleaved type system

Provides a formal foundation for elementary recursion in lambda calculus

Abstract

A fragment of second-order lambda calculus (System F) is defined that characterizes the elementary recursive functions. Type quantification is restricted to be non-interleaved and stratified, i.e., the types are assigned levels, and a quantified variable can only be instantiated by a type of smaller level, with a slightly liberalized treatment of the level zero.