Dirk Pattinson
Institut fuer Informatik
LMU Muenchen, Germany
We consider initial value problems of the form
is a real vector field defined in a
neighbourhood of the origin. Extending v to intervals, Moore's
Method can be used to compute guaranteed enclosures of the
solution. In the process of computing the solution, conservative
outward rounding is applied if the result of arithmetic operations
cannot be represented exactly. As a consequence, only the
correctness of the result can be guaranteed, but no guarantees
regarding the speed of convergence of the implementation can be given.
We translate Moore's Method into the language of domain theory. The main technical tool is the so-called interval domain, which embodies notions both from recursion theory and classical analysis. In this framework, every computable real function is approximated by a chain of machine representable functions.
Moore's method for solving ODE's can thus be formulated as a continuous operator, which maps a convergent sequence of vector fields to an approximating sequence of interval valued functions. We show, that this operator can be restricted to bases of the associated domains, that is, on machine representable elements, only. We show that the resulting sequence of interval valued functions converges to a solution of the initial value problem and give an estimate on the speed of convergence. Because the bases of the involved domains can be directly represented as data types, our results on the speed of convergence are also sharp for an implementation of the domain theoretic framework.
The domain theoretic framework can be put to use with different bases, depending on the concrete nature of the problem. We discuss two such bases, consisting of piecewise linear and piecewise constant functions, respectively, and report on results of a prototypical implementation.