Primitive Recursive Dependent Type Theory
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , |
|---|---|
| Format: | Preprint |
| Publié: |
2024
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866909156139597824 |
|---|---|
| author | Buchholtz, Ulrik von Branitz, Johannes Schipp |
| author_facet | Buchholtz, Ulrik von Branitz, Johannes Schipp |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2404_01011 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Primitive Recursive Dependent Type Theory Buchholtz, Ulrik von Branitz, Johannes Schipp Logic Logic in Computer Science 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. |
| title | Primitive Recursive Dependent Type Theory |
| topic | Logic Logic in Computer Science |
| url | https://arxiv.org/abs/2404.01011 |