Просьба ко всем участникам, в том числе смотрящим видеозаписи,
зарегистрироваться по этой ссылке.
Формализация понятия вычислимости, построение универсальных вычислимых функций (прообразов операционных систем) и появление естественных примеров алгоритмически неразрешимых проблем — одни из ярчайших событий в истории современной математики и информатики, связанные с пионерскими работами Курта Гёделя, Алонзо Чёрча, Алана Тьюринга и Стивена Клини. Курс будет посвящён стоящему за этими событиями математическому аппарату и его развитию. В частности, мы обсудим знаменитую «проблему остановки», весьма полезную теорему Клини о неподвижной точке, вычислимость с оракулом (предложенную Тьюрингом) и арифметическую иерархию (тесно связанную с формальной арифметикой), а также то, как классифицировать алгоритмические проблемы по степени неразрешимости.
В одной из исторически первых формализаций понятия вычислимости использовалось так называемое лямбда-исчисление (предложенное Чёрчем). Лямбда-исчисление лежит в основе парадигмы функционального программирования, в которой программа представляется в виде сложного выражения (терма), а процесс вычисления заключается в применении упрощающих преобразований (редукций). В курсе будет представлено лямбда-исчисление в его бестиповом и типизованном вариантах. В первом реализуются все вычислимые функции, а во втором — только некоторый подкласс всюду определённых вычислимых функций. В конце курса также будет рассказано о связи лямбда-исчисления с доказуемостью в интуиционистской логике (соответствие Карри–Говарда) и его приложениях в системах автоматизированного поиска доказательств.
Программа
- Формализация понятия (частичной) вычислимой функции: регистровые машины, рекурсивные схемы и т.д. Тезис Чёрча–Тьюринга.
- Разрешимые и полуразрешимые (вычислимо перечислимые) множества. Универсальные вычислимые функции. Проблемы самоприменимости и остановки.
- Сводимость между алгоритмическими проблемами. Вычислимая неотделимость. Полнота проблемы самоприменимости в классе всех полуразрешимых множеств. О связи с 10-й проблемой Гильберта.
- Теорема Клини о неподвижной точке (теорема о рекурсии) и её вариации. Эффективно неотделимые множества. Вычисления с оракулом и релятивизация. Операция скачка (по Тьюрингу).
- Арифметическая иерархия. Теорема о её строгости. Классификация алгоритмических проблем по степени неразрешимости.
- Бестиповое лямбда-исчисление. Бета-редукции, теорема Чёрча-Россера. Стратегии редукций. Теорема о нормальной стратегии.
- Комбинаторы неподвижной точки. Представимость вычислимых функций в бестиповом лямбда-исчислении.
- Типы в лямбда-исчислении: простое типизованное лямбда исчисление; лямбда-исчисление второго порядка и система $F$. Сильная нормализуемость термов, типизуемых в системе $F$.
- Представимость примитивно-рекурсивных функций и функции Аккермана в системе $F$.
- Лямбда-исчисление как основа систем автоматизированного поиска доказательств. Соответствие Карри-Говарда.
 RSS: Ближайшие семинары
 Лекторы
Кузнецов Степан Львович
Сперанский Станислав Олегович
Организации
Математический институт им. В.А. Стеклова Российской академии наук, г. Москва
Математический центр мирового уровня «Математический институт им. В.А. Стеклова Российской академии наук» (МЦМУ МИАН) |
