# nLab Turing category

Contents

### Context

#### Constructivism, Realizability, Computability

intuitionistic mathematics

# Contents

## Definition

A Turing category is a certain categorification of partial combinatory algebras (PCAs) based on restriction categories.

###### Definition

(Turing category)

A Turing category is a cartesian restriction category $(\mathcal{C}, \bar{} )$ with a fixed object A and morphism $\bullet \colon A \times A \rightarrow A$ having the following universal property:

For each $\mathcal{C}$-morphism $f \colon X \rightarrow Y$ there is a section $s \colon Y \rightarrow A$ and retract $r \colon A \rightarrow X$, along with a total map $h \colon \mathbf{1} \rightarrow A$ making the following diagram commute:

While restriction structure captures the function partiality one finds in computability theory, the universal property stated above captures the universal coding of $\mathcal{C}$-morphisms into operations on the Turing object $A$, via the application $\bullet$. Indeed one recovers, as an example, the category $\mathbf{Rec}$, of natural numbers $n, m \in \mathbf{N}$ and partial recursive functions $\mathbf{N}^n \rightarrow \mathbf{N}^m$. This has universal applicative structure:

and universal representation $\langle i, n \rangle = f_i(n)$ of the $i$th computable function. In this case the PCA is Kleene's first algebra. More generally, the computable map category of any PCA forms a Turing category, with Turing object the PCA and its Turing morphism being the applicative structure.

And conversely, a Turing object $A$ of $\mathcal{C}$ and its Turing morphism $\bullet : A \times A \rightarrow A$ form a (relative) PCA. This is effectively a PCA-object internal to an appropriate category:

###### Definition

(Relative PCA)

A (relative) PCA $A$ is a combinatory complete partial applicative system in a cartesian restriction category $\mathcal{D}$, i.e. a morphism $\bullet : A \times A \rightarrow A$ in $\mathcal{D}$ such that finite powers $A^n$ and $A$-computable morphisms form a well-defined cartesian restriction subcategory of $\mathcal{D}$.

Note, however, that not every relative PCA in a Turing category $\mathcal{C}$ is a Turing object for $\mathcal{C}$.

### Basic properties

The arithmetical representation of a (partial) function $f : \mathbf{N} \rightarrow \mathbf{N}$ as a member of the recursive enumeration of relations $\varphi_i \subset \mathbf{N} \times \mathbf{N}$ is universal, and this representation satisfies the Kleene recursion theorems?:

$\bullet$ (smn) Let $f: \mathbf{N} \rightarrow \mathbf{N}$ be a partial computable function. Then there is a partial computable function $s : \mathbf{N} \rightarrow \mathbf{N}$ such that $f(\langle i, n \rangle) = f_{s(i)} (n)$.

$\bullet$ (utm) There is a partial computable function $U : \mathbf{N} \rightarrow \mathbf{N}$ such that $U(\langle i, n \rangle ) = f_i (n)$.

As can be nearly read off the definition above, these properties hold with respect to any Turing object. This is part of the overall motivation for Turing categories, since they provide a more model-independent setting both for stating the main theorems of recursion theory, while also allowing the βintrinsic meaningβ of different constructions in computability theory to stand out. For example, in Type II computability (or function realizability) it turns out that function computability with respect to the PCA $\mathbf{N}^\mathbf{N}$ (either as Kleene's second algebra or the Baire space of sequences) has the topological meaning of continuity. Hence, despite the universal availability of GΓΆdel-encodings of all β$A$-computationsβ for an appropriate data type $A$ into $\mathbf{N}$-computations (a form of the Church-Turing thesis), the theory of Turing categories and their applications to categorical realizability models, for example, are intended to give the intrinsic meaning of computational mathematics without resorting to such a universal representation, much like the success story of Type II computability.

(β¦)

(β¦)

## References

Turing categories were isolated categorically and named in:

Last revised on November 3, 2021 at 03:14:47. See the history of this page for a list of all contributions to it.