Аннотация
Вычисления на компьютере в плавающей арифметике всегда являются приближенными. Напротив, вычисления в рациональной арифметике (например, в компьютерной алгебре) всегда абсолютно точны и воспроизводимы как на других компьютерах, так и (теоретически) вручную. Поэтому такие вычисления могут быть доказательными в том смысле, что доказательство, полученное с их помощью, ничем не отличается от традиционного. Однако обычно такие вычисления в достаточно сложной задаче невозможны ввиду ограниченности ресурсов памяти и времени. Мы предлагаем механизм округления рациональных чисел при расчетах в рациональной арифметике, который решает эту проблему (ресурсов), т.е. вычисления по-прежнему могут быть доказательными, но уже не требуют неограниченных ресурсов. Приведен ряд примеров реализации стандартных численных алгоритмов в этой арифметике. Результаты имеют приложения к аналитической теории чисел. Библ. 22. Фиг. 3.