Small TYPES workshop

Constructive analysis, types and exact real numbers.

I'll review some results and open questions on operational and denotational semantics of programming languages with abstract data types for real-numbers, by myself and others, where real numbers are taken in the sense of recursion theory or of constructive mathematics.

Positive results include computational adequacy (good match of the operational and denotational semantics), an invariance result for the notion of computability at higher types, and a universality result for a family of languages (all computable function(al)s of all orders are programmable).

Partial results include the coincidence of the ‘abstract' or extensional approach with the intensional approach up to order two (where e.g. integration functionals live). The coincidence from order three onwards is open, but there are interesting results in this direction, which reduce the problem to a purely topological question.

A negative result on ‘sequential' computation in the presence of data abstraction has bad consequences regarding efficient implementation of such languages.

Thus, a major open problem is how to reconcile data abstraction with efficiency, so that such languages can be used in practice. It has been shown that the negative effect can be overcome to some extent by the introduction of a certain form of non-determinism, but much work remains to be done in this area. Several questions and problems in this direction will be formulated in the talk.

An implementation of exact arithmetic on the real numbers has to fulfill many (antithetic) demands: On the one hand, its use must be as easy as possible, handling of exact reals should be similar to ordinary floating point numbers. The implementation has to be very efficient, close to the speed of the hardware. Imperative programming languages are still state of the art for numerical purposes. On the other hand, computability on real numbers deals with infinite objects and infinite computations. Multi-valued functions are needed to relax continuity constraints, also lazy evaluation can be advantageous. Limits of sequences are the basis for calculus and numerical analysis, which must be reflected in an implementation. In this talk, we will explain how the iRRAM package for exact real arithmetic tries to match many of these points: For simple applications, it is almost as fast as interval packages based on double precision floating points numbers, but smoothly extends to cases where fixed precision is not enough and exact reals simplify programming.

We will explain the theoretical background to the RealLib library for exact real number arithmetic and some of the practical problems that have arised during the development of the library along with the solutions we have used.

COMP stands for ‘Collection Of Mathematical Programs'. But the COMP project aims further than just providing software: its main goal is to give creedence to the motto that ‘Constructive Mathematics equal Computable Mathematics'.

The first subgoal is to show that abstraction can be profitably reconciled with usability. For COMP, it means that using a pure functional language (Haskell) doesn't hurt too much the timings, while allowing further progress: more conceptual algorithms, code more easily proven, support for more abstract objects and computing.

As of now, only real numbers and basic operations on them are implemented. In this talk, I will try to show what the original approach of COMP means both conceptually and in practice, as compared to other efforts towards exact real numbers.

We consider the problem of constructivising elementary homotopy theory, and how it may be resolved using fo rmal topology.

A implementation of constructive real numbers already exists for Coq from the C-Corn project; however, this implementation is not optimized for speed. My project is to implement a reasonably fast constructive real number library, a nd prove the functions are equivalent to the C-Corn functions.

I will discuss the approach I intend to take, and examine a Haskell prototype. Comments and criticisms will be welcome.

The sum of two periodic functions need not be periodic. Consider for example the sum of the functions sin(x) and sin(sqrt(2)x). Fortunately, such a sum is almost periodic and much of the (Fourier) theory of periodic functions carries over. Unfortunately, constructively matters are complicated by the fact that the almost periodic functions form an inseparable normed space. As such, it has been a challenge for constructive mathematicians to find a natural treatment of them. In this talk we will present a simple constructive proof of Bohr's fundamental theorem for almost periodic functions which we then generalise to almost periodic functions on general topological groups.

The proof of the Kepler conjecture given by Thomas C. Hales in 1998 makes intensive use of computer calculations. In particular, it relies on the correctness of many inequalities over real numbers. For this purpose a formalization of interval arithmetic with some refinements, such as branch-and-bound and monotonicity checks, is presented. The ultimate goal of this work is to develop a reflectional Coq tactic for real inequalities and its correctness proof.

The MathXpert computer algebra system is one of the few computer algebra systems that tries to be logically sound. It implements basic algebra and analysis on the high school level, and for educational purposes is as faithful to high school textbooks as possible.

MathXpert gives its users 1702 ‘operations' that can be applied to expressions inside the system. We will show that it is easy to mimic the MathXpert architecture inside the HOL Light proof assistant, so that one gets MathXpert-style ‘operations' available there as well, but with the advantage that they also generate proofs, so that the correctness of the algebraic manipulations will be guaranteed by the proof assistant.

The aim of this talk is to study how Haskell programs manipulating exact representations of real numbers can be encoded in the Coq system in a way that ensures both that the code can be extracted and that its correctness properties can be proved. The main inspirations come from the work of Edalat and Potts and Niqui. In the current state of experiments, the correctness proofs rely on an axiomatic, non constructive presentation of real numbers.

Tis talk will describe the latest developments in the MPFR library in the last two years, and future plans for the next two years. This is joint work with Vincent Lefèvre, Patrick Pelissier and Laurent Fousse.

Exact real number arithmetic has had the reputation of being excessively slow in comparison to standard machine precision floating point. Even in cases where high precisions are not neccessary, real number systems tend to take hundreds of times longer to compute their results.

RealLib is a system that changes this. It uses an approach that treats functions on real numbers as lower-type objects, which allows it to run very close to the computer hardware. As a result, real number computations with RealLib can run nearly as fast as floating point computations with double precision.

One objective of COMP is to make the mathematician feel at home, computing with COMP, even if he doesn't know anything about floating point numbers, programming or computing architectures. If he means ‘Log x', then he should type ‘Log x' - and that should mean the exact same thing as in mathematics.

Straight from the beginning, there is no place for unreliability in COMP. Each answer of the system has to be correct - barring bugs, of course - and no computation shall be left to go on forever.

So COMP gives the user the full responsibility for the data he's providing. For example, if he wants to know the inverse of a number, he should give a lower bound to the number. This is a strong departure from usual practice - but a departure that is expected to have great rewards as the project goes forward towards its goals.