Formal Proof of the Fundamental Theorem of Decorated Interval Arithmetic

Abstract

<p>Interval arithmetic is used to enclose roundoff, truncation, and modeling errors in interval methods, thus obtaining numerical methods with automatic verification of the results. The Fundamental Theorem of Interval Arithmetic (FTIA) shows that, when evaluating an expression using interval arithmetic, the computed result contains the mathematically correct value of the expression.</p> <p>Decorations were introduced in the IEEE P1788 working group for standardizing interval arithmetic. Their role is to help track properties of interval evaluations. That is, we wish to say if a function is defined, undefined, or continuous in its inputs. Moreover, decorations act as local exception flags and do not lead to interruption of the computations. The FTIA plus the decoration system is expanded into the Fundamental Theorem of Decorated Interval Arithmetic (FTDIA).</p> <p>Several versions of this theorem are formulated and proved by J. Pryce. This thesis formalizes and proves the core of this theorem (version 3.0 of the IEEE-P1788 proposal) using the theorem prover Coq. Namely, we prove it for the common case where all the inputs to a function are non-empty intervals.</p> <p>There are two distinctive features of our formalization and proof. First, we define the semantics of an interval as a set of real numbers (including the empty set), and we do not impose any other restrictions on such a set, except that models of this interval can decide if the set is empty or not. For example, an interval need not be closed and bounded, as in traditional interval arithmetic. Second, our formalization and proof do not rely on specific interval operations: it works with any interval operation that satisfies the requirements for decorated interval library operations.</p> <p>As the FTDIA is central to the IEEE-P1788 proposal, the correctness of the FTDIA is crucial. Our mechanized proof can give the research community in interval computations much confidence in its correctness. The current version of the FTDIA (in P1788 version 8.0) is slightly different from the theorem proved here. Modifying our proof to reflect this is left as future work.</p>