8
$\begingroup$

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.]

$\endgroup$
  • $\begingroup$ Do you maybe want $\sim_A\subseteq A\times A$ instead of $\mathbb{N}\times\mathbb{N}$? (Also, what is the "comment below"?) $\endgroup$ – Noah Schweber Mar 5 '15 at 17:54
  • $\begingroup$ The other obvious question is whether to allow arbitrary (total) recursive functions in this definition. But, I think in the context of the Kleene Normal form theorem I think it's clear using primitive recursive functions is the correct choice. The coding/uncoding that takes place during a computation should be simple and total by construction. Unbounded minimization should be required only once, as in the Kleene Normal Form theorem. $\endgroup$ – Rex Butler Mar 5 '15 at 18:01
  • $\begingroup$ See also: cs.nyu.edu/pipermail/fom/2005-August/009024.html $\endgroup$ – Rex Butler Mar 5 '15 at 18:16
18
$\begingroup$

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.

| cite | improve this answer | |
$\endgroup$
9
$\begingroup$

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:

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
| cite | improve this answer | |
$\endgroup$
  • $\begingroup$ Thanks for pointing out that realizability also incorporates the continuous version, namely TTE and equilogical spaces (and domain-theoretic representations as well). It would be interesting to see if the Borel stuff is of the realizability kind as well. $\endgroup$ – Andrej Bauer Mar 6 '15 at 7:31
  • $\begingroup$ am far from an expert on realizability or TTE, but my guess is that the relationship between the collection of equivalence relations on Borel spaces (with Borel maps between them) and realizability will have a very similar feel to the relationship between represented spaces (and continuous maps) and realizability. $\endgroup$ – Nate Ackerman Mar 6 '15 at 22:40
  • $\begingroup$ For example they both run into the issue that they are fundamentally only talking about equivalence relations on Baire space (as all Borel spaces of the same cardinality is isomorphic). This is something which isn't an issue with equilogical spaces. In particular I don't know if the category of represented spaces and continuous functions is Cartesian closed (although I imagine it wouldn't be to hard to check). $\endgroup$ – Nate Ackerman Mar 6 '15 at 22:40
  • $\begingroup$ A further analogy is that just as continuous maps can be thought of as "computable relative to an oracle" Borel maps really can be thought of as "higher computable relative to an oracle" where here higher computable is in the sense of $\alpha$-recursion theory (and the many equivalent variants of the notions) $\endgroup$ – Nate Ackerman Mar 6 '15 at 22:40
  • $\begingroup$ Categories of represented spaces are locally cartesian closed and regular. (I say "categories" because using the Baire space is just one option.) To get Borel realizability going we'd need to know whether there is a reasonable category of measurable spaces and measurable maps which is at least weakly cartesian closed. I thought about this once but did not get far, and my measure-theory colleagues refuse to think about "weakly cartesian closed". $\endgroup$ – Andrej Bauer Mar 7 '15 at 1:08
7
$\begingroup$

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.

| cite | improve this answer | |
$\endgroup$
  • $\begingroup$ I have wondered essentially the same thing myself. I'm glad I'm not alone in this. $\endgroup$ – Rex Butler Mar 6 '15 at 21:38
  • 1
    $\begingroup$ When I write that book on computable mathematics I will present classical computability as an arcane way of thinking about computation. I'll even add a hint of perversion to it. $\endgroup$ – Andrej Bauer Mar 7 '15 at 1:05

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.