Вопросы к зачёту по курсу «Математические модели вычислений», 2022 год, осенний семестр

1. Методы верификации программ в целом. Рецензирование. Тестирование.
2. Методы верификации программ в целом. Статический анализ и формальная верификация.
3. Фундаментальные модели вычислений. Конечные автоматы, магазинные автоматы. Леммы о накачке (формулировки).
4. Формальные языки и их связь с вычислениями. Иерархия Хомского. Леммы о накачке (формулировки).
5. Фундаментальные модели вычислений. Понятие эквивалентности фундаментальных моделей вычислений. Машина Тьюринга. Машины с регистрами.
6. Фундаментальные модели вычислений. Понятие эквивалентности фундаментальных моделей вычислений. Частично-рекурсивные функции (μ-рекурсивные функции Клини).
7. Фундаментальные модели вычислений. Понятие эквивалентности фундаментальных моделей вычислений. Нормальные алгорифмы Маркова.
8. Фундаментальные модели вычислений. Понятие эквивалентности фундаментальных моделей вычислений. λ-исчисление.
9. Фундаментальные модели вычислений. Понятие эквивалентности фундаментальных моделей вычислений. Клеточные автоматы, комбинаторная логика.
10. Понятие разрешимости. Теорема Райса о неразрешимости нетривиальных свойств. Схема доказательства.
11. Понятие разрешимости. Проблема останова. Схема доказательства неразрешимости проблемы останова.
12. Определение формальной системы. Пример формальной системы (исчисление предикатов или исчисление высказываний). Полнота, непротиворечивость и разрешимость формальных систем.
13. Полнота, непротиворечивость и разрешимость формальных систем. Первая и вторая теоремы Гёделя о неполноте (формулировки, «физический смысл»). Схема доказательства первой теоремы Гёделя о неполноте.
14. Метод Model checking. Основные принципы.
15. Темпоральные логики LTL (Linear Time Logic), CTL (Computational Tree Logic).
16. Метод SLAM (Software Model Checking via Counterexample Guided Abstraction Refinement). Основные принципы, схема метода.
17. Нетипизированное λ-исчисление и λ-исчисление с простыми типами. Пример нетипизированного терма, редукция которого не завершается. Парадокс Карри.
18. Определения методом естественной дедукции. Правила вывода λ-исчисления с простыми типами в терминах естественной дедукции. Пустой тип, тип из одного элемента и тип из двух элементов, определённые методом естественной дедукции.
19. Определения методом естественной дедукции. Типы суммы и произведения, определённые методом естественной дедукции.
20. Свойства систем редукции: конфлюэнтность, нормализация, сильная нормализация. Соответствие Карри-Говарда для просто типизированного λ-исчисления.
21. Эквивалентность термов. α, β и η-эквивалентность.
22. Постановки задач анализа термов в системах типов. Метапеременные и унификация.
23. λ-куб Барендрегта. Расширения типизированного λ-исчисления. Полиморфное λ-исчисление (System F).
24. λ-куб Барендрегта. Расширения типизированного λ-исчисления. Полиморфное λ-исчисление с конструкторами типов (System F_omega).
25. Кодирование типов данных по термам удаления в полиморфном λ-исчислении.
26. λ-куб Барендрегта. Расширения типизированного λ-исчисления. λ-исчисление с (простыми) зависимыми типами.
27. Исчисление конструкций. Зависимые произведения. Соответствие Карри-Говарда для зависимых произведений.
28. Расширенное исчисление конструкций. Зависимые суммы. Соответствие Карри-Говарда для зависимых сумм.
29. Универсумы и уровни универсумов.
30. Индуктивные типы. Примеры. Зависимое удаление индуктивных типов. Определение через набор конструкторов.
31. Операторные схемы программ. Схемы Янова. Эквивалентность схем Янова (определения и формулировки теорем).
32. Типы идентичности (равенства). Понятие о гомотопической теории типов. Функциональная экстензиональность. Аксиома унивалентности.
33. Самоинтерпретация системы F_omega. Диагонализация универсального интерпретатора для функций на натуральных числах. Отличия для типизированного случая. Поверхностная (shallow) схема самоинтерпретации.

Литература

Дополнительные источники, в том числе ссылки на электронные ресурсы, приведены в презентациях.

1. Б. Пирс. Типы в языках программирования. 2010
2. Henk Barendregt, Wil Dekkers, Richard Statman. Lambda Calculus With Types. Cambridge University Press, 2010.
3. М. Кривчиков. Формальные модели и верификация свойств программ с использованием промежуточного представления. Глава 1, раздел 2.1, подраздел 3.2.6.
4. Васенин В. А., Кривчиков М. А. Формальные модели программ и языков программирования. Часть 1. Библиографический обзор 1930—1989 гг // Программная инженерия. — 2015. — № 5. — С. 10–19.
5. Васенин В. А., Кривчиков М. А. Формальные модели программ и языков программирования. Часть 2. Современное состояние исследований // Программная инженерия. — 2015. — № 6. — С. 24–33.
6. Пентус А. Е., Пентус М. Р. Теория формальных языков: Учебное пособие. — М.: Изд-во ЦПИ при механико-математическом ф-те МГУ, 2004. — 80 с.
7. Homotopy Type Theory: Univalent Foundations of Mathematics. — Princeton: Institute for Advanced Study, 2013. — 603 p. https://homotopytypetheory.org/book/
8. F. William Lawvere, Stephen H. Schanuel. Conceptual Mathematics: A First Introduction to Categories. Cambridge University Press — 1997. — 374 p.
9. А. П. Ершов. Введение в теоретическое программирование: беседы о методе. М.: Наука, 1977. 288 С.
10. А. А. Марков, Н. М. Нагорный. Теория алгорифмов. М.: Наука, 1984. 432 С.