Contributions offered by Martin Escardo for topic
I (domain theory and real number computation)


TITLE: Effective and sequential definition by cases on the reals 
       via infinite signed-digit numerals

PREAMBLE (followed by a technical abstract):

It is a surprising fact, discovered by the constructive 
mathematician Brouwer in 1920, that potentially infinite decimal
numerals are not suitable for effective (exact) real number
computation. After this discovery, he and other mathematicians, 
logicians and computer scientists proposed many essentially 
equivalent concrete representations of real numbers that are 
suitable for constructive or mechanical computation.

In this paper we consider a variation of Brouwer's solution, 
proposed by Wiedmer in 1980 and further investigated by Boehm
and his collaborators, Di Gianantonio, and Weihrauch among others, 
which consists of the use of signed-digit numerals. One learns 
from Di Gianantonio (1996) that Leslie considered signed-digit 
numerals in 1817 from a philosophical point of view, and
from Suenderhauf (1995) that Cauchy observed in 1840 that 
signed-digit numerals simplify computations by hand. Avizienis 
proposed in 1964 signed-digit numerals as an efficient internal 
representation of finite-precision numbers for hardware 
implementation of arithmetic. Elegant algorithms for exact Riemann 
integration and global maximum determination via signed-digit 
numerals were recently developed by Alex Simpson.

It is a problem common to all approaches to exact real number
computation that (in)equality of real numbers is not decidable.
It has been shown that the so-called parallel-conditional
allows one to overcome this difficulty to a great extent. 
In this talk we show how overcome this problem in a sequential 
fashion. 

TECHNICAL ABSTRACT: 

The lexicographical and numerical orders on infinite 
signed-digit numerals are unrelated. However, we show that there 
is a computable normalization operation on pairs of signed-digit
numerals such that for normal pairs the two orderings coincide. 
In particular, one can always assume without loss of generality 
that any two numerals that denote the same number are themselves 
the same. We apply the order-normalization operator to easily 
obtain an effective and sequential definition-by-cases scheme in 
which the cases consist of (in)equalities between real numbers.

KEYWORDS: exact real number computation, domain theory, 
          parallel-conditional
------------------------------------------------------------------
TALK #2 (domains and locales)

If there is time available, I would like to also talk about a 
localic version of the so-called patch topology
(which includes the Lawson topology as a particular case).

TITLE: The compact-regular coreflection 
       of a stably locally compact locale

The Scott continuous nuclei form a subframe of the frame of
all nuclei (Lavwere-Tierney topologies). We refer to this subframe 
as the patch frame. We show, in an intuitionistic way, that the 
patch construction exhibits the category of Stone locales as
a coreflective full subcategory of the category of spectral 
locales and perfect maps. More generally, it exhibits the
category of compact regular locales as a coreflective full
subcategory of the category of stably locally compact locales
and perfect maps. Here a continuous map is perfect iff its 
associated frame homomorphism preserves the way-below relation 
iff its right adjoint is Scott continuous (topologically, iff 
it reflects compact upper sets).

(NB. The category of stably locally compact locales includes
(the point-free versions of) Scott domains, SFP domains, 
FS domains, and Lawson compact continuous dcpos (in ascending
generality), and at the same time Hausdorff objects like the
unit interval and Cantor space. So it is a convenient category
which includes classical and computational (point-free) spaces.)

---------------------------------------------------------------------------
Result of feedback submitted by
Escardo (mhe@dcs.ed.ac.uk) on Monday, August 24, 1998 at 18:28:41