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