Category of Gödel Codings? [Reference Request]

Question

Consider computation with the integers $\mathbb{Q}$. The traditional theory of recursive functions on $\mathbb{N}$ applies to $\mathbb{Q}$ by the identification of $\frac{a}{b} \in \mathbb{Q}$ with $2^{a}3^{b} \in \mathbb{N}$. Similarly, if I have any similar unnamed structure I can proceed likewise, as follows:

First, note that in this process of "Gödel numbering" a given object may have more than one representative Gödel number in $\mathbb{N}$. However the set of valid Gödel numbers is primitive recursive and there is a primitive recursive equivalence relation that determines whether two numbers represent the same object.

This leads to the following category $\textsf{PRA}$: The objects of $\textsf{PRA}$ objects are pairs $(A, \sim _{A})$ where $A \subseteq \mathbb{N}$ is a primitive recursive set and $\sim _{A} \subseteq A \times A$ is a primitive recursive equivalence relation. The morphisms of $\textsf{PRA}$ are are functions $f: (A, \sim _A) \rightarrow (B, \sim _B)$ induced by primitive recursive functions $F: \mathbb{N} \rightarrow \mathbb{N}$ such that $x \sim _{A} y \Rightarrow F(x) \sim _{B} F(y)$.

This is all rather rudimentary and seems like the correct definition (to me) of a Gödel numbering and leads naturally to the category just described. However I have never seen this category described or studied. Is this category simply

1. Uninteresting, or perhaps
2. Unimportant?

Any references would be appreciated. [See comment below.]

Answer 1

You are about to invent realizability theory. The particular category you are suggesting is going to be some sort of a category of numbered sets, see this answer for a definition. Category-theoretic aspects of realizability are considered in Jaap van Oosten's book "Realizability - An Introduction to its Categorical Side". A less demanding text might be my PhD thesis, or some of the other links on the nLab realizability page, linked above.

Answer 2

I would like to second Andrej's answer as that was my first instinct as well. However I thought I would also give some links to related concepts. In particular if you are willing to change the natural numbers to some other set and use a different "notion of computability" then this idea appears in several places. For example:

Represented spaces and Type Two Effectivity (TTE)

Underlying set: Baire space ($\omega^\omega$)

Notion of Computable Function: Extensions of computable functions from $\omega^{<\omega}$ to $\omega^{<\omega}$.

References:

• "Computable Analysis" by Klaus Weihrauch.

  This is the standard text book.

• "On the topological aspects of the theory of represented spaces" by Arno Pauly

  This gives a more modern approach (and is much shorter).

Equilogical spaces

Underlying set : $T_0$-topological space.

Notion of Computability: Continuous functions.

References:

• nlab

Note one reason "continuous" can be thought of as "notion of computation" is a function from reals to reals is continuous if and only if it is computable relative to some oracle.

For more on effective analogs of continuous functions (and more complicated functions)

• "Descriptive Set Theory" by Yiannis Moschovakis

is excellent.

Borel Equivalence Relations

Underlying set: Borel Space

Notion of Computable Function: Borel function.

References:

• There is a chapter by Hjorth in the Handbook of Set Theory. You can find a link to it on his webpage: Hjorth

Computable Equivalence Relations

Underlying set: Natural Numbers

Notion of Computable Function: Computable function.

This is the analog of Borel reducibility for the natural numbers. This is relatively new to be studied.

References:

• "The hierarchy of equivalence relations on the natural numbers under computable reducibility" by S. Coskey, J. D. Hamkins, and R. Miller

Answer 3

Andrej and Nate have given good introductions to a number of "sophisticated" ideas in computability theory, but I would like to point out something elementary that ought perhaps to be said beforehand.

We have been doing practical computatation for at least seven decades now, so it mystifies me why theoretical compubaility still insists on basing all of its encodings on $\mathbb N$. We can all do actual computation in $\mathbb Q$, but it becomes absurdly infeasible if $p/q$ has to be encoded as $2^p 3^q$. This is unnecessary -- why do it?

The axioms for $\mathbb N$ use zero, successor and recursion. If we simply replace unary successor in this with a binary operation (pairing), written $[-|-]$, then we obtain a type $\mathbb T$ of finite binary trees that is sufficient to encode a large variety of computational objects in a way that is computationally feasible. From the definition it clearly satisfies $$ {\mathbb T} \equiv {\mathbb 1} + {\mathbb T} \times {\mathbb T}, $$ whilst also
$$ {\mathbf{List}} ({\mathbb T}) \equiv {\mathbb T} $$ by, for example, $[a,b,c,d] \equiv [a|[b|[c|[d|0]]]]$.

This form of encoding has been used in functional and logic programming languages at least since Lisp. Given that it differs so little from the natural numbers I don't understand why it is not adopted in coomputability theory. Of course $\mathbb T$ is isomorphic to $\mathbb N$, but the functions are ridiculously infeasible.