От переводчиков 9
Что называют теорией языков программирования? 13
Благодарности 17
Глава 1. Термы и отношения 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. Функции с несколькими аргументами . . . . . . . 366 Оглавление
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
Глава 5. PCF с типами 79
5.1. Типы . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 80
5.1.1. PCF с типами . . . . . . . . . . . . . . . . . . . . 80
5.1.2. Отношение типизации . . . . . . . . . . . . . . . . 82
5.2. Отсутствие ошибок во время выполнения . . . . . . . . 84
5.2.1. Использование операционной семантики с
малым шагом . . . . . . . . . . . . . . . . . . . . . 84
5.2.2. Использование операционной семантики с
большим шагом . . . . . . . . . . . . . . . . . . . 85
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. Ссылки и присваивание 107
7.1. Расширение PCF . . . . . . . . . . . . . . . . . . . . . . 108
7.2. Семантика PCF со ссылками . . . . . . . . . . . . . . . 109
Глава 8. Записи и объекты 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