С.Л. Кузнецов. Спецкурс «Лямбда-исчисление, или вычислительная теория доказательств»

Лекции и семинары Научно-образовательного центра Математического института им. В.А. Стеклова Российской академии наук. С.Л. Кузнецов. Спецкурс «Лямбда-исчисление, или вычислительная теория доказательств». Москва, МИАН, весна 2015 г. Все лекции спецкурса: http://www.mathnet.ru/conf664. 1. λ-термы. Бестиповое λ-исчисление. α-конверсия и β-редукция. 2. Граф редукций λ-терма. Свойство Чёрча–Россера. Нормальные формы. Единственность нормальной формы. Примеры λ-термов, не имеющих нормальной формы. 3. Теорема о неподвижной точки для бестипового λ-исчисления. Равномерная теорема о неподвижной точке (комбинатор неподвижной точки). 4. Кодирование натуральных чисел и представимость вычислимых функций в бестиповом λ-исчислении. Неразрешимость проблемы нормализуемости. 5. Типовое λ-исчисление (варианты с жесткой типизацией и с мягкой типизацией в стиле Карри и Чёрча). Слабая нормализуемость. 6. Теорема о сильной нормализуемости для типового λ-исчисления. 7. η-редукция. Теоретико-множественная интерпретация типового λ-исчисления с правилом η-редукции; теорема о полноте. 8. Введение в теорию категорий. Декартово замкнутые категории. Интерпретация типового λ-исчисления без правила η-редукции на декартово замкнутых категориях; теорема о полноте. 9. Интуиционистская логика высказываний. Неформальная семантика Брауэра–Гейтинга–Колмогорова (BHK). Семантика Крипке, теорема о полноте. Теорема Гливенко. 10. Система естественного вывода для импликативного фрагмента интуиционистской логики высказываний. Соответствие Карри–Говарда (формулы как типы, термы как доказательства). 11. Гильбертовское исчисление для интуиционистской логики высказываний и комбинаторная логика. Перевод из типового λ-исчисления в комбинаторную логику. 12. Генценовское (секвенциальное) исчисление для интуиционистской логики высказываний. Теорема об устранении сечения. 13. Интуиционистская логика первого порядка. Система естественного вывода и генценовское (секвенциальное) исчисление. 14. Введение в теорию типов. Зависимое произведение типов и соответствие (по Карри–Говарду) с интуиционистским квантором всеобщности. Исчисление индуктивных конструкций (CIC); система Coq для формализации математических доказательств на ЭВМ. 15. Применение λ-исчисления в языкознании: категориальные грамматики, семантика Монтегю.