Виталий Николаевич Брагилевский
Соответствие Карри–Ховарда:
от математической логики к программированию
В. Н. Брагилевский планирует провести 4 занятия.
Доступны 4 видеозаписи курса.
В программировании есть область, тесно связанная с математической логикой и другими разделами математики, — это верификация программного обеспечения, то есть проверка корректности программы относительно некоторой формальной спецификации. В наиболее жёстком режиме верификация превращается в доказательство теорем о правильности результатов работы программ. В этом курсе мы посмотрим на те математические основания, которые делают возможной именно такую верификацию.
Курс начнётся с элементарного введения в интуиционистскую логику и теорию доказательств, в рамках которого мы рассмотрим основные логические связки и правила вывода, а также построение с их помощью деревьев вывода, то есть собственно доказательств. После этого мы перейдём к изучению лямбда-исчисления как модели вычислений (эквивалентной, как известно, машине Тьюринга): мы определим множество лямбда-термов, обсудим понятия подстановки, альфа-эквивалентности и бета-редукции, после чего построим на этой базе простейший язык программирования.
Следующий шаг будет состоять в добавлении к лямбда-исчислению системы типов — так мы получим сначала простое типизированное лямбда-исчисление, а затем и некоторые наиболее важные его расширения. Лямбда-исчисление с типами оказывается удивительным образом связано с теорией доказательств: существует прямая связь между высказываниями и типами, а также между доказательствами и термами (программами) — мы увидим, что «доказывать теорему» означает в точности то же самое, что и «писать программу». Эту связь называют соответствием или изоморфизмом Карри–Ховарда, именно она делает возможными разработку и использование систем автоматического и интерактивного доказательства теорем. Наш курс завершится обзором и небольшой демонстрацией возможностей одной из таких систем, которая называется Coq: с её помощью мы формально докажем одну из математических теорем и построим доказуемо корректную реализацию одного из алгоритмов.
Этот курс не требует предварительных знаний вне стандартной школьной программы по математике и информатике, все используемые в нём понятия будут введены непосредственно по ходу. Курс будет сопровождаться упражнениями.
Материалы
Organization Committee e-mail:
dubna@mccme.ru