Степан Львович Кузнецов

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

Пререквизиты

От слушателей курса не требуется специальных предварительных знаний, однако полезной окажется общая программистская интуиция.

План

1. Бестиповое лямбда-исчисление. Свойство Чёрча—Россера, стратегии вычислений. Нумералы Чёрча, представимость примитивной рекурсии. Комбинатор неподвижной точки, представимость произвольных вычислимых функций.
2. Типы в основаниях математики и в языках программирования. Простая система типов для лямбда-исчисления. Алгоритм выведения типов (неявная типизация).
3. Связь типизуемости и нормализуемости (завершения вычисления). Соответствие Карри—Говарда: типы как математические утверждения, лямбда-термы как доказательства.
4. Система $F$ (полиморфная система типов) для лямбда-исчисления. Представимость примитивной рекурсии и функции Аккермана в системе $F$.