К доказательному программированию для непрерывных данных (Николай Непейвода, OSEDUCONF-2026)

Ссылки сюда (1) →

Короткая ссылка: 20260208C

Докладчик

Николай Непейвода

Рассматриваются фундаментальные различия между алгоритмикой для дискретных и непрерывных объектов и показывается, что классические модели вычислимости адекватны прежде всего для дискретных задач. Опираясь на результаты конструктивной математики, демонстрируется связь непрерывности и относительной вычислимости, а также невозможность полноценной работы с действительными числами в рамках традиционных подходов к программированию без явной спецификации точности.

Особое внимание уделяется проблемам равенства и недетерминированности в вычислениях над действительными числами. Показывается, что точное равенство в непрерывной среде неконструктивно, а корректные программы должны работать с оценками точности и учитывать приближённый характер входных и выходных данных. Предлагаются принципы замещения равенства оценками и использования контролируемой недетерминированности.

Формулируются практические рекомендации по конструктивизации программ и их спецификаций:

• необходимость явного задания точности данных и результатов,
• введения «окрестностного отношения» как характеристики программы
• разработки методики построения логически корректных непрерывных программ в среде свободного программного обеспечения.

Видео

on youtube

Презентация

Thesis

Теоретическая прелюдия

Алгоритмика для работы с точными дискретными объектами и непрерывными, заданными приближениями, принципиально отличается. Теоретическим аспектам алгоритмики для топологических объектов занимается конструктивная математика, итоги 120-летнего развития которой подведены в фундаментальной коллективной монографии. Значительная часть этих работ посвящена конструктивизации и вычислимости для хаусдорфовых пространств со счётной базой окрестностей, которыми почти всегда являются структуры, основанные на действительных числах. При этом конструктивные функции и функционалы всегда оказывались непрерывными. Но не любая непрерывная функция была конструктивной. Причины этого оказалось возможным полностью прояснить.

В работе на базе соединения понятия относительной вычислимости, конструктивизации произвольных хаусдорфовых пространств со счётной базой, рекурсивных схем, типизированного λ-исчисления и методов суперкомпиляции доказано, что функция непрерывна тогда и только тогда, когда она вычислима относительно некоторой целочисленной функции. При этом для каждой вычислимой функции имеется окрестностное отношение, показывающее, какой окрестности аргумента достаточно для вычисления каждой окрестности результата. Но вычислить это отношение, имея лишь конструктивную функцию, невозможно, нужно знать и преобразовать её программу методами суперкомпиляции.

Работу конструктивной функции можно охарактеризовать следующей схемой:

Работа с конечной информацией

Практика программирования показала, что функциональные программы для дискретных и непрерывных задач пишутся в разном стиле. Стандартное в информатике определение вычислимости через машины Тьюринга либо λ-исчисление прагматически корректно прежде всего для дискретных задач. Более того, для работы с функционалами высокого порядка машины Тьюринга практически непригодны: они приспособлены лишь обрабатывать первопорядковую функцию как бесконечную ленту с записями только для чтения. Тем самым они оказываются недостаточно адекватны уже для вычислимости над действительными числами.

Фундаментальный результат Крайзеля и Трулстра показал, что моделью вычислимости с неполной информацией служит не алгоритм, а относительная вычислимость. Она представляется как алгоритмическое устройство, программу в котором мы не знаем, принимающее на входы дискретную информацию, физический датчик, моделируемый в первом приближении беззаконной последовательностью, знания о которой исчерпываются уже полученными данными, и творческой последовательностью, моделирующей действия человека-оператора.

Вычисления по Крайзелю и Трулстра

Тем самым программы для работы с непрерывными объектами являются обрывками алгоритмов, где вход и вывод оборваны в некотором, порою достаточно произвольном, месте.

В дискретной математике оказалось полезным понятие доказательного программирования, стандартной реализацией которого стала система AGDA. В ней исключительно богатые библиотеки работы с алгебраическими и комбинаторными алгоритмами, высокоразвитая система функционального программирования, но почти нет пакетов для работы с действительными числами. Причины этого показала теорема.

Кошмар равенства

В AGDA принимается, что значения можно проверять на равенство, но равенство действительных чисел вычислительного смысла не имеет, оно требует проверки бесконечной информации. Практики также неоднократно предупреждали о некорректности использования равенства в типе действительных чисел. Этот вариант неконструктивности теоретически неизлечим.

Практически же есть возможность в некоторых случаях его преодолевать.

1. Заменить равенство приближённым равенством, возможно несколько исправив формулировку задачи. Например, классическая задача нахождения нуля функции, меняющей знак на отрезке, конструктивно некорректна. Её нужно заменить на нахождение точки с малым значением функции.
2. Сравниваемые значения задаются последовательностью, члены которой различаются больше, чем на точность представления чисел. В этом случае целесообразно определить новый класс значений последовательности, позволяющий новые операции и переопределяющий практически все старые как дающие результат в стандартном классе.

Вывод, что действительные числа должны быть не исходным типом, а классом, важен. Поскольку любое конкретное представление является обрывком чисел, логически корректная программа должна быть шаблоном, куда подставляются конкретные представления чисел и операций.

1. В этом случае равенство замещается совпадением классов, то есть единым источником копирования, что корректно. Но стоит помнить: тогда не влечёт , а лишь . Все операции неточные и часто недетерминированные.

Недетерминированность

В конструктивизме нет трихотомии, она заменяется сравнением с точностью до некоторого :

Самой точной конструктивизацией оператора

является недетерминированный условный оператор Дейкстры:

либо:

В случае интервальных либо других избыточных представлений чисел недетерминированность реализуется как в теории: разные представления числа дают разные результаты.

Педагогическая проблема

Корректному программированию численных задач мешает глобальная педагогическая ошибка. От школы вплоть до серьёзных книг утверждают, что рациональные числа — подмножество действительных. Но в таком случае избыточная информация, унаследованная ими, забивает релевантную и возникают все недостатки непрерывности. Целые числа корректно представлять как частный случай действительных.

Основная проблема действий с рациональными числами — быстрый рост числителей и знаменателей. Возможное решение — разложить дробную часть в цепную дробь и отбросить последний член.

Следующие шаги по конструктивизации программы и её спецификации

В конструктивном представлении программ над топологическим пространством аргументы всегда задаются с некоторой точностью и результат тоже получается приближённым. Поэтому логичным шагом является спецификация критически важных значений их точностью.

Информация о функции.

По приближении к функции можно найти приближение к интегралу: границы прямоугольников позволяют вычислить нижние и верхние интегральные суммы. Также видна возможность получения информации о равномерной непрерывности функции.

Информация о функции с производной

Для функций с несколькими производными потребуется создавать собственную конечную информацию.

Большое конечное как непрерывное

Большой текст можно представить как бесконечную последовательность символов, большую базу данных — как бэровское пространство. Здесь естественно строить функции, пытающиеся выдать результат с требуемой точностью по части большой информации и запрашивающие уточнения.

Заключение

Ближайшая задача для свободного софта — накопить примеры логически корректных непрерывных программ и выработать рекомендации по технике их спецификации. Здесь поможет опыт рецензирования кода сообществом и инструменты, в частности, bugzilla.