Skip to main content
deleted 2 characters in body
Source Link
Andrej Bauer
  • 31.2k
  • 1
  • 73
  • 119

Arno's answer provides some very useful background reading material, I would just like to address your specific question about $\mathbb{R}$.

Let us first recall a result by Peter Hertling, see Theorem 4.1 in A Real Number Structure that is Effectively Categorical (PDF here), about computable structure of the real numbers. Suppose we have a representation of $\mathbb{R}$, i.e., a data structure representing the reals, such that:

  • $0$ and $1$ are computable elements of $\mathbb{R}$,
  • the field operations $+$, $-$, $\times$ and $/$ are computable (where division by zero is of course undefined)
  • the limit operator, taking a rapid Cauchy sequence to its limit, is computable (a sequence $(x_n)_n$ is rapid when $|x_n - x_m| \leq 2^{-\min(m,n)}$).
  • the strict order $<$ is semidecidable

The above conditions simply state that the reals should be a computable Cauchy ordered field, which is pretty much the computable version of the usual chracterization of reals (the Archimedean axiom holds as well, as it turns out).

Then it follows that:

  1. The topology of $\mathbb{R}$ is the standard Euclidean topology
  2. Equality is undecidable, or equivalently, testng for zero is undecidable.
  3. Any two such structures are computably isomorphic.

These are unavoidable facts. Your teacher may think that not having decidable equality is unfortunate, or that division by zero should report an error, but that is impossible to arrange if one wants to keep the computable structure of the reals.

Regarding your implementation: it is vitalvital that you represent a real with a Cauchy sequence together with information on how fast it converges. I hope you did that.

Arno's answer provides some very useful background reading material, I would just like to address your specific question about $\mathbb{R}$.

Let us first recall a result by Peter Hertling, see Theorem 4.1 in A Real Number Structure that is Effectively Categorical (PDF here), about computable structure of the real numbers. Suppose we have a representation of $\mathbb{R}$, i.e., a data structure representing the reals, such that:

  • $0$ and $1$ are computable elements of $\mathbb{R}$,
  • the field operations $+$, $-$, $\times$ and $/$ are computable (where division by zero is of course undefined)
  • the limit operator, taking a rapid Cauchy sequence to its limit, is computable (a sequence $(x_n)_n$ is rapid when $|x_n - x_m| \leq 2^{-\min(m,n)}$).
  • the strict order $<$ is semidecidable

The above conditions simply state that the reals should be a computable Cauchy ordered field, which is pretty much the computable version of the usual chracterization of reals (the Archimedean axiom holds as well, as it turns out).

Then it follows that:

  1. The topology of $\mathbb{R}$ is the standard Euclidean topology
  2. Equality is undecidable, or equivalently, testng for zero is undecidable.
  3. Any two such structures are computably isomorphic.

These are unavoidable facts. Your teacher may think that not having decidable equality is unfortunate, or that division by zero should report an error, but that is impossible to arrange if one wants to keep the computable structure of the reals.

Regarding your implementation: it is vital that you represent a real with a Cauchy sequence together with information on how fast it converges. I hope you did that.

Arno's answer provides some very useful background reading material, I would just like to address your specific question about $\mathbb{R}$.

Let us first recall a result by Peter Hertling, see Theorem 4.1 in A Real Number Structure that is Effectively Categorical (PDF here), about computable structure of the real numbers. Suppose we have a representation of $\mathbb{R}$, i.e., a data structure representing the reals, such that:

  • $0$ and $1$ are computable elements of $\mathbb{R}$,
  • the field operations $+$, $-$, $\times$ and $/$ are computable (where division by zero is of course undefined)
  • the limit operator, taking a rapid Cauchy sequence to its limit, is computable (a sequence $(x_n)_n$ is rapid when $|x_n - x_m| \leq 2^{-\min(m,n)}$).
  • the strict order $<$ is semidecidable

The above conditions simply state that the reals should be a computable Cauchy ordered field, which is pretty much the computable version of the usual chracterization of reals (the Archimedean axiom holds as well, as it turns out).

Then it follows that:

  1. The topology of $\mathbb{R}$ is the standard Euclidean topology
  2. Equality is undecidable, or equivalently, testng for zero is undecidable.
  3. Any two such structures are computably isomorphic.

These are unavoidable facts. Your teacher may think that not having decidable equality is unfortunate, or that division by zero should report an error, but that is impossible to arrange if one wants to keep the computable structure of the reals.

Regarding your implementation: it is vital that you represent a real with a Cauchy sequence together with information on how fast it converges. I hope you did that.

Source Link
Andrej Bauer
  • 31.2k
  • 1
  • 73
  • 119

Arno's answer provides some very useful background reading material, I would just like to address your specific question about $\mathbb{R}$.

Let us first recall a result by Peter Hertling, see Theorem 4.1 in A Real Number Structure that is Effectively Categorical (PDF here), about computable structure of the real numbers. Suppose we have a representation of $\mathbb{R}$, i.e., a data structure representing the reals, such that:

  • $0$ and $1$ are computable elements of $\mathbb{R}$,
  • the field operations $+$, $-$, $\times$ and $/$ are computable (where division by zero is of course undefined)
  • the limit operator, taking a rapid Cauchy sequence to its limit, is computable (a sequence $(x_n)_n$ is rapid when $|x_n - x_m| \leq 2^{-\min(m,n)}$).
  • the strict order $<$ is semidecidable

The above conditions simply state that the reals should be a computable Cauchy ordered field, which is pretty much the computable version of the usual chracterization of reals (the Archimedean axiom holds as well, as it turns out).

Then it follows that:

  1. The topology of $\mathbb{R}$ is the standard Euclidean topology
  2. Equality is undecidable, or equivalently, testng for zero is undecidable.
  3. Any two such structures are computably isomorphic.

These are unavoidable facts. Your teacher may think that not having decidable equality is unfortunate, or that division by zero should report an error, but that is impossible to arrange if one wants to keep the computable structure of the reals.

Regarding your implementation: it is vital that you represent a real with a Cauchy sequence together with information on how fast it converges. I hope you did that.