Abstract:
Computations on a computer with a floating point arithmetic are always approximate. Conversely, computations with the rational arithmetic (in a computer algebra system, for example) are always absolutely exact and reproducible both on other computers and (theoretically) by hand. Consequently, these computations can be demonstrative in a sense that a proof obtained with their help is no different from a traditional one (computer assisted proof). However, usually such computations are impossible in a sufficiently complicated problem due to limitations on resources of memory and time. We propose a mechanism of rounding off rational numbers in computations with rational arithmetic, which solves this problem (of resources), i.e., computations can still be demonstrative but do not require unbounded resources. We give some examples of implementation of standard numerical algorithms with this arithmetic. The results have applications to analytical number theory.
