Formal aspects of correctness and optimality of interval computations

An interval is a continuum of real numbers, defined by its end-points. Interval analysis, proposed by R. Moore in the 50's, concerns the discovery of interval functions to produce bounds on the accuracy of numerical results that are guaranteed to be sharp and correct. The last criterion, correctness, is the main one since it establishes that the result of an interval computation must always contains the value of the related real function. Correctness rests on the "Fundamental Theorem of Interval Arithmetic". This theorem, induced us to define interval representations, which captures the fact that interval analysis works like a kind of language to express computations with real numbers, this is implicitly formulated at [HJE01] p. 1045, lemma 2. Until now the idea of intervals as representation of real numbers was not explicitly defined and its relation with some aspects of interval analysis was not explored. Here we show some of these relations in terms of the topological aspects of intervals (Scott and Moore topologies). The paper also defines what we call the canonical interval representation of a real function, which is the obvious best "mathematical" (not necessarily computable) interval representation of a real function f. The idea is to show some properties of correct interval algorithms giving a relationship with some other kind of functions, such as extensions and inclusion monotonic functions; and to show how this ideal object preserves the continuity of real functions into Scott and Moore topologies.