[Math] Difference between constructive Dedekind and Cauchy reals in computation

computability-theoryconstructive-mathematicslo.logic

If the Axiom of Countable Choice (ACC)

$$ \forall n\in \mathbb{N} . \exists x \in X . \varphi [n, x] \implies \exists f: \mathbb{N} \longrightarrow X . \forall n \in \mathbb{N} . \varphi [n, f(n)] $$

is not assumed in constructive mathematics, Dedekind and Cauchy real numbers are not equivalent in general. Even worse, Dedekind real numbers might not even form a set. Besides that, Dedekind cuts are notoriously unpleasant in terms of actual computation which is one of the most attractive parts of constructive mathematics. However, see Efficient Computation with Dedekind Reals by Bauer.

If we think of a Cauchy real as an algorithm that contains a convergence modulus $M_x: \mathbb{Z} \rightarrow \mathbb{N}$ and outputs rational approximations as:

$$ \left( x \in \mathbb{R} \right) \triangleq \left( \forall k \forall n,m \geq M_x(k) . \big| x(n) – x(m) \big| \leq 2^{-k} \right), $$

we then have a straightforward and transparent framework for computations (see, for instance, Schwichtenberg). On the other hand, in presence of the ACC, program extraction from proofs may get more difficult.

Dedekind reals are often used instead of Cauchy reals when ACC does not hold.

A Dedekind real is a defined as a pair $(L, U)$ of located sets of rational numbers satisfying:

$q \in L \iff \exists r.(q < r \land r \in L)$ and $q \in U \iff \exists r.(r < q \land r \in U)$
Both sets are inhabited: $\exists q. q \in L$ and $\exists q. q \in U$
Sets are disjoint: $ \neg (q \in U \land q \in L)$
(locatedness): $q < r \implies q \in L \lor r \in U$

What is the actual computational content of a Dedekind real in comparison to a (straightforward) Cauchy real? Can an efficient algorithm be derived for every constructive Dedekind real that outputs rational approximations with predictable accuracy (cf. modulus of convergence)? If yes, what is the difference between Cauchy and Dedekind algorithms?

Best Answer

In line with what is actually asked in the bold part of the question, I have taken the liberty of changing the title from constructive mathematics to computation. As it stood it was essentially a duplicate of another one, which already contains a lot about constructive but non-computational mathematics and so that would be the appropriate forum for further such discussion.

In fact Valery tagged the answer to the end of his first paragraph, namely @AndrejBauer's Efficient Computation with Dedekind Reals, which describes the ideas behind his Marshall calculator, whilst being based on our Dedekind Reals in Abstract Stone Duality and my Lambda Calculus for Real Analysis.

The setting for this answer is my ASD programme. I refuse to carry the baggage of obsolete programming languages (Turing Machines and Gödel Codings), any form of set theory (CZF, which I think is the setting for Lubarsky and Rathjen's paper, or even a topos) or the two bolted together (computable analysis in Weihrauch's TTE).

Valery's definition of a Dedekind cut is correct, but (to underline my rejection of any form of set theory) I write $\delta d$ and $\upsilon u$ for the down and up predicates instead of his $q\in L$ and $q\in U$ for lower and upper sets.

The predicate $\delta d$ says that (we so far know that) $d\lt x$ where $x$ is the real number being defined and similarly $\upsilon u$ means that (we so far know that) $x\lt u$.

Where this knowledge is incomplete, the pair $(\delta,\upsilon)$ satisfies all but the last axiom (locatedness) and is equivalent to an interval.

In particular, Dedekind cuts are two-sided. Taking the complement would amount to deducing knowledge or termination from ignorance or divergence.

There are plenty of examples of limiting processes that define "uncomputable" numbers that are best thought of as one-sided cuts. For example, the domain of definition of the solution of a differential equation is something that is only known from the inside; it is remarkable if we can obtain some knowledge from the outside, not that the boundary is "uncomputable" in this sense.

In the case where the cut defines a rational number, it should occur on neither side (Dedekind's choice was wrong here).

Defining the usual stuff in elementary real analysis is much easier and more natural using Dedekind cuts than with Cauchy sequences. Consider Riemann integration: $\delta d$ holds if there is some polygon (piecewise linear function) that lies below the curve and has area more than $d$; deducing the various properties from this is easy. This is gratuitously difficult if you insist in advance that the polygon have a particular shape of resolution $2^{-n}$ to make a Cauchy sequence.

The essential difference between a Dedekind cut and a Cauchy sequence as the representation of the solution of a mathematical problem is that Cauchy assumes that the problem has already been solved (to each degree of precision), whereas Dedekind merely combines all the formulae ("compiles" them into an "intermediate code", if you like), so that the problem remains to be solved.

This means that deriving a Cauchy sequence or decimal expansion from a Dedekind cut in general is just as difficult as solving a general real-valued mathematical problem. So I am under no illusion about the difficulty in implementing this proposal.

But it is a novel and so valuable way of looking at things.

The predicates define open subspaces of $\mathbb R$, so I would think that, in terms of recursion, they have to be $\Sigma^0_1$ or recursively enumerable. (I have thought a little bit about "descriptive set theory" (a name that needs to be changed) but haven't got very far with it.)

These predicates $\delta$ and $\upsilon$ are in the language of ASD and you will need to read the papers that I have linked to find out the details.

In the first instance, such predicates are built from $f(\vec x)\lt g(\vec x)$, where $f$ and $g$ are polynomials, using $\land$, $\lor$, $\exists$, recusion over $\mathbb N$ and universal quantification over closed bounded intervals.

We are given that $\delta d$ and $\upsilon u$ hold for certain rationals $d$ and $u$ and want to find some $d\lt m\lt u$ that is nearer to the result and whether $\delta m$ or $\upsilon m$.

In the case of $f(\vec x)\lt g(\vec x)$ we can use the (formal, interval) derivatives of $f$ and $g$ and the Newton--Raphson algorithm to do this. As is well known, this algorithm doubles the number of bits of precision at each step. This would justify the claim that the computation is efficient if we can extend it to more general formulae.

For more complicated logical expressions, Andrej developed a method of approximating these expressions with simpler ones. See his paper for details of this. This is quite closely analogous to methods of approximating real-valued functions by low(er) degree polynomials that have a very long history but have been developed in interval computation by Michal Konecny. Whilst Michal himself has used these computationally, they have not yet been incorporated into Andrej's calculator, but I hope that this will be done in future.

Computations like this with so-called "exact real arithmetic" are necessarily non-deterministic with regard to the Cauchy sequences tat they produce, which means that the existence of the completed sequence necessarily relies on Dependent Choice. This is entirely natural from a computational point of view and I don't see what use there is in discussing it as an issue of constructivity.

Related Solutions

[Math] What happens when we print the digits of a real number

[Edit: Following Carl Mummert's comments, I have improved the part about transformation of Cauchy sequences to digit expansions. Thanks to Carl for interesting observations.]

Your question is best divided into two subquestions:

Does every real number have a digit expansion?
What is the nature of the "process" of going from a real number to its digit expansion, assuming it has one.

For the purposes of this discussion let us say that the real numbers are defined a la Cauchy, i.e., $\mathbb{R}$ is the metric completion of $\mathbb{Q}$ equipped with the Euclidean metric. Let me also assume countable choice, so that $\mathbb{R}$ can be shown to exist. In particular, we can take $\mathbb{R}$ to be the set of Cauchy sequences quotiented by a suitable equivalence relation. (I am talking informal intuitionistic mathematics here and do not want to tell you what formal system I am in, but if you force me, I can tell you about various possibilities.)

We need to be careful about what is understood by "digit expansion" of a real number. Digit expansions are special kind of a Cauchy sequences: they are monotone and have a fixed rate of convergence. We have the following observations, none of which is hard to establish (assuming countable choice):

for every Cauchy sequence there exists one with a fixed rate of convergence (say the $n$-th term is within $2^{-n}$ of its limit), but a function mapping from the former to the later cannot be shown to exist.
every Cauchy sequence with a fixed rate of convergence (let me call such fast Cauchy sequences) has a monotone fast Cauchy sequence, and there is a function mapping the former to the later, as pointed out by Carl in the comments.
a decimal digit expansion is an infinite sequence, i.e., a member of $D = \lbrace 0, 1, \ldots 9\rbrace^\mathbb{N}$. We cannot prove constructively that every monotone fast Cauchy sequence has a corresponding digit expansion (again, by a continuity argument).
if we try to weasle out of the problem by taking only those reals which have a decimal digit expansion, then basic operations such as addition and multiplication cannot be shown to exist because they would be discontinuous.
as is well known, if we allow negative digits so that a digit expansion is a member of $\lbrace -9, -8, \ldots, 8, 9\rbrace^\mathbb{N}$ then every Cauchy sequence has a corresponding digit expansion, but now every real has very many digit expansions.

So I am going to assume that by "digit expansion" you mean one which can contain negative digits (otherwise your premise that every real has an expansion cannot be established). As you notice, there is no continuous map from reals to (negative) digit expansions. Nevertheless, one can write a program which takes a real number (represented by a rational Cauchy sequence with an explicit modulus of convergence, or some other equivalent form, such as a sequence of ensted intervals with rational endpoints) and produces one of its digit expansions. Such programs can be understood in several ways:

As realizers for the statement $$\forall x \in \mathbb{R} . \exists d \in D . \;\text{$d$ is digit expansion of $x$}.$$ This is my favorite. When we reason about real numbers in analysis, we rarely talk about digit expansions, so it does not matter if the computation of a digit expansion appears only implicitly as a realizer for a $\forall\exists$ statement.
We can formalize a distinction between an operation and a function. The former can be intensional, i.e., it does not have to repsect the equality of its domain, while the later must be extensional so that it maps equals to equals. This introduces certain subtleties that only logicians can appreciate. In this setting, the program is an operation which is not a function.
Such programs can be seen as realizers witnessing the totality of a multi-valued function that maps a real to the set of its digit expansions. Such a map is easily seen to exist. This is more manageable than option 2 and is popular in Type Two Effectivity.

In practice, you cannot hope to implement reals in such a way that each real receives only one representation. Even having finitely many representations is out of the question – some reals will necessarily have infinitely many representatives, or something will go wrong (arithmetical operations won't be computable, or the structure won't be closed under limits of (computable) Cauchy sequences, or the strict linear order won't be semidecidable). Classical decimal digit expansions are not computable, even though every single computable real has a decimal digit expansion. This shows the importance of thinking about spaces as whole entities, rather than each of its points in isolation. Or to be even more blunt: spaces are not determined by their points!

[Math] Axioms of Choice in constructive mathematics

The following is a proof in Coq, or am I missing something?

Goal forall (X : Set) (phi : nat -> X -> Prop),
    (forall (n : nat), {x : X | phi n x})
    -> {f : nat -> X | forall n, phi n (f n)}.
Proof.
  intros X phi all.

  exists (fun n => proj1_sig (all n)).
  intros n.
  destruct (all n).
  simpl.
  auto.
Qed.

Best Answer

Related Solutions

[Math] What happens when we print the digits of a real number

[Math] Axioms of Choice in constructive mathematics

Related Question