Введение в теорию языков программирования

Жиль Довек, Жан-Жак Леви

Введение в теорию

языков программирования

Москва, 2016

Introduction to the Theory of
Programming Languages

Gilles Dowek, Jean-Jacques L´evy

Введение в теорию
языков программирования

Жиль Довек, Жан-Жак Леви

Перевод с английского
В. Н. Брагилевского и А. М. Пеленицына

Москва, 2023

2-е издание, электронное

УДК 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

Оглавление

От переводчиков
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. Функции с несколькими аргументами . . . . . . .
36

Оглавление

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

От переводчиков

Теория языков программирования является важным разделом современной теоретической информатики, она активно развивается в работах
западных специалистов, ей посвящаются большие конференции, статьи по
этой тематике публикуются в ведущих научных журналах. К сожалению,
эта теория долгое время оставалась на обочине советской, а затем российской науки, что, видимо, привело к дефициту русскоязычной литературы,
в которой излагались бы её основы. Тем не менее, хотелось бы указать
несколько исключений.
В первую очередь следует упомянуть сборник переводов под общим
названием «Математическая логика в программировании» [1], изданный
в 1991 году. В нём были опубликованы статьи таких известных учёных
как Дана Скотт, Роджер Хиндли, Саймон Пейтон Джонс и других. Большой вклад в доведение теории языков программирования до российского
читателя много позже внесла публикация перевода обширной научной монографии Джона Митчелла «Основания языков программирования» [2],
выполненного под научной редакцией Н. Н. Непейводы. Наконец, благодаря труду энтузиастов был издан перевод книги Бенджамина Пирса «Типы
в языках программирования» [3].
Настоящая книга представляет собой введение в теорию языков программирования, по содержанию и стилю изложения намного более доступное, чем любая из перечисленных книг. Авторам удалось вместить в очень
небольшой объём самые необходимые сведения, удачно соединив вопросы операционной и денотационной семантики программ и теорию типов.
В книге также нашлось место достаточному числу упражнений, что исключительно важно для начинающих. В результате данное издание можно рекомендовать для факультативов или семинаров на младших курсах
университетов, а также для самостоятельного изучения. Упомянутые выше
книги могли бы составить основу для более глубокого знакомства с темой
на старших курсах, что обеспечило бы теории языков программирования
более достойное место в университетских курсах, чем мы видим сейчас в
нашей стране.

От переводчиков

Несмотря на выход указанных изданий, в литературе по данному
предмету остаётся несколько существенных пробелов, обозначим два из
них. В теории языков программирования можно выделить два крупных
раздела: теория типов и семантика языков программирования. Упомянутая выше книга Б. Пирса, а верней её перевод, даёт достаточно полное
представление о теории типов. К сожалению, нам неизвестно перевода или
оригинальной сравнимой по уровню работы на русском языке, посвящённой семантике языков программирования. Достойными кандидатами на
эту роль видятся книги Карла Гюнтера или Глинна Винскеля, приведённые в авторском списке литературы в конце книги (пункты 3 и 14 соответственно), если бы они были изданы на русском языке.
Для глубокого изучения теории языков программирования совершенно необходимо знакомство с лямбда-исчислением, которое вполне можно
считать тем самым «единственным универсальным» языком программирования, упомянутым авторами во введении к данной книге, но только
для специалистов по теории языков программирования. Оно вводится в
том или ином объёме в книгах Б. Пирса и Д. Митчелла, но (весьма разумно) обойдено стороной в настоящем издании. Тем не менее, полезно
было бы иметь русскоязычное издание, посвящённое целиком этому предмету. Стоит отметить, что в издательстве «Мир» ещё в 1985 году выходил
перевод энциклопедической книги выдающегося голландского учёного и
специалиста в этой области Хенка Барендрегта «Ламбда-исчисление. Его
синтаксис и семантика» [4]. Однако эта работа целиком посвящена бестиповому лямбда-исчислению, в то время как для современной теории языков
программирования более важным представляется лямбда-исчисление с типами, великолепно описанное в доступной форме университетского учебника, например, Роджером Хиндли и Джонатаном Селдином [5]. Пример
того, как более глубокое изучение вопросов типизации языков программирования часто проводится в рамках лямбда-исчисления, дают пятая и
шестая главы настоящей книги, в которых приведены два различных подхода к типизации. Эти два подхода по существу соответствуют «типизации
по Чёрчу» и «типизации по Карри», детально рассматриваемым в книге
Р. Хиндли и Дж. Селдина.
Ещё один компонент общего образования в информатике, который используется в большинстве книг по теории языков программирования, это
функциональное программирование. Прекрасный обзор переводной и оригинальной литературы по этому предмету содержится в статье [6]. Заметим лишь, что в данной книге, как и в издании труда Б. Пирса, для иллюстрации материала используется язык программирования ML, относительно непопулярный в российском академическом сообществе. Нетрудно