Re Dedekind versus Cauchy reals

Re Dedekind versus Cauchy reals

[Thomas Streicher]

Dear Paul and Andrej,

I was aware of the fact that locatedness is part of definition of Dedekind
cut it guarantees. It guarantees that there are close enough approximations
for any required degree of precision.
Having had a look at Andrej's slides I can't say that they provided me with
an understanding of the operational semantics of the language.
The impression I got is that he is using (kind of) interval arithmetic for
determining truth values of terms of type \Sigma. That's ok but doesn't
answer the question what is a computationally given real number.

Do I understand your approach correctly as follows: when given a Dedekind
cut as a mapping  c : Q -> 2_\bot and an accuracy eps then

     \exists p,q : Q  c(p) = 0 /\ c(q) = 1 /\ q-p < eps

is true and computing this truth value gives the witnesses p and q.

I.e. one evaluates terms of type \Sigma of the ASD language in a way
reminiscent of logic programming.

Thomas