Abstrakt. Ett konstrukivt reellt tal kan förstås som en Cauchy-följd där både fundamentalföljden och konvergensmodulus bestäms av algoritmer. Aritmetiska operationer på reella tal ges av algoritmer som bearbetar sådana algoritmer. Aritmetiken blir exakt till skillnad från flyttalsaritmetik. Som en inledning till seminarieserien presenteras grundläggande begrepp och resultat om konstruktiva reella tal och funktioner på reella tal.
Referenser
Abstract: Interval analysis is the mathematical foundation of so called auto-validating algorithms. By computing with intervals instead of single real numbers, important properties of the real line can be captured and used when devising set-valued numerical algorithms. In this talk, we will give a brief introduction to the topic, and then discuss how to solve ordinary differential equations for entire sets of initial conditions.
This is a symposium is devoted to interval analysis, domain theory and constructive mathematics.
Venue: Lecture room 6111, MIC, Polacksbacken, Uppsala
Organisers: Viggo Stoltenberg-Hansen and Warwick Tucker
Abstracts of talks
Dirk Pattinson (Leicester), Continuous mathematics over discrete structures.
One standard way of synthesising modern-day computer science with continuous mathematics is to equip the underlying (classical) space with a discrete representation that allows to approximate all elements of the space of interest up to any given degree of accuracy. In a concrete computational setup, calculations are then performed on the representatives. For this purpose, domain-theoretic representations are often very fruitful, as they allow to deal with higher types, naturally qualify as topological spaces and can be easily adapted to deal with specific problems.
In this talk, I will survey different domain-theoretic representations for spaces involving real numbers, in particular the real line and the spaces $C^0([0,1]^n)$ and $C^1([0,1]^n)$ of continuous (resp. continuously differentiable) real-valued functions of $n$ variables. The versatility of the domain theoretic approach becomes apparent in concrete applications, and we discuss the intermediate value theorem and the inverse function theorem.
Helmut Schwichtenberg (LMU, Munich/Uppsala), Estimating solutions of ODEs.
We compare the interval analysis methods of Moore for estimating solutions of ODEs (first order, $k$-th order method) with related approaches in constructive analysis with witnesses.
Peter Schuster (LMU, Munich), Problems as solutions.
It is folklore that if a continuous equation has approximate solutions and - in a quantitative manner - at most one solution, then it has a (of course, uniquely determined) exact solution. I first review the standard ways to validate this heuristic principle both in classical mathematics and in constructive mathematics with countable choice, and then indicate how this can be carried over to the choice-free way of doing completions put forward by Mulvey, Stolzenberg, Richman, et al. Moreover, I sketch how the crucial "at most one" hypothesis can be obtained, by invoking Brouwer's fan theorem, from appropriate preconditions of a qualitative nature. In fact, the fan theorem is equivalent to the general validity of the implication from the qualitative to the quantitative uniqueness condition for continuous functions on a compact metric space.
Erik Palmgren (Uppsala), On localic completion of metric spaces.
Locale theory, or pointfree topology, may be regarded as an extension of domain theory where the notion of a covering is basic. This allows for a constructive treatment of compactness issues. The pointfree construction of the real numbers starts with intervals with rational endpoints and their interval arithmetic. Constructive covers of intervals are defined by an inductive method. In this talk we present a generalisation of this construction to metric spaces due to Lawvere and Vickers. We relate this localic notion of metric space to the standard notion of constructive metric space with special attention to compactness properties.
Last change 2006-03-02 by Erik Palmgren