RUS  ENG ЖУРНАЛЫ   ПЕРСОНАЛИИ   ОРГАНИЗАЦИИ   КОНФЕРЕНЦИИ   СЕМИНАРЫ   ВИДЕОТЕКА   ПАКЕТ AMSBIB


Л. Д. Беклемишев, С. Л. Кузнецов. Вычислительная теория доказательств и лямбда-исчисление
30 сентября 2019 – 25 мая 2020 г., МИАН, комн. 530 (ул. Губкина, 8), г. Москва

Курс планируется как годовой. В первой части (осенний семестр) планируется изложить основы лямбда-исчисления и его связь с системой естественного вывода для интуиционистской логики (соответствие Карри‒Говарда).
Примерный список тем первого семестра:

  1. Бета-редукции. Свойство Чёрча‒Россера. Стратегии редукций. Слабая и сильная нормализуемость для типизованного лямбда-исчисления.
  2. Теорема о неподвижной точке для бестипового лямбда-исчисления. Кодирование рекурсивных функций.
  3. Алгоритм выведения типов для простого типового лямбда-исчисления.
  4. Эта-редукция. Теоретико-множественная интерпретация лямбдаисчисления, теорема о полноте.
  5. Интуиционистская логика высказываний. Семантика Крипке, теорема о полноте. Соответствие Карри‒Говарда.
  6. Исчисление гильбертовского типа и комбинаторная логика.
  7. Интерпретация типизованного лямбда-исчисления на декартово замкнутых категориях.
  8. Семантики Скотта и Ершова для бестипового лямбда-исчисления.

Во второй части курса планируется рассказать о семантике Скотта для бестипового лямбда-исчисления, гёделевской системе T и и её связи с классами доказуемо тотальных вычислимых функций в арифметике 1-го порядка. Примерный список тем второго семестра:

  1. Семантика бестипового лямбда-исчисления, модели Скотта и Плоткина, полные частично упорядоченные множества.
  2. Интуиционистская и классическая арифметика. Гёделевский перевод. Перевод Фридмана‒Драгалина. Доказуемо тотальные вычислимые функции.
  3. Функционалы конечных типов. Гёделевская система T. Функциональная интерпретация. Характеризация доказуемо тотальных вычислимых функций в арифметике PA как функций, представимых в системе T.

Финансовая поддержка. Курс проводится при финансовой поддержке Минобрнауки России (грант на создание и развитие МЦМУ МИАН, соглашение № 075-15-2019-1614).

Регистрационная форма участников




Программа осеннего семестра

Программа весеннего семестра


RSS: Ближайшие семинары

Руководители семинара
Беклемишев Лев Дмитриевич
Кузнецов Степан Львович

Организации
Математический институт им. В.А. Стеклова Российской академии наук, г. Москва
Математический центр мирового уровня «Математический институт им. В.А. Стеклова Российской академии наук» (МЦМУ МИАН)


Л. Д. Беклемишев, С. Л. Кузнецов. Вычислительная теория доказательств и лямбда-исчисление, г. Москва, 30 сентября 2019 – 25 мая 2020 г.

17 февраля 2020 г. (пн)
1. Лекция 12. Комбинаторные алгебры, лямбда-алгебры, модель Плоткина $P \omega$
Л. Д. Беклемишев
17 февраля 2020 г. 16:30, г. Москва, МИАН, комн. 530 (ул. Губкина, 8)
  

10 февраля 2020 г. (пн)
2. Лекция 11. Модели лямбда-исчисления
Л. Д. Беклемишев, С. Л. Кузнецов
10 февраля 2020 г. 16:30, г. Москва, МИАН, комн. 530 (ул. Губкина, 8)
  

9 декабря 2019 г. (пн)
3. Лекция 10. Комбинаторная логика
Л. Д. Беклемишев
9 декабря 2019 г. 16:30, г. Москва, МИАН, комн. 530 (ул. Губкина, 8)
Л. Д. Беклемишев
  

2 декабря 2019 г. (пн)
4. Лекция 9. Полнота типового лямбда-исчисления относительно теоретико-множественной семантики
С. Л. Кузнецов
2 декабря 2019 г. 16:30, г. Москва, МИАН, комн. 530 (ул. Губкина, 8)
С. Л. Кузнецов
  

25 ноября 2019 г. (пн)
5. Лекция 8. Теорема о сильной нормализуемости для типового лямбда-исчисления (окончание). Теоретико-множественная семантика типового лямбда-исчисления
С. Л. Кузнецов
25 ноября 2019 г. 16:30, г. Москва, МИАН, комн. 530 (ул. Губкина, 8)
С. Л. Кузнецов
  

18 ноября 2019 г. (пн)
6. Лекция 7. Алгоритм выведения наиболее общего типа в системе Карри (окончание). Теорема о сильной нормализуемости для типового лямбда-исчисления
С. Л. Кузнецов
18 ноября 2019 г. 16:30, г. Москва, МИАН, комн. 530 (ул. Губкина, 8)
С. Л. Кузнецов
  

11 ноября 2019 г. (пн)
7. Лекция 6. Алгоритм выведения наиболее общего типа в системе Карри
С. Л. Кузнецов
11 ноября 2019 г. 16:30, г. Москва, МИАН, комн. 530 (ул. Губкина, 8)
С. Л. Кузнецов
  

28 октября 2019 г. (пн)
8. Лекция 5. Сохранение типа при бета-редукции. Интуиционистская логика высказываний, соответствие Карри - Говарда
С. Л. Кузнецов
28 октября 2019 г. 16:30, г. Москва, МИАН, комн. 530 (ул. Губкина, 8)
С. Л. Кузнецов
  

21 октября 2019 г. (пн)
9. Лекция 4. Свойство Чёрча - Россера (окончание). Типовое лямбда исчисление: типизации по Чёрчу и по Карри
С. Л. Кузнецов
21 октября 2019 г. 16:30, г. Москва, МИАН, комн. 530 (ул. Губкина, 8)
С. Л. Кузнецов
  

14 октября 2019 г. (пн)
10. Лекция 3. Представимость вычислимых функций в бестиповом лямбда-исчислении. Свойство Чёрча - Россера
С. Л. Кузнецов
14 октября 2019 г., г. Москва, МИАН, комн. 530 (ул. Губкина, 8)
С. Л. Кузнецов
  

7 октября 2019 г. (пн)
11. Лекция 2. Теорема о неподвижной точке. Представимость примитивно-рекурсивных функций в бестиповом лямбда-исчислении
С. Л. Кузнецов
7 октября 2019 г., г. Москва, МИАН, комн. 530 (ул. Губкина, 8)
С. Л. Кузнецов
  

30 сентября 2019 г. (пн)
12. Лекция 1.Введение. Бестиповое лямбда-исчисление. Представление натуральных чисел в бестиповом лямбда-исчислении
Л. Д. Беклемишев, С. Л. Кузнецов
30 сентября 2019 г., г. Москва, МИАН, комн. 530 (ул. Губкина, 8)
Л. Д. Беклемишев, С. Л. Кузнецов
  
 
Обратная связь:
 Пользовательское соглашение  Регистрация  Логотипы © Математический институт им. В. А. Стеклова РАН, 2020