"new foundations must give new math"
from "The Basic Picture. Structures for constructive
topology"
by Giovanni Sambin, Oxford University Press, forthcoming
To register send an e-mail to maietti @ math.unipd.it
Registration fee: 40 euros
(to be paid at arrival).
Dipartimento di Matematica Pura ed Applicata, Università degli Studi di Padova, Italy
University of Padova, Italy
AILA (Italian Association of Logic and Applications), whose first president was Giovanni Sambin (from 1987 to 1994).
Andrej Bauer
Ljubljana
Efficient Computation with Dedekind Reals
Cauchy's construction of reals as sequences of rational approximations
is the theoretical basis for a number of implementations of exact
real numbers, while Dedekind’s construction of reals as cuts has inspired
fewer useful computational ideas.
Nevertheless, we can see the computational content of Dedekind reals
by constructing them within Abstract Stone Duality (ASD), a computationally
meaningful calculus for topology. This provides the theoretical background
for a novel way of computing with real numbers in the style of logic
programming.
Real numbers are defined in terms of (lower and upper) Dedekind cuts,
while programs are expressed as statements about real numbers in the
language of ASD. By adapting Newton's method to interval arithmetic
we can make the computations as efficient as those based on Cauchy
reals.