УДК 004.42
ББК 32.973-018
Д58
Д58
Довек, Жиль.
Введение в теорию языков программирования / Ж. Довек, Ж.-Ж. Леви
; пер. с англ. В. Н. Брагилевского, А. М. Пеленицына. — 2-е изд., эл. —
1 файл pdf : 135 с. — Москва : ДМК Пресс, 2023. — Систем. требования:
Adobe Reader XI либо Adobe Digital Editions 4.5 ; экран 10". — Текст :
электронный.
ISBN 978-5-89818-582-4
Языки программирования от Фортрана и Кобола до Caml и Java играют ключевую
роль в управлении сложными компьютерными системами. Книга «Введение
в теорию языков программирования» представляет читателю средства, необходимые
для проектирования и реализации подобных языков. В ней предлагается единый
подход к различным формализмам для определения языков программирования —
операционной и денотационной семантике. Особое внимание при этом уделяется
способам задания отношений между тремя объектами: программой, входным значением
и результатом. Эти формализмы демонстрируются на примере таких типичных
элементов языков программирования, как функции, рекурсия, присваивание,
записи и объекты. При этом показывается, что теория языков программирования
состоит не в последовательном изучении самих языков один за другим, а
строится вокруг механизмов, входящих в различные языки. Изучение таких механизмов
в книге приводит к разработке вычислителей, интерпретаторов и компиляторов,
а также к реализации алгоритмов вывода типов для учебных языков.
УДК 004.42
ББК 32.973-018
Электронное издание на основе печатного издания: Введение в теорию языков программирования
/ Ж. Довек, Ж.-Ж. Леви ; пер. с англ. В. Н. Брагилевского, А. М. Пеленицына.
— Москва : ДМК Пресс, 2016. — 134 с. — ISBN 978-5-97060-242-3. — Текст : непосредственный.
Все
права защищены. Любая часть этой книги не может быть воспроизведена в какой бы то ни было
форме и какими бы то ни было средствами без письменного разрешения владельцев авторских прав.
Материал, изложенный в данной книге, многократно проверен. Но поскольку вероятность технических
ошибок все равно существует, издательство не может гарантировать абсолютную точность и правильность
приводимых сведений. В связи с этим издательство не несет ответственности за возможные ошибки,
связанные с использованием книги.
В соответствии со ст. 1299 и 1301 ГК РФ при устранении ограничений, установленных техническими средствами
защиты авторских прав, правообладатель вправе требовать от нарушителя возмещения убытков или выплаты
компенсации.
ISBN 978-5-89818-582-4
© 2011 Springer-Verlag London Limited
© Перевод на русский язык, оформление,
ДМК Пресс, 2015
Стр.5
Оглавление
От переводчиков
Что называют теорией языков программирования?
Благодарности
Глава 1. Термы и отношения
9
13
17
19
1.1. Индуктивные определения . . . . . . . . . . . . . . . . . 19
1.1.1. Теорема о неподвижной точке . . . . . . . . . . . 19
1.1.2. Индуктивные определения . . . . . . . . . . . . . 22
1.1.3. Структурная индукция . . . . . . . . . . . . . . . 25
1.1.4. Рефлексивно-транзитивное замыкание отношения 25
1.2. Языки . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26
1.2.1. Языки без переменных . . . . . . . . . . . . . . . 26
1.2.2. Переменные . . . . . . . . . . . . . . . . . . . . . . 26
1.2.3. Многосортные языки . . . . . . . . . . . . . . . . 29
1.2.4. Свободные и связанные переменные . . . . . . . 29
1.2.5. Подстановка . . . . . . . . . . . . . . . . . . . . . 30
1.3. Три способа задания семантики языка . . . . . . . . . . 32
1.3.1. Денотационная семантика . . . . . . . . . . . . . 32
1.3.2. Операционная семантика с большим шагом . . . 32
1.3.3. Операционная семантика с малым шагом . . . . 33
1.3.4. Незавершающиеся вычисления . . . . . . . . . . 33
Глава 2. Язык PCF
35
2.1. Функциональный язык PCF . . . . . . . . . . . . . . . . 35
2.1.1. Программы как функции . . . . . . . . . . . . . . 35
2.1.2. Функции как объекты первого класса . . . . . . 35
2.1.3. Функции с несколькими аргументами . . . . . . . 36
Стр.6
6
Оглавление
2.1.4. Без присваиваний . . . . . . . . . . . . . . . . . . 36
2.1.5. Рекурсивные определения . . . . . . . . . . . . . 36
2.1.6. Определения . . . . . . . . . . . . . . . . . . . . . 37
2.1.7. Язык PCF . . . . . . . . . . . . . . . . . . . . . . . 37
2.2. Операционная семантика с малым шагом . . . . . . . . 39
2.2.1. Правила . . . . . . . . . . . . . . . . . . . . . . . . 39
2.2.2. Числа . . . . . . . . . . . . . . . . . . . . . . . . . 40
2.2.3. Эквивалентность (congruence) . . . . . . . . . . . 42
2.2.4. Пример . . . . . . . . . . . . . . . . . . . . . . . . 42
2.2.5. Нередуцируемые замкнутые термы . . . . . . . . 43
2.2.6. Незавершающиеся вычисления . . . . . . . . . . 45
2.2.7. Слияние (confluence) . . . . . . . . . . . . . . . . . 46
2.3. Стратегии редукции . . . . . . . . . . . . . . . . . . . . 47
2.3.1. Понятие стратегии . . . . . . . . . . . . . . . . . . 47
2.3.2. Слабая редукция . . . . . . . . . . . . . . . . . . . 48
2.3.3. Вызов по имени . . . . . . . . . . . . . . . . . . . 49
2.3.4. Вызов по значению . . . . . . . . . . . . . . . . . 50
2.3.5. Немного лени не помешает . . . . . . . . . . . . . 50
2.4. Операционная семантика с большим шагом . . . . . . . 51
2.4.1. Вызов по имени . . . . . . . . . . . . . . . . . . . 51
2.4.2. Вызов по значению . . . . . . . . . . . . . . . . . 52
2.5. Вычисление PCF-программ . . . . . . . . . . . . . . . . 54
Глава 3. От вычисления к интерпретации
57
3.1. Вызов по имени . . . . . . . . . . . . . . . . . . . . . . . 57
3.2. Вызов по значению . . . . . . . . . . . . . . . . . . . . . 59
3.3. Оптимизация: индексы де Брауна . . . . . . . . . . . . 60
3.4. Построение функций с помощью неподвижных точек . 63
3.4.1. Первая версия: рекурсивные замыкания . . . . . 63
3.4.2. Вторая версия: рациональные значения . . . . . 65
Глава 4. Компиляция
69
4.1. Интерпретатор, написанный на языке без функций . . 70
4.2. От интерпретации к компиляции . . . . . . . . . . . . . 71
4.3. Абстрактная машина для PCF . . . . . . . . . . . . . . 72
4.3.1. Окружение . . . . . . . . . . . . . . . . . . . . . . 72
4.3.2. Замыкания . . . . . . . . . . . . . . . . . . . . . . 72
4.3.3. Конструкции PCF . . . . . . . . . . . . . . . . . . 73
4.3.4. Использование индексов де Брауна . . . . . . . . 74
4.3.5. Операционная семантика с малым шагом . . . . 74
4.4. Компиляция PCF . . . . . . . . . . . . . . . . . . . . . . 75
Стр.7
Оглавление
7
Глава 5. PCF с типами
79
5.1. Типы . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 80
5.1.1. PCF с типами . . . . . . . . . . . . . . . . . . . . 80
5.1.2. Отношение типизации . . . . . . . . . . . . . . . . 82
5.2.2. Использование операционной семантики с
большим шагом . . . . . . . . . . . . . . . . . . . 85
5.2. Отсутствие ошибок во время выполнения . . . . . . . . 84
5.2.1. Использование операционной семантики с
малым шагом . . . . . . . . . . . . . . . . . . . . . 84
5.3. Денотационная семантика для PCF с типами . . . . . . 86
5.3.1. Тривиальная семантика . . . . . . . . . . . . . . . 86
5.3.2. Завершаемость . . . . . . . . . . . . . . . . . . . . 87
5.3.3. Отношение порядка Скотта . . . . . . . . . . . . 89
5.3.4. Семантика неподвижной точки . . . . . . . . . . 90
Глава 6. Вывод типов
95
6.1. Вывод мономорфных типов . . . . . . . . . . . . . . . . 95
6.1.1. Присвоение типов нетипизированным термам . . 95
6.1.2. Алгоритм Хиндли . . . . . . . . . . . . . . . . . . 96
6.1.3. Алгоритм Хиндли с немедленным разрешением . 99
6.2. Полиморфизм . . . . . . . . . . . . . . . . . . . . . . . . 101
6.2.1. PCF с полиморфными типами . . . . . . . . . . . 102
6.2.2. Алгоритм Дамаса—Милнера . . . . . . . . . . . . 104
Глава 7. Ссылки и присваивание
Глава 8. Записи и объекты
107
7.1. Расширение PCF . . . . . . . . . . . . . . . . . . . . . . 108
7.2. Семантика PCF со ссылками . . . . . . . . . . . . . . . 109
117
8.1. Записи . . . . . . . . . . . . . . . . . . . . . . . . . . . . 117
8.1.1. Помеченные поля . . . . . . . . . . . . . . . . . . 117
8.1.2. Расширение PCF записями . . . . . . . . . . . . . 118
8.2. Объекты . . . . . . . . . . . . . . . . . . . . . . . . . . . 122
8.2.1. Методы и функциональные поля . . . . . . . . . 122
8.2.2. Что значит «Self»? . . . . . . . . . . . . . . . . . . 123
8.2.3. Объекты и ссылки . . . . . . . . . . . . . . . . . . 125
Послесловие
Библиография
Предметный указатель
127
131
132
Стр.8