nLab Turing category




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


(Turing category)

A Turing category is a cartesian restriction category (π’ž,Β―)(\mathcal{C}, \bar{} ) with a fixed object A and morphism β€’:AΓ—Aβ†’A\bullet \colon A \times A \rightarrow A having the following universal property:

For each π’ž\mathcal{C}-morphism f:Xβ†’Yf \colon X \rightarrow Y there is a section s:Yβ†’As \colon Y \rightarrow A and retract r:Aβ†’Xr \colon A \rightarrow X, along with a total map h:1β†’Ah \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 AA, via the application β€’\bullet. Indeed one recovers, as an example, the category Rec\mathbf{Rec}, of natural numbers n,m∈Nn, m \in \mathbf{N} and partial recursive functions N nβ†’N m \mathbf{N}^n \rightarrow \mathbf{N}^m. This has universal applicative structure:

and universal representation ⟨i,n⟩=f i(n)\langle i, n \rangle = f_i(n) of the iith 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 AA of π’ž\mathcal{C} and its Turing morphism β€’:AΓ—Aβ†’A\bullet : A \times A \rightarrow A form a (relative) PCA. This is effectively a PCA-object internal to an appropriate category:


(Relative PCA)

A (relative) PCA AA is a combinatory complete partial applicative system in a cartesian restriction category π’Ÿ\mathcal{D}, i.e. a morphism β€’:AΓ—Aβ†’A\bullet : A \times A \rightarrow A in π’Ÿ\mathcal{D} such that finite powers A nA^n and AA-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:Nβ†’Nf : \mathbf{N} \rightarrow \mathbf{N} as a member of the recursive enumeration of relations Ο† iβŠ‚NΓ—N\varphi_i \subset \mathbf{N} \times \mathbf{N} is universal, and this representation satisfies the Kleene recursion theorems?:

β€’\bullet (smn) Let f:Nβ†’Nf: \mathbf{N} \rightarrow \mathbf{N} be a partial computable function. Then there is a partial computable function s:Nβ†’Ns : \mathbf{N} \rightarrow \mathbf{N} such that f(⟨i,n⟩)=f s(i)(n)f(\langle i, n \rangle) = f_{s(i)} (n).

β€’\bullet (utm) There is a partial computable function U:Nβ†’NU : \mathbf{N} \rightarrow \mathbf{N} such that U(⟨i,n⟩)=f i(n)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 N N\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 β€œAA-computations” for an appropriate data type AA into N\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.

More Examples


Weak Limits and Exact Completions



Turing categories were isolated categorically and named in:

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