Interval Analysis Without Intervals

This paper applies Abstract Stone Duality to computation with real numbers.

We argue that Dedekind completeness and the Heine–Borel property should be seen as part of the “algebraic” structure of the real line, along with the usual arithmetic operations and relations. Dedekind cuts provide a uniform and natural way of formulating differentiation, integration and limits. They and these examples also generalise to intervals. Together with the arithmetic order, cuts enjoy proof-theoretic introduction and elimination rules similar to those for lambda abstraction and application. This system completely axiomatises computably continuous functions on the real line.

We show how this calculus (of “single” points) can be translated formally into Interval Analysis, interpreting the arithmetic operations a la Moore, and compactness as optimisation under constraints. Notice that interval computation is the conclusion and not the starting point.

This calculus for the real line is part of a more general recursive axiomatisation of general topology called Abstract Stone Duality.

Download the paper to print it

PDF,  DVI,  compressed PostScript  or  A5 booklet.

Table of contents

1. Introduction

2. Natural axioms for the real line

3. Dedekind cuts and intervals

4. Cuts and intervals in analysis

5. Type theory for Dedekind cuts

6. The translation

7. The Heine–Borel property

8. Proof of the central proposition

References

This document was translated from L^AT_EX by H^EV^EA.