Excursions on Exact Real-Number Computation
Martín Escardó
School of Computer Science,
The University of Birmingham
The subject of this talk has its origins in
intuitionistic/constructive/effective real analysis. It started in
around 1920 with some thoughts by Brouwer about calculation with
infinite decimal expansions and other realizations of real numbers.
Since then, it has split in various directions in mathematics and
logic, which will be briefly explored. There are many interesting and
surprising results, some negative (algorithms that one would expect to
exist turn out to be impossible) and some positive (algorithms whose
existence one would quickly dismiss turn out to be possible). Somewhat
puzzlingly, the three fields mentioned in the first paragraph don't
share the same sets of positive and negative results, even though all
of them are meant to capture the computational content of
analysis. I'll briefly indicate what is going on.
A recent direction, in computer science this time, has been (1) the
implementation of these ideas, and (2) the design of built-in abstract
data types for real numbers with infinite precision in traditional
programming languages. After briefly reporting some progress by
various people on (1), I'll discuss in more detail progress on (2),
including some notorious open problems.
