Видеотека
RUS  ENG    ЖУРНАЛЫ   ПЕРСОНАЛИИ   ОРГАНИЗАЦИИ   КОНФЕРЕНЦИИ   СЕМИНАРЫ   ВИДЕОТЕКА   ПАКЕТ AMSBIB  
Видеотека
Архив
Популярное видео

Поиск
RSS
Новые поступления






Летняя школа «Современная математика», посвященная памяти Виталия Арнольда, 2017
26 июля 2017 г. 09:30, г. Дубна, дом отдыха «Ратмино»
 


Соответствие Карри–Ховарда: от математической логики к программированию. Занятие 2

В. Н. Брагилевский
Видеозаписи:
MP4 625.1 Mb
MP4 2,749.6 Mb

В. Н. Брагилевский



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

Website: https://www.mccme.ru/dubna/2017/courses/bragilevsky.html
Цикл лекций
 
  Обратная связь:
 Пользовательское соглашение  Регистрация посетителей портала  Логотипы © Математический институт им. В. А. Стеклова РАН, 2024