Primitive Recursive Dependent Type Theory

Buchholtz, Ulrik Torben; Schipp von Branitz, Johannes

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 ####II-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 [18], work on Joyal's arithmetic universes [27], and Hugo Herbelin and Ludovic Patey's sketched Calculus of Primitive Recursive Constructions [16].We define a theory Tpr that is a subtheory of MLTT with two universes U0 : U1, such that all inductive types are finitary and U0 is restricted to not contain II-types:[EQUATION]We prove soundness such that all functions N → N are primitive recursive. The proof requires that Tpr satisfies canonicity, which we easily prove using synthetic Tait computability [36].

Citation

Buchholtz, U. T., & Schipp von Branitz, J. (2024, July). Primitive Recursive Dependent Type Theory. Presented at LICS '24: 39th Annual ACM/IEEE Symposium on Logic in Computer Science, Tallinn, Estonia

• Presentation Conference Type: Edited Proceedings
• Conference Name: LICS '24: 39th Annual ACM/IEEE Symposium on Logic in Computer Science
• Start Date: Jul 8, 2024
• End Date: Jul 12, 2024
• Acceptance Date: Apr 15, 2024
• Online Publication Date: Jul 8, 2024
• Publication Date: Jul 8, 2024
• Deposit Date: Oct 11, 2024
• Publicly Available Date: Jul 9, 2025
• Publisher: Association for Computing Machinery (ACM)
• Peer Reviewed: Peer Reviewed
• Volume: 24
• Article Number: 18
• Pages: 1-12
• Book Title: LICS '24: Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science
• DOI: https://doi.org/10.1145/3661814.3662136
• Public URL: https://nottingham-repository.worktribe.com/output/37140593
• Publisher URL: https://dl.acm.org/doi/10.1145/3661814.3662136
• Additional Information: Published: 2024-07-08