Введение в теорию языков программирования
Покупка
Тематика:
Программирование и алгоритмизация
Издательство:
ДМК Пресс
Год издания: 2013
Кол-во страниц: 134
Дополнительно
Вид издания:
Учебное пособие
Уровень образования:
ВО - Бакалавриат
ISBN: 978-5-94074-913-4
Артикул: 458607.03.99
К покупке доступен более свежий выпуск
Перейти
Языки программирования от Фортрана и Кобола до Caml и Java играют ключевую роль в управлении сложными компьютерными системами. Книга «Введение в теорию языков программирования» представляет читателю средства, необходимые для проектирования и реализации подобных языков. В ней предлагается единый подход к различным формализмам для определения языков программирования — операционной и денотационной семантике. Особое внимание при этом уделяется способам задания отношений между тремя объектами: программой, входным значением и результатом. Эти формализмы демонстрируются на примере таких типичных элементов языков программирования, как функции, рекурсия, присваивание, записи и объекты. При этом показывается, что теория языков программирования состоит не в последовательном изучении самих языков один за другим, а строится вокруг механизмов, входящих в различные языки. Изучение таких механизмов в книге приводит к разработке вычислителей, интерпретаторов и компиляторов, а также к реализации алгоритмов вывода типов для учебных языков.
Тематика:
ББК:
УДК:
ОКСО:
- ВО - Бакалавриат
- 02.03.01: Математика и компьютерные науки
- 02.03.02: Фундаментальная информатика и информационные технологии
- 09.03.01: Информатика и вычислительная техника
- 09.03.02: Информационные системы и технологии
- 09.03.03: Прикладная информатика
- 09.03.04: Программная инженерия
ГРНТИ:
Скопировать запись
Фрагмент текстового слоя документа размещен для индексирующих роботов
Жиль Довек, Жан-Жак Леви Введение в теорию языков программирования Москва, 2013
Introduction to the Theory of Programming Languages Gilles Dowek, Jean-Jacques L´evy
Введение в теорию языков программирования Жиль Довек, Жан-Жак Леви Перевод с английского В. Н. Брагилевского и А. М. Пеленицына Москва, 2013 Издание рекомендовано в качестве учебного пособия для студентов технических вузов
УДК 004.42 ББК 32.973-018 Д58 Д 58 Довек Жиль, Леви Жан-Жак Введение в теорию языков программирования — Пер. с англ. — М.: ДМК Пресс, 2013. — 134 с.: ил. ISBN 978-5-94074-913-4 Языки программирования от Фортрана и Кобола до Caml и Java играют ключевую роль в управлении сложными компьютерными системами. Книга «Введение в теорию языков программирования» представляет читателю средства, необходимые для проектирования и реализации подобных языков. В ней предлагается единый подход к различным формализмам для определения языков программирования — операционной и денотационной семантике. Особое внимание при этом уделяется способам задания отношений между тремя объектами: программой, входным значением и результатом. Эти формализмы демонстрируются на примере таких типичных элементов языков программирования, как функции, рекурсия, присваивание, записи и объекты. При этом показывается, что теория языков программирования состоит не в последовательном изучении самих языков один за другим, а строится вокруг механизмов, входящих в различные языки. Изучение таких механизмов в книге приводит к разработке вычислителей, интерпретаторов и компиляторов, а также к реализации алгоритмов вывода типов для учебных языков. УДК 004.42 ББК 32.973-018 Все права защищены. Любая часть этой книги не может быть воспроизведена в какой бы то ни было форме и какими бы то ни было средствами без письменного разрешения владельцев авторских прав. Материал, изложенный в данной книге, многократно проверен. Но, поскольку вероятность технических ошибок всё равно существует, издательство не может гарантировать абсолютную точность и правильность приводимых сведений. В связи с этим издательство не несёт ответственности за возможные ошибки, связанные с использованием книги. ISBN 978-0-85729-075-5 (англ.) © 2011 Springer-Verlag London Limited ISBN 978-5-94074-913-4 (рус.) © Перевод на русский язык, оформление, ДМК Пресс, 2013
Оглавление От переводчиков 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, относительно непопулярный в российском академическом сообществе. Нетрудно
К покупке доступен более свежий выпуск
Перейти