Программирование: теория типов
-
Скопировать в буфер библиографическое описание
Кудрявцева, И. А. Программирование: теория типов : учебное пособие для вузов / И. А. Кудрявцева, М. В. Швецкий. — 2-е изд., перераб. и доп. — Москва : Издательство Юрайт, 2022. — 652 с. — (Высшее образование). — ISBN 978-5-534-11088-3. — Текст : электронный // Образовательная платформа Юрайт [сайт]. — URL: https://urait.ru/bcode/444496 (дата обращения: 06.07.2022).
- Добавить в избранное
2-е изд., пер. и доп. Учебное пособие для вузов
- Нравится
- Посмотреть кому понравилось
- Поделиться
Страниц
652
Обложка
Мягкая
Гриф
Гриф УМО ВО
ISBN
978-5-534-11088-3
Библиографическое описание
Кудрявцева, И. А. Программирование: теория типов : учебное пособие для вузов / И. А. Кудрявцева, М. В. Швецкий. — 2-е изд., перераб. и доп. — Москва : Издательство Юрайт, 2022. — 652 с. — (Высшее образование). — ISBN 978-5-534-11088-3. — Текст : электронный // Образовательная платформа Юрайт [сайт]. — URL: https://urait.ru/bcode/444496 (дата обращения: 06.07.2022).
Серия
Тематика/подтематика
Учебное пособие представляет собой систему упражнений и лабораторных работ по курсу «Теоретические основы программирования», содержащих теоретические сведения по элементам теории типов, теории категорий и интуиционистской логике. Особое внимание уделено методам решения основных задач теории типов (TCP, TSP, TIP). Соответствует актуальным требованиям федерального государственного образовательного стандарта высшего образования. Пособие предназначено для преподавателей, аспирантов и студентов факультетов институтов компьютерных наук и информационных технологий.
- Введение
- Часть 1. ТИПИЗИРОВАННОЕ ?-ИСЧИСЛЕНИЕ
- Часть 2. АЛГОРИТМЫ УНИФИКАЦИИ
-
Часть 3. МОНОМОРФНЫЕ ТИПЫ (СИСТЕМА ? >)
-
Упражнение 4. Мономорфные типы: система ? > в стиле А. Чёрча
-
Теоретические сведения
- Грамматический разбор. Абстрактные синтаксические деревья
- Аннотированные абстрактные синтаксические деревья
- Понятие «тип данных» (повторение)
- Понятие «система типов» (в программировании)
- Семейства систем типов типизированного ?-исчисления
- Система типов ? > в стиле Чёрча
- Основные задачи в системе ? >
- Свойства системы ? > в стиле Чёрча
- Биографические сведения
- Примеры решения некоторых типов упражнений
- Упражнения для самостоятельного решения
-
Теоретические сведения
- Упражнение 5. Мономорфные типы: система ? > в стиле X. Карри
- Упражнение 6. Мономорфные типы: изоморфизм Карри — Говарда, свойства системы ? >
- Упражнение 7. Элементы теории типов ? > (для первокурсников)
- Упражнение 8. Мономорфные типы: алгоритм Хиндли — Милнера в системе ? > в стиле X. Карри
-
Упражнение 9. Проверка и синтез типа для функций в бесточечной форме записи
-
Теоретические сведения
- Бесточечный стиль программирования
- Коммутативные диаграммы функций в бесточечной форме записи
- Технология построения коммутативных диаграмм для функций в бесточечной форме записи
- Образцы диаграмм последовательностей сечений композиции функций
- Метод коммутативных диаграмм для решения задач типизированного ?-исчисления
- Примеры решения некоторых типов упражнений
- Демонстрационные примеры
- Задачи для самостоятельного решения
-
Теоретические сведения
- Упражнение 10. Расширения системы ? >: рекурсивные типы (система ? ), типы-пересечения (система ??)
- Лабораторная работа 11. Программная модель вывода типов (в системе ? >)
-
Упражнение 4. Мономорфные типы: система ? > в стиле А. Чёрча
-
Часть 4. ПОЛИМОРФНЫЕ ТИПЫ (СИСТЕМА ?2)
- Упражнение 12. Полиморфные типы: система ?2 в стиле X. Карри
- Упражнение 13. Полиморфные типы: решение задачи TSP для рекурсивных типов
-
Упражнение 14. Полиморфные типы: система ?2 в стиле А. Чёрча
-
Теоретические сведения
- Вспомогательные сведения
- Правила типизации в системе ?2 в стиле Чёрча
- Типизация самоприменения
- Связь между системой ?2 в стиле Карри и системой ?2 в стиле Чёрча
- Правила вывода для решения задачи TIP для системы ?2 в стиле Чёрча
- Разрешимость основных задач в системе ?2 в стиле Чёрча
- Свойства системы ?2 в стиле Чёрча
- Примеры решения некоторых типов упражнений
- Упражнения для самостоятельного решения
-
Теоретические сведения
- Упражнение 15. Система ?2 в стиле А. Чёрча: логические связки и квантор ?, логические операции, упорядоченные пары, нумералы, списки
- Упражнение 16. Система ?2 в стиле А. Чёрча: метод синтаксически ориентированного конструирования
-
Часть 5. ?-КУБ БАРЕНДРЕГТА
-
Упражнение 17. Операторы на типах. Кайнды конструкторов типов
-
Теоретические сведения
- Предварительные сведения
- Алгебраический тип данных в языке Haskell (повторение)
- Операторы на типах. Кайнды
- Операторы высших порядков на типах
- Система кайндов ?kind для операторов на типах
- Операторы на типах и кайнды в языке Haskell
- Построение кайнда конструктора типов (решение задачи TSP)
- Построение конструктора типов по кайнду (решение задачи TIP)
- Поддержка явных аннотаций кайндов
- Представление об обобщённых алгебраических типах данных (GADT)
- Примеры решения некоторых типов упражнений
- Упражнения для самостоятельного решения
-
Теоретические сведения
- Упражнение 18. Система типов ?? с операторами на типах
- Упражнение 19. Система типов ?P с зависимыми типами
- Упражнение 20. ?-куб Барендрегта
- Упражнение 21. Логические системы ?-куба. Прямое погружение логических систем в ?-куб
-
Упражнение 17. Операторы на типах. Кайнды конструкторов типов
-
Часть 6. ИНТУИЦИОНИСТСКИЕ ЛОГИЧЕСКИЕ ИСЧИСЛЕНИЯ
- Упражнение 1L. Интуиционистские пропозициональные логики
- Упражнение 2L. Интуиционистские пропозициональные логики: минимальное позитивное исчисление Prop
- Упражнение 3L. Интуиционистские пропозициональные логики: секвенциальное исчисление Н. Н. Воробьёва — Дж. Худельмайера без правила сокращения
- Упражнение 4L. Интуиционистские пропозициональные логики: логика второго порядка Рrор2
-
Упражнение 5L. Интуиционистская предикатная логика: минимальная логика Pred
-
Теоретические сведения
- Гильбертовская формализация интуиционистской логики первого порядка
- Интуиционистское понимание кванторов
- Интуиционистское секвенциальное исчисление предикатов Н. Н. Воробьёва — Дж. Худельмайера
- Интуиционистская предикатная логика первого порядка Pred
- Редукции классических систем к интуиционистским системам
- Примеры решения некоторых типов упражнений
- Упражнения для самостоятельного решения
-
Теоретические сведения
- Литература
- Новые издания по дисциплине «Программирование» и смежным дисциплинам
- Приложение 1. Программа синтеза типа ?-терма в системе ? > по двухэтапному алгоритму Хиндли — Милн
- Приложение 2. Транслятор математической формы записи ?-терма в системе ?-> в запись с конструктора
- Приложение 3. Программа синтеза типа ?-терма и кайнда типа в системах ?-куба Барендрегта
Высшее образование
-
Программирование: комбинаторная логика
2-е изд., пер. и доп. Учебное пособие для вузов -
Программирование: математическая логика
2-е изд., пер. и доп. Учебное пособие для вузов