Thomas Streicher asked about the "operational semantics" of the ASD calculus, and in particular computation with Dedekind cuts. As he says, the public documentation is rather limited at the moment, but Andrej and I don't want to give all our ideas away before we have made good use of them ourselves. The first thing that one should say about "operational semantics" is that mathematical formulae do NOT come with a prescibed way of computing them. A large part of what makes mathematics interesting is that there may be many ways of looking at a problem, besides the "obvious" one. The two situations in which notation does come with a preferred way of computing with it are long multiplication and lambda calculus, but even these cases are open to INGENUITY in finding better algorithms.
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.
Yes. In fact, there are two notions of locatedness, and this is the stronger one, which is necessary for arithemetic. There are some comments linking these ideas to the Archimedean axiom and the Conway numbers in Sections 11 and 12 of "The Dedekind reals in ASD".
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.
Yes, that's right, except that "a mapping c : Q -> 2_\bot" is not a very helpful way of formulating it. When computing a real number, what we have (going back very clearly to Archimedes) is a pair of logical formulae, each with a single free variable (p and q in your notation, d and u in ours). One of which says when p is less than the real number being computed, and the other when q is greater. In order to fix the precision, we add another constraint that squeezes them close together. Then, as Thomas rightly says,
one evaluates terms of type \Sigma of the ASD language in a way reminiscent of logic programming.
He claimed that this
doesn't answer the question what is a computationally given real number.
Yes, it does, exactly. Notice that the "real number" is only on the "outside" of the computation, and is only manifested when we want to print it out --- hence my earlier pun that it is "peripheral". The "guts" of the computation are with LOGICAL formulae.
The impression I got is that he is using (kind of) interval arithmetic for determining truth values
Yes, but interval arithmetic is only one of a variety of tools. Also, if you only think of intervals as a way of computing real numbers to a given precision, you miss their real power. Plainly, these intervals just get wider and wider. Really, one should think of interval analysis as USING CRUDE ARITHMETIC TO DERIVE STRONG LOGICAL INFORMATION ABOUT FUNCTIONS. For example, if, when a function f is applied to an interval [d,u] using Moore arithmetics, the result f[d,u] lies within an interval (e,t), which we may determine purely ARITHMETICALLY, then we know the LOGICAL statement that All x:[d,u]. e < f(x) < t. Since f is given, not just as a funtion in the set-theoretic sense of a collection of input--output pairs, but as a FORMULA in a certain language, we may differentiate it formally, and apply interval arithmetic to that, obtaining even stronger LOGICAL information about the behaviour of the function. Examining the language, the real work consists of manipulating inequalities between polynomials over certain ranges of the variables. Often we just want to know whether the inequality ALWAYS, SOMETIMES or NEVER holds. A simple way to answer this question may just be Moore-wise evaluation, Then there is the sitation where the inequality is f(x,y) > 0 in a certain rectangle. The polynomial defines a curve (=0) and two regions (<0 and >0). As we increase the precision, the curve becomes closer to being a straight line, and the main numerical computation is of the gradient of this line, and of a narrow rectangle that encloses the curve. Just as the well known Moore arithmetic provides a way of evaluating universally quantified statments, so Kaucher arithmetic with back- to-front intervals answers existential statements. I don't want to go into more detail that this, because we want to get the credit for making this work (although we are keen to invove more collaborators). But also, these are just SOME of the things that might be done, AFTER ESCAPING FROM THE MENTAL STRAITJACKET of computation with Cauchy sequences or intervals. Paul Taylor