Элементы Элементы большой науки

Поставить закладку

Напишите нам

Карта сайта

Содержание
Энциклопедия
Новости науки
LHC
Картинка дня
Библиотека
Методология науки
Избранное
Публичные лекции
Лекции для школьников
Библиотека «Династии»
Интервью
Опубликовано полностью
В популярных журналах
Из Книжного клуба
Статьи наших друзей
Статьи лауреатов «Династии»
Выставка
Происхождение жизни
Видеотека
Книжный клуб
Задачи
Масштабы: времена
Детские вопросы
Плакаты
Научный календарь
Наука и право
ЖОБ
Наука в Рунете

Поиск

Подпишитесь на «Элементы»



ВКонтакте
в Твиттере
в Фейсбуке
на Youtube
в Instagram



Новости науки

 
21.02
В пении флейтовых птиц обнаружены музыкальные принципы

20.02
Экстракт из старых сородичей ускоряет старение

16.02
Открыт бензольный дикатион — пирамида с шестикоординационным углеродом

15.02
Детектор ATLAS увидел рассеяние света на свете

14.02
Кембрийское ископаемое Saccorhytus поместили в основание эволюционной линии вторичноротых






Главная / Библиотека / Избранное версия для печати

Брайан Дэвис (Brian Davies),
профессор математики Лондонского Кингс Колледжа

Формальная проверка доказательств

Кому доводилось писать компьютерные программы, пусть даже самые простые и короткие, тот прекрасно знает, что они, в отличие от математиков, не прощают ошибок. Малейшая ошибка в синтаксисе будет замечена компилятором, и выполнение такой программы будет тут же остановлено. Использование одного и того же имени для двух разных переменных компилятор пропустит, но такую ошибку трудно не заметить, поскольку на выходе программы скорее всего окажется полная ерунда. Математические ошибки часто выявляются путем прогона программы для несложной задачи аналогичного типа, решение которой заведомо известно. Варьирование входных параметров задачи при этом позволяет удостовериться, что модель ведет себя предсказуемо. Возможные ошибки и погрешности в утилитах, входящих в стандартные пакеты программного обеспечения, выявить гораздо сложнее в силу их незначительности и редкости проявления. Тем не менее программа длиной всего лишь в несколько сот строк способна невероятно облегчить жизнь математикам, и практика показывает, что отладка программы позволяет в конце концов добиться от нее правильного поведения. Реальные проблемы возникают при использовании по-настоящему длинных и сложных программ — как раз недавно администрация правительства Великобритании была почти неделю парализована из-за того, что на компьютеры всех ее подразделений было установлено некорректное обновление программного обеспечения.

Формальная проверка корректности работы программного обеспечения — забота одновременно и специалистов в области прикладной математической логики, и представителей бизнеса. В частности, повышение надежности Windows XP было достигнуто благодаря мощному аппарату анализа корректности программного обеспечения, который основан на математических методах формальной проверки непротиворечивости математических же алгоритмов, лежащих в основе функционирования программ. Однако в некоторых отношениях проблемы кибернетики и математики лежат в принципиально различных плоскостях. Техническая документация некоторых языков программирования, таких как Java, может занимать сотни страниц — значительно больше, чем может потребоваться для формулировки самой заумной теоремы. Иногда трудно даже сказать, «своеобразное» поведение программного обеспечения — это ошибка или особенность программы. Зависания (часто вследствие переполнения буфера) — это, несомненно, недоработки программистов; сложнее сказать что-либо определенное, когда LATEX, например, отказывается делать по запросу пользователя что-то такое, о чем разработчикам не пришло в голову, что такая функция вообще может кому-нибудь понадобиться. Вообще, неадекватные технические задания на разработку крупных программных пакетов — гораздо более распространенная причина катастрофических сбоев с непредсказуемыми экономическими последствиями, нежели неправильное выполнение технических заданий программистами.

Доказанная ценность формальных доказательств корректности программного обеспечения подтолкнула некоторых кибернетиков к идее попытаться применить те же методы и в строгой математике, однако это поле деятельности на сегодняшний момент для сбора урожая явно не созрело. Из нижеследующих замечаний явственно видно, что в анализируемой мною области с реализацией предлагаемых методов формального доказательства корректности предвидятся большие трудности. В других областях, возможно, им и найдется достойное применение (например, в математической логике или алгебре), но об этом пусть судят специалисты, работающие в этих областях. Я же приведу лишь некоторые детали, чтобы дать читателям возможность почувствовать атмосферу происходящего, пусть эти детали и несущественны. Почти все доказательства теорем в математическом анализе опираются на внешние факты, которые обычно не объясняются, поскольку подразумеваются известными читателю. Статью можно начать заявлением, что она посвящена спектральному анализу лапласиана на ограниченной евклидовой области с граничными условиями Дирихле. По одной этой теме, наверное, имеются сотни монографий и тысячи публикаций, и автор берет на себя смелость утверждать, что с большей их частью он знаком. При этом автор будет ссылаться лишь на новые и малоизвестные работы, о которых читатель может быть не в курсе, подразумевая, что с «классикой жанра» человек, взявшийся за чтение такой статьи, скорее всего, знаком в силу полученного им образования.

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

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

Эксперты почти инстинктивно «понимают», когда возможно изменить классическую теорему так, чтобы она подошла к обсуждаемому контектсту; по-видимому, эта способность и отличает эксперта. Время от времени находятся математики, у которых хватило сил собраться и написать монографию с более или менее полным описанием какой-либо области. Это большое дело, поскольку коллегам впоследствии будет на что ссылаться. Однако иногда такая монография только искажает реальное состояние дел, поскольку автор вольно или невольно выстраивает ее в однородном контексте, и многие теоремы, приведенные в таких монографиях, верны и при более слабых условиях.


Комментарии (31)


 


при поддержке фонда Дмитрия Зимина - Династия