Доказательные вычисления

Материал из Википедии — свободной энциклопедии
Перейти к: навигация, поиск

Доказательные вычисления — целенаправленные вычисления на ЭВМ, комбинируемые с аналитическими исследованиями, которые приводят к строгому установлению новых фактов и доказательству теорем[1].

Достоверные вычисления[править | править вики-текст]

Одним из часто применяемых методов доказательных вычислений являются достоверные вычисления. Под достоверными вычислениями понимаются численные методы с автоматической верификацией точности получаемых результатов[2]. Довольно часто доказательные вычисления строятся на основе интервального анализа, где вместо вещественных чисел рассматриваются интервалы, которые определяют точность величин. Интервальный анализ широко применяется для вычислений с гарантируемой точностью в условиях машинной арифметики.

Примеры[править | править вики-текст]

В теории чисел[править | править вики-текст]

Благодаря тому, что теория чисел во многом оперирует целыми числами, использование доказательных вычислений в теории чисел оказывается очень плодотворным.

  • Утверждается, что число Мерсенна M_{43112609} = 2^{43112609} - 1 является простым. Проверить этот факт теоретически возможно человеку, но практически только с использованием вычислительной техники.
  • Л. Эйлер выдвинул гипотезу, что уравнение x^5_1+x^5_2+x^5_3+x^5_4=x^5_5 не имеет решений в целых положительных числах. Однако позднее было показано, что существует как минимум одно решение:
x_1=27, x_2=84, x_3=110, x_4=133, x_5=144.

Причем это решение было найдено с помощью перебора на компьютере[1].

В теории графов[править | править вики-текст]

Одно из наиболее известных успехов применения доказательных вычислений в теории графов является решение проблемы четырёх красок. Эта знаменитая задача была поставлена 1852 году и формулируется следующим образом: «выяснить, можно ли всякую расположенную на сфере карту раскрасить четырьмя красками так, чтобы любые две области, имеющие общий участок границы, были раскрашены в разные цвета». В 1976 году К. Аппель и В. Хакен с помощью доказательных вычислений показали, что так можно раскрасить любую карту.

В гидродинамике[править | править вики-текст]

Применением доказательных вычислений в математических задачах гидродинамики систематически занимались в Институте прикладной математики им. М. В. Келдыша РАН под руководством К. И. Бабенко. Примером является следующая теорема, полученная с помощью доказательных вычислений[3].

Теорема. При \alpha=1.02 и R=6000 спектральная задача Орра — Зоммерфельда имеет собственное значение, лежащее в полуплоскости \mathrm{Re}\,\lambda>0. Следовательно, в линеаризованной постановке при этих параметрах течение Пуазёйля неустойчиво.

Примечания[править | править вики-текст]

  1. 1 2 Бабенко К. И.  Основы численного анализа. — М.: Наука, 1986.
  2. Кулиш У., Рац Д., Хаммер Р., Хокс М. Достоверные вычисления. Базовые численные методы. — РХД, 2005.
  3. Бабенко К. И., Васильев М. М. О доказательных вычислениях в задаче об устойчивости течения Пуазейля // ДАН СССР. — 1983. — Т. 273. — № 6. — С. 1289—1294.

См. также[править | править вики-текст]

Ссылки[править | править вики-текст]