#матлог #учёба #спецкурс

С.Л. Кузнецов, С.О. Сперанский в Математическом институте им. В.А. Стеклова РАН (Москва, ул. Губкина, 8) прочитают спецкурс "Теория вычислимости и лямбда-исчисление".

Первая лекция: 11 февраля

Место проведения: МИАН, ком. 303

Время проведения: среда 18:00

Страница спецкурса: https://www.mathnet.ru/conf2697

‼Всем участникам (в т.ч. онлайн-участникам) просьба зарегистрироваться на странице курса по ссылке выше. Будет возможность удалённого подключения через Контур Толк (ссылку получат зарегистрированные слушатели).

Аннотация.
Формализация понятия вычислимости, построение универсальных вычислимых функций (прообразов операционных систем) и появление естественных примеров алгоритмически неразрешимых проблем — одни из ярчайших событий в истории современной математики и информатики, связанные с пионерскими работами Курта Гёделя, Алонзо Чёрча, Алана Тьюринга и Стивена Клини. Курс будет посвящён стоящему за этими событиями математическому аппарату и его развитию. В частности, мы обсудим знаменитую «проблему остановки», весьма полезную теорему Клини о неподвижной точке, вычислимость с оракулом (предложенную Тьюрингом) и арифметическую иерархию (тесно связанную с формальной арифметикой), а также то, как классифицировать алгоритмические проблемы по степени неразрешимости.

В одной из исторически первых формализаций понятия вычислимости использовалось так называемое лямбда-исчисление (предложенное Чёрчем). Лямбда-исчисление лежит в основе парадигмы функционального программирования, в которой программа представляется в виде сложного выражения (терма), а процесс вычисления заключается в применении упрощающих преобразований (редукций). В курсе будет представлено лямбда-исчисление в его бестиповом и типизованном вариантах. В первом реализуются все вычислимые функции, а во втором — только некоторый подкласс всюду определённых вычислимых функций. В конце курса также будет рассказано о связи лямбда-исчисления с доказуемостью в интуиционистской логике (соответствие Карри–Говарда) и его приложениях в системах автоматизированного поиска доказательств.

➰ ВК