FOM: Precision and Turing-computability

[Vladimir N. Krupski]

References:
        D Richardson - RE: FOM: Precision and Turing-computability
<Pine.GSO.4.04.10205301127180.28830-100000 at mary.bath.ac.uk>

I don't believe that the symbolic computations and computable reals are
so close to each other as we may suppose.

The honest symbolic computations deal not with numbers
but with terms of some formal language. They never answer a question
"How much ?". It may be a derivation of something like "expr=3.14..."
but it is the user who should guess what does it mean. If he wants to
compare the result with Pi or with 3 -- he should try to prove
the corresponding statements ("expr=Pi" or "expr>3") by other
symbolic computation. Nothing strange that he may fail --
practically interesting theories usually are incomplete.

How do we  want to use something like computable reals or computable
algebras ... here? We may want to have an admissible rule like this:
 In order to prove an equality "expr1=expr2" do
 1) chose some special computable algebra;
 2) evaluate expr1, expr2 in it;
 3) expr1=expr2 is provable when these values coincide.
But the limitation is that practically interesting theories
should be incomplete, so this method should not work for every
equality. Thus we should not seek for a correct universal notion of
computable reals. It is better to look at a particular form of
equality and to investigate the decidability problem for corresponding
fragment of the ground theory. Only after we obtain the answer
"decidable"
we may seek for a good decision procedure and  may be some rule like
this
will work. But no hopes to have any unique class of  "good numbers with
good enumeration".

I suppose that negative results can be proved here -- something like
"if a countable set of reals is closed under the operations ...
then it does not have enumerations for which all operations are
computable and equality -- decidable".  And ... hardly contains all
the operations which a pocket calculator can perform.
Or some negative results about complexity. For example,
1) a lower complexity bound  for testing the equality x=y
when x,y are algebraic numbers represented by corresponding
polynomials; 2) something which states that this bound is also
valid when we choose any other good enumeration of algebraic numbers.

The problem is that these are negative results, they don't give anything

which _helps_ to do computations.

Vladimir N. Krupski
Associate Professor
Department of Mathematical Logic and Theory of Algorithms
Laboratory of Logical Problems in CS
Faculty of Mechanics and Mathematics
Moscow State University, Russia.

homepage: http://lpcs.math.msu.ru/~krupski/
e-mail: krupski at lpcs.math.msu.ru  (office)
             kru at voll.math.msu.su      (home)