|
Л. Д. Беклемишев, С. Л. Кузнецов. Вычислительная теория доказательств и лямбда-исчисление
30 сентября 2019 – 12 мая 2020 г., МИАН, комн. 530 (ул. Губкина, 8), г. Москва
C 23.03 в связи с эпидемической обстановкой курс переходит в удаленный режим. Лекции будут продолжать записываться без слушателей и выкладываться на этом сайте и в youtube в еженедельном режиме. Лекторы постараются подготовить записки по материалам лекций и/или снабдить видеозаписи подробными ссылками на литературу. Следите за объявлениями здесь.
Курс планируется как годовой. В первой части (осенний семестр) планируется
изложить основы лямбда-исчисления и его связь с системой естественного
вывода для интуиционистской логики (соответствие Карри‒Говарда).
Примерный список тем первого семестра:
- Бета-редукции. Свойство Чёрча‒Россера. Стратегии редукций. Слабая и
сильная нормализуемость для типизованного лямбда-исчисления.
- Теорема о неподвижной точке для бестипового лямбда-исчисления.
Кодирование рекурсивных функций.
- Алгоритм выведения типов для простого типового лямбда-исчисления.
- Эта-редукция. Теоретико-множественная интерпретация лямбдаисчисления, теорема о полноте.
- Интуиционистская логика высказываний. Семантика Крипке, теорема о
полноте. Соответствие Карри‒Говарда.
- Исчисление гильбертовского типа и комбинаторная логика.
- Интерпретация типизованного лямбда-исчисления на декартово
замкнутых категориях.
Во второй части курса планируется рассказать о семантике Скотта для бестипового лямбда-исчисления, гёделевской системе T и и её связи с классами доказуемо тотальных вычислимых функций в арифметике 1-го порядка. Примерный список тем
второго семестра:
- Семантика бестипового лямбда-исчисления, модели Скотта и Плоткина, полные частично упорядоченные множества.
- Интуиционистская и классическая арифметика. Негативный перевод. Перевод Фридмана‒Драгалина. Доказуемо тотальные вычислимые функции.
- Функционалы конечных типов. Гёделевская система T. Функциональная интерпретация.
Характеризация доказуемо тотальных вычислимых функций в арифметике PA как функций,
представимых в системе T.
 Регистрационная
форма участников
Объявления
21.03. В следующей части курса будет рассказано об интуиционистской арифметике, функционалах конечных типов и гёделевской системе T. Очередная лекция будет записана 23.03 и должна появиться в сети на следующий день. Тема лекции: интуиционистская логика предикатов и интуиционистская арифметика. Лектор: Л.Д. Беклемишев.
Прошедшие лекции
26.03. Лекция 16: Негативный перевод (Гёделя--Генцена) классической логики в интуиционистскую.
04.04 Лекция 17: Примитивно рекурсивная арифметика.
11.04. Лекция 18: Интуиционистская арифметика.
Аннотация: теория НА, принцип наименьшего числа влечет закон исключенного третьего, негативная интерпретация PA в HA, перевод Фридмана-Драгалина, замкнутость HA относительно рекурсивного правила Маркова и правила независимости посылок, консервативность PA над HA для $\forall\exists$-формул, штрих Акцеля, дизъюнктивное и экзистенциальное свойства НА.
21.04 Лекция 19: Гёделевская система Т. Функциональная интерпретация интуиционистской арифметики в Т, часть 1.
Аннотация: Функционалы конечных типов. Язык системы Т. Рекурсор. Аксиоматика системы Т. D-перевод формул арифметики Гейтинга HA в T. Формулировка теоремы Гёделя о функциональной интерпретации. Начало её доказательства: эквивалентная аксиоматизация исчисления высказываний, интерпретация правил modus ponens и силлогизма, аксиома $\phi\to\phi\land\phi$.
28.04 Лекция 20: Функциональная интерпретация интуиционистской арифметики в Т, часть 2.
Аннотация: Завершение доаказательства теоремы Гёделя об интерпретации арифметики HA в системе T. Правило индукции. Следствия об относительной непротиворечивости, консервативности и представимости доказуемо рекурсивных функций PA в системе T.
12.05 Лекция 21. Применения функциональной интерпретации. Интерпретация отсутствием контрпримера. Модели системы Т.
Программа осеннего семестра
Программа весеннего семестра
Финансовая поддержка. Курс проводится при финансовой поддержке
Минобрнауки России (грант на создание и развитие МЦМУ МИАН, соглашение № 075-15-2019-1614).
 Лекторы
Беклемишев Лев Дмитриевич
Кузнецов Степан Львович
Организации
Математический институт им. В.А. Стеклова Российской академии наук, г. Москва
Математический центр мирового уровня «Математический институт им. В.А. Стеклова Российской академии наук» (МЦМУ МИАН) |
|
| Л. Д. Беклемишев, С. Л. Кузнецов. Вычислительная теория доказательств и лямбда-исчисление, г. Москва, 30 сентября 2019 – 12 мая 2020 г. |
|
|
12 мая 2020 г. (вт) |
 |
| 1. |
Лекция 21. Применения функциональной интерпретации. Интерпретация отсутствием контрпримера. Модели системы Т
Л. Д. Беклемишев
12 мая 2020 г. 16:30, г. Москва, online
|
|
|
|
|
|
28 апреля 2020 г. (вт) |
|
| 2. |
Лекция 20. Гёделевская система Т. Интерпретация формальной арифметики в Т (продолжение)
Л. Д. Беклемишев
28 апреля 2020 г. 16:30, г. Москва, МИАН, комн. 530 (ул. Губкина, 8)
|
|
|
|
|
|
|
21 апреля 2020 г. (вт) |
|
| 3. |
Лекция 19. Гёделевская система $Т$. Функциональная интерпретация интуиционистской арифметики в $Т$
Л. Д. Беклемишев
21 апреля 2020 г., г. Москва, online
|
|
|
|
|
|
|
14 апреля 2020 г. (вт) |
|
| 4. |
Лекция 18. Интуиционистская арифметика
Л. Д. Беклемишев
14 апреля 2020 г. 16:30, г. Москва, online
|
|
|
|
|
|
|
7 апреля 2020 г. (вт) |
|
| 5. |
Лекция 17. Примитивно рекурсивная арифметика
Л. Д. Беклемишев
7 апреля 2020 г., г. Москва, online
|
|
|
|
|
|
|
26 марта 2020 г. (чт) |
|
| 6. |
Лекция 16. Негативная интерпретация классической логики в интуиционистской
Л. Д. Беклемишев
26 марта 2020 г. 16:00, г. Москва, МИАН, комн. 530 (ул. Губкина, 8)
|
|
|
|
|
|
|
23 марта 2020 г. (пн) |
|
| 7. |
Лекция 15. Интуиционистское исчисление предикатов. Гильбертовский и генценовский формат. Теорема об устранении сечения. Дизъюнктивное и экзистенциальное свойства интуиционистской логики.
Л. Д. Беклемишев
23 марта 2020 г. 16:30, г. Москва, МИАН, комн. 530 (ул. Губкина, 8)
|
|
|
|
|
|
|
16 марта 2020 г. (пн) |
|
| 8. |
Лекция 14. Полные частично упорядоченные множества. Модель Скотта $D_\infty$.
С. Л. Кузнецов
16 марта 2020 г. 16:30, г. Москва, МИАН, комн. 530 (ул. Губкина, 8)
|
|
|
|
|
|
|
2 марта 2020 г. (пн) |
|
| 9. |
Лекция 13. Слабо экстенсиональные лямбда-алгебры. Модель Плоткина $\mathcal{P}\omega$.
Л. Д. Беклемишев
2 марта 2020 г. 16:30, г. Москва, МИАН, комн. 530 (ул. Губкина, 8)
|
|
|
|
|
|
|
17 февраля 2020 г. (пн) |
|
| 10. |
Лекция 12. Комбинаторные алгебры, лямбда-алгебры.
Л. Д. Беклемишев
17 февраля 2020 г. 16:30, г. Москва, МИАН, комн. 530 (ул. Губкина, 8)
|
|
|
|
|
|
|
10 февраля 2020 г. (пн) |
|
| 11. |
Лекция 11. Модели лямбда-исчисления
Л. Д. Беклемишев, С. Л. Кузнецов
10 февраля 2020 г. 16:30, г. Москва, МИАН, комн. 530 (ул. Губкина, 8)
|
|
|
|
|
|
|
9 декабря 2019 г. (пн) |
|
| 12. |
Лекция 10. Комбинаторная логика
Л. Д. Беклемишев
9 декабря 2019 г. 16:30, г. Москва, МИАН, комн. 530 (ул. Губкина, 8)
|
|
|
|
|
|
|
2 декабря 2019 г. (пн) |
|
| 13. |
Лекция 9. Полнота типового лямбда-исчисления относительно теоретико-множественной семантики
С. Л. Кузнецов
2 декабря 2019 г. 16:30, г. Москва, МИАН, комн. 530 (ул. Губкина, 8)
|
|
|
|
|
|
|
25 ноября 2019 г. (пн) |
|
| 14. |
Лекция 8. Теорема о сильной нормализуемости для типового лямбда-исчисления (окончание). Теоретико-множественная семантика типового лямбда-исчисления
С. Л. Кузнецов
25 ноября 2019 г. 16:30, г. Москва, МИАН, комн. 530 (ул. Губкина, 8)
|
|
|
|
|
|
|
18 ноября 2019 г. (пн) |
|
| 15. |
Лекция 7. Алгоритм выведения наиболее общего типа в системе Карри (окончание). Теорема о сильной нормализуемости для типового лямбда-исчисления
С. Л. Кузнецов
18 ноября 2019 г. 16:30, г. Москва, МИАН, комн. 530 (ул. Губкина, 8)
|
|
|
|
|
|
|
11 ноября 2019 г. (пн) |
|
| 16. |
Лекция 6. Алгоритм выведения наиболее общего типа в системе Карри
С. Л. Кузнецов
11 ноября 2019 г. 16:30, г. Москва, МИАН, комн. 530 (ул. Губкина, 8)
|
|
|
|
|
|
|
28 октября 2019 г. (пн) |
|
| 17. |
Лекция 5. Сохранение типа при бета-редукции. Интуиционистская логика высказываний, соответствие Карри - Говарда
С. Л. Кузнецов
28 октября 2019 г. 16:30, г. Москва, МИАН, комн. 530 (ул. Губкина, 8)
|
|
|
|
|
|
|
21 октября 2019 г. (пн) |
|
| 18. |
Лекция 4. Свойство Чёрча - Россера (окончание). Типовое лямбда исчисление: типизации по Чёрчу и по Карри
С. Л. Кузнецов
21 октября 2019 г. 16:30, г. Москва, МИАН, комн. 530 (ул. Губкина, 8)
|
|
|
|
|
|
|
14 октября 2019 г. (пн) |
|
| 19. |
Лекция 3. Представимость вычислимых функций в бестиповом лямбда-исчислении. Свойство Чёрча - Россера
С. Л. Кузнецов
14 октября 2019 г., г. Москва, МИАН, комн. 530 (ул. Губкина, 8)
|
|
|
|
|
|
|
7 октября 2019 г. (пн) |
|
| 20. |
Лекция 2. Теорема о неподвижной точке. Представимость примитивно-рекурсивных функций в бестиповом лямбда-исчислении
С. Л. Кузнецов
7 октября 2019 г., г. Москва, МИАН, комн. 530 (ул. Губкина, 8)
|
|
|
|
|
|
|
30 сентября 2019 г. (пн) |
|
| 21. |
Лекция 1.Введение. Бестиповое лямбда-исчисление. Представление натуральных чисел в бестиповом лямбда-исчислении
Л. Д. Беклемишев, С. Л. Кузнецов
30 сентября 2019 г., г. Москва, МИАН, комн. 530 (ул. Губкина, 8)
|
|
|
|
|
|
|
Обратная связь: