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

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