Введение в теорию языков программирования (3000,00 руб.)

Стр.5

Стр.6

Стр.7

Стр.8

УДК 004.42 ББК 32.973-018 Д58 Д 58 Довек Жиль, Леви Жан-Жак Введение в теорию языков программирования — Пер. с англ. — М.: ДМК Пресс, 2015. — 134 с.: ил. ISBN 978-5-97060-242-3 Языки программирования от Фортрана и Кобола до Caml и Java играют ключевую роль в управлении сложными компьютерными системами. Книга «Введение в теорию языков программирования» представляет читателю средства, необходимые для проектирования и реализации подобных языков. В ней предлагается единый подход к различным формализмам для определения языков программирования — операционной и денотационной семантике. Особое внимание при этом уделяется способам задания отношений между тремя объектами: программой, входным значением и результатом. Эти формализмы демонстрируются на примере таких типичных элементов языков программирования, как функции, рекурсия, присваивание, записи и объекты. При этом показывается, что теория языков программирования состоит не в последовательном изучении самих языков один за другим, а строится вокруг механизмов, входящих в различные языки. Изучение таких механизмов в книге приводит к разработке вычислителей, интерпретаторов и компиляторов, а также к реализации алгоритмов вывода типов для учебных языков. УДК 004.42 ББК 32.973-018 Все права защищены. Любая часть этой книги не может быть воспроизведена в какой бы то ни было форме и какими бы то ни было средствами без письменного разрешения владельцев авторских прав. Материал, изложенный в данной книге, многократно проверен. Но, поскольку вероятность технических ошибок всё равно существует, издательство не может гарантировать абсолютную точность и правильность приводимых сведений. В связи с этим издательство не несёт ответственности за возможные ошибки, связанные с использованием книги. ISBN 978-0-85729-075-5 (англ.) © 2011 Springer-Verlag London Limited ISBN 978-5-97060-242-3(рус.) 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