Primitive Recursive Dependent Type Theory

TL;DR

The paper addresses extracting primitive recursive content from a dependent type theory by restricting natural numbers elimination to a universe without $Π$-types, proving that every definable $f:\mathbb{N}\to\mathbb{N}$ is primitive recursive within the standard Set interpretation. The authors construct a subsystem $\mathrm{T}_{\mathrm{pr}}$ of MLTT with two universes and employ synthetic Tait computability and Artin gluing to a topos of primitive recursive functions to prove canonicity and soundness. They show that all $\mathrm{T}_{\mathrm{pr}}$-definable functions are primitive recursive, via a carefully designed semantic glue $\mathcal{G}=\mathrm{Set}\downarrow\rho$ and a semantics in a PR-topos $\mathcal{R}$, ensuring a conservative extension over PRA while remaining expressive for dependent types. The work offers modular extensions and discusses practical mechanization prospects, with potential applications to Cubical Type Theory and future enrichment by finitary inductive types and a comonadic modality, aiming at a proof-assistant-friendly framework for PR computations within dependent type theory.

Abstract

We show that restricting the elimination principle of the natural numbers type in Martin-Löf Type Theory (MLTT) to a universe of types not containing $Π$-types ensures that all definable functions are primitive recursive. This extends the concept of primitive recursiveness to general types. We discuss extensions to univalent type theories and other notions of computability. We are inspired by earlier work by Martin Hofmann, work on Joyal's arithmetic universes, and Hugo Herbelin and Ludovic Patey's sketched Calculus of Primitive Recursive Constructions. We define a theory Tpr that is a subtheory of MLTT with two universes, such that all inductive types are finitary and the lowest universe is restricted to not contain $Π$-types. We prove soundness such that all functions $\mathbb{N}\to\mathbb{N}$ are primitive recursive. The proof requires that Tpr satisfies canonicity, which we easily prove using synthetic Tait computability.

Figures (3)

• Figure 1: Rules of $\mathrm{T}_{\mathrm{pr}}$.
• Figure 2: Higher Order Abstract Syntax for $\mathrm{T}_{\mathrm{pr}}$.
• Figure 3: Lifted Syntax for Canonicity

Theorems & Definitions (53)

• definition 1
• definition 2
• theorem 2.1: hofstra_aspects_2020ROMAN1989267Lambek1986IntroductionTH
• theorem 4.1
• proof
• remark 3
• remark 4
• theorem 6.1
• definition 5
• lemma 6