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

Исследование систем типов, а также языков программирования с точки зрения теории типов, в последнее время превратилось в энергично развивающуюся научную дисциплину, имеющую важные приложения в проектировании программ, дизайне языков программирования, реализации высокопроизводительных компиляторов и в области безопасности. Настоящий текст представляет собой подробное введение в основные понятия, достижения и методы этой дисциплины.

Предполагаемая аудитория

Книга предназначена для двух основных групп читателей: с одной стороны, для аспирантов и исследователей, специализирующихся на языках программирования и теории типов; с другой стороны, для аспирантов и продвинутых студентов из других областей информатики, которые хотели бы получить введение в основные понятия теории языков программирования. Для первой из этих групп книга дает обширный обзор рассматриваемой области, с глубиной, достаточной для чтения исследовательской литературы. Для второй она предоставляет подробный вводный материал и обширное собрание примеров, упражнений и практических ситуаций. Книга может служить как для вводных курсов аспирантского уровня, так и для более продвинутых семинаров по языкам программирования.

Цели

Основной моей задачей был охват материала, включая базовую операционную семантику и связанные с ней способы построения доказательств, бестиповое лямбда-исчисление, простые системы типов, универсальный и экзистенциональный полиморфизм, реконструкцию типов, иерархии типов, ограниченную квантификацию, рекурсивные типы и операторы над типами, а также краткое обсуждение некоторых других тем.

Второй задачей был прагматизм. Книга сосредоточена на использовании систем типов в языках программирования, за счет некоторых тем (например, денотационной семантики), которые, вероятно, были бы включены в более математически ориентированный текст по типизированным лямбда-исчислениям. В качестве базового вычислительного формализма выбрано лямбда-исчисление с вызовом по значению, которое соответствует большинству современных языков программирования и легко расширяется императивными конструкциями вроде ссылок и исключений. При рассмотрении каждого языкового элемента основными вопросами являются: практическая мотивация для введения этого элемента; методы доказательства безопасности языков, включающих его; а также трудности, с которыми приходится сталкиваться при его реализации — в особенности, построение и анализ алгоритмов проверки типов.

Также задачей было уважение к разнообразию в рассматриваемой дисциплине; книга охватывает множество отдельных тем и несколько хорошо исследованных их сочетаний, но при этом не предпринимается попытки собрать все в единую целостную систему. Существуют единые подходы к некоторым подмножествам набора тем — например, многие разновидности “стрелочных типов” можно компактно и изящно описать в единой нотации чистых систем типов, — но дисциплина в целом пока что растет слишком быстро, чтобы можно было систематизировать ее целиком.

Книга построена так, чтобы облегчить ее использование, как в рамках университетских курсов, так и при самостоятельном изучении. Для большинства упражнений прилагаются полные решения. Базовые определения организованы в самодостаточные таблицы, чтобы их легко было найти. Зависимости между понятиями и системами по возможности явно указываются. К тексту прилагается обширная библиография и индекс.

Последним организующим принципом при написании книги была честность. Все обсуждаемые в книге системы (кроме некоторых, лишь упомянутых мельком) реализованы. Для каждой главы существует программа проверки типов и интерпретатор, и все примеры механически проверены с их помощью. Эти программы доступны на веб-сайте книги, их можно использовать при программировании упражнений, для экспериментов по дальнейшему расширению и в учебных проектах.

Для того, чтобы достичь поставленных целей, пришлось отказаться от желания придать книге некоторые желательные свойства. Наиболее важное из них — полнота рассмотрения. Полный обзор дисциплины языков программирования и систем типов, вероятно, невозможен в рамках одного текста – уж точно не в рамках учебника. Я сосредоточился на тщательном рассмотрении базовых понятий; многочисленные отсылки на научную литературу служат как отправные точки для дальнейшего исследования. Также не была целью практическая эффективность алгоритмов проверки типов: эта книга не является пособием по реализации компиляторов промышленного качества.

Структура книги

В Части I обсуждаются бестиповые системы. Основные понятия абстрактного синтаксиса, индуктивные определения и доказательства, правила вывода и операционная семантика сначала вводятся в контексте чрезвычайно простого языка для работы с числами и логическими значениями, затем повторяются для бестипового лямбда-исчисления. В Части II рассматривается простое типизированное лямбда-исчисление, а также набор базовых языковых конструкций: произведение, сумма, записи, варианты, ссылки и исключения. Предварительная глава о типизированных арифметических выражениях плавно подводит к ключевой идее типовой безопасности. В промежуточной главе (которую можно пропустить) методом Тейта доказывается теорема о нормализации для простого типизированного лямбда-исчисления. Часть III посвящена основополагающему механизму наследования; она содержит подробное обсуждение метатеории и два расширенных примера. В Части IV рассматриваются рекурсивные типы, как в простой изорекурсивной формулировке, так и в более хитроумной эквирекурсивной. Вторая из двух глав этой части развивает метатеорию системы с эквирекурсивными типами и наследованием в рамках математической конструкции с коиндукцией. Темой Части V является полиморфизм. Она содержит главы по реконструкции типов в стиле ML, по более мощному импредикативному полиморфизму Системы F, по экзистенциальной квантификации и ее связям с абстрактными типами данных, а также по комбинации полиморфизма и наследования в системах с ограниченной квантификацией. В Части VI речь идет об операторах над типами. В одной главе вводятся основные понятия; в следующей разрабатывается Система F_ω и ее метатеория; в третьей операторы над типами скрещиваются с ограниченной квантификацией, давая в результате Систему F_<^ω; последняя глава представляет собой расширенный пример.

Основные зависимости между главами изображены на рис. 0.1. Серые стрелки означают, что только часть более поздней главы зависит от более ранней.

Обсуждение каждой языковой конструкции, представленной в книге, следует общей схеме. Сначала идут мотивирующие примеры; затем формальные определения; затем доказательства основных свойств, таких как типовая безопасность; затем (обычно в отдельной главе) более глубокое исследование метатеории, которое ведет к алгоритмам проверки типов и доказательству их корректности, полноты и гарантии завершения; наконец (опять же, в отдельной главе) конкретная реализация этих алгоритмов в виде программы на языке OCaml.

На протяжении всей книги важным источником примеров служит анализ и проектирование языковых свойств для объектно-ориентированного программирования. В четырех главах с расширенными примерами детально развиваются различные подходы — простая модель с обыкновенными императивными объектами и классами (Глава 18), базовое исчисление, основанное на Java (Глава 19), более изысканный подход к императивным объектам с использованием ограниченной квантификации (Глава 27) и рассмотрение объектов и классов в рамках чисто функциональной Системы F_<^ω, при помощи экзистенциальных типов (Глава 32).

Для того, чтобы удержать размер книги в рамках необходимого для односеместрового продвинутого курса — а вес ее в рамках подъемного для среднего аспиранта, — пришлось исключить из рассмотрения многие интересные и важные темы. Денотационный и аксиоматический подходы к семантике опущены полностью; по этим направлениям уже существуют замечательные книги, и эти темы отвлекали бы от строго прагматической, ориентированной на реализацию перспективы, принятой в этой книге. В нескольких местах делаются намеки на богатые связи между системами типов и логикой, но в детали я не вдаюсь; эти связи важны, но они увели бы нас слишком далеко в сторону. Многие продвинутые черты языков программирования и систем типов лишь кратко упомянуты, например, зависимые типы, типы-пересечения, а также соответствие Карри-Ховарда; краткие разделы по этим вопросам служат как отправные пункты для дальнейшего чтения. Наконец, за исключением краткого экскурса в Java-подобный базовый язык (Глава 19), в книге рассматриваются исключительно языки на основе лямбда-исчисления; однако понятия и механизмы, исследованные в этих рамках, могут напрямую быть перенесены в родственные области, такие как типизированные параллельные языки, типизированные ассемблеры и специализированные исчисления объектов.

Требуемая подготовка

Текст не предполагает никаких знаний по теории языков программирования, однако читатели должны в известной степени обладать математической зрелостью — а именно, иметь опыт строгой учебной работы в таких областях, как дискретная математика, алгоритмы и элементарная логика.

Читатели должны быть знакомы по крайней мере с одним функциональным языком высокого уровня (Scheme, ML, Haskell и т. п.) и с основными понятиями в теории языков программирования и компиляторов (абстрактный синтаксис, грамматики BNF, вычисление, абстрактные машины и т. п.). Этот материал доступен для изучения во множестве замечательных учебников; я особенно ценю “Основные понятия языков программирования” Фридмана, Ванда и Хейнса (Friedman, Wand, and Haynes, Essentials of Programming Languages, 2001), а также “Прагматику языков программирования” Скотта (Scott, Programming Language Pragmatics, 1999). В нескольких главах полезен будет опыт работы с объектно-ориентированным языком, например, с Java (Arnold and Gosling, 1996).

Главы, посвященные конкретным реализациям программ проверки типов, содержат большие фрагменты кода на OCaml (он же Objective Caml), популярном диалекте языка ML. Для чтения этих глав будет полезно знать OCaml заранее, но это не абсолютно необходимо; используется только небольшое подмножество языка, и его конструкции объясняются при первом использовании. Эти главы образуют отдельную нить в ткани книги, и при желании их можно полностью пропустить.

В настоящее время лучший учебник по OCaml — Кузино и Мони (Cousineau and Mauny, 1998). Кроме того, вполне читабельны и учебные материалы, поставляемые с дистрибутивом OCaml (http://caml.inria.fr или http://www.ocaml.org).

Для читателей, знакомых с другим крупным диалектом ML, Стандартным ML, фрагменты кода на OCaml не должны представлять трудности. Срели популярных учебников по Стандартному ML можно назвать книги Поульсона (Paulson 1996) и Ульмана (Ullman 1997).

Примерный план курса

В рамках аспирантского курса среднего или продинутого уровня должно быть возможно пройти большую часть материала книги за семестр. На рис 0.2 показана примерная схема продвинутого курса для аспирантов Пенсильванского университета (две лекции по 90 минут в неделю; предполагается наличие минимальной подготовки в теории языков программирования, однако продвижение очень быстрое).

При составлении курса для студентов или начинающих аспирантов можно выбрать несколько способов подачи материала. Курс по системам типов в программировании будет сосредоточен на главах, где вводятся различные особенности типовых систем и показывается их использование; большая часть метатеории и главы, где строятся реализации, будут пропущены. Курс по основам теории и реализации систем типов, с другой стороны, может использовать все ранние главы, возможно, за исключением Главы 12 (еще, может быть, 19 и 21), принося в жертву более сложный материал в конце книги. Возможно также построить более короткие курсы, выбирая отдельные главы и следуя диаграмме на Рис. 0.1.

Книгу можно также использовать как основной текст в более широко организованном аспирантском курсе по теории языков программирования. Такой курс может потратить половину или две трети семестра на прохождение большей части книги, а остаток времени посвятить, скажем, рассмотрению теории параллелизма на основе книги Милнера по пи-исчислению (Milner 1999), введению в логику Хоара и аксиоматическую семантику (напр., Winskel 1993) или обзору продвинутых языковых конструкций вроде продолжений или модульных систем.

Если существенная роль отводится курсовым проектам, может оказаться полезным отложить часть теоретического материала (скажем, нормализацию, и, возможно, некоторые главы по метатеории), чтобы продемонстрировать широкий спектр примеров, прежде чем студенты выберут себе курсовые.

Упражнения

Большинство глав снабжено многочисленными примерами — некоторые рассчитаны на решение с помощью карандаша и бумаги, некоторые требуют программирования в обсуждаемых исчислениях, а некоторые рассматривают расширения для реализаций этих исчислений на ML. Ожидаемая сложность упражнений указывается по следующей шкале:

Упражения, отмеченные знаком ★, предназначены для быстрой проверки, насколько усвоен смысл какого-либо важного понятия. Я советую читателю останавливаться и отвечать на них, прежде чем продолжать чтение. В каждой главе набор упражнений примерно размером с домашнее задание отмечен знаком Рекомендуется.

В Приложении A для большинства упражнений приведены полные решения. Чтобы избавить читателя от поиска, в тех немногих случаях, когда их нет, используется значок ¬→.

Типографские соглашения

Большинство глав книги построено так: сначала особенности некоторой системы типов описываются в тексте, затем эта система определяется формально как набор правил вывода, сведенных в одну или несколько таблиц. Для того, чтобы облегчить их использование в качестве справочника, обычно эти определения приводятся полностью, включая не только новые правила для особенностей, обсуждаемых в данный момент, но и остальные, сколько их требуется для построения полного исчисления. Новые части системы печатаются на сером фоне, чтобы отличия от предыдущих систем были более заметны.

Необычным качеством этой книги является то, что все примеры были механически проверены при верстке: с помощью особого скрипта из каждой главы извлекались примеры, строилась и компилировалась специальная программа проверки типов, содержащая обсуждаемые в главе особенности, эта программа прогонялась на примерах, и результаты проверки вставлялись в текст. Система, которая делает при этом всю сложную работу, называется TinkerType и была написана Майклом Левином и мной (Levin and Pierce 2001). Средства на ее разработку были получены от Национального Научного Фонда по грантам CCR-9701826 Принципиальные основы программирования с объектами и CCR-9912352 Модульные системы типов.

Электронные ресурсы

Веб-сайт, посвященный этой книге, можно найти по адресу

На этом сайте расположены следующие ресурсы: список ошибок, найденных в тексте, предложения по возможным курсовым проектам, ссылки на дополнительный материал, предоставленные читателями, а также набор реализаций (программы проверки типов и простые интерпретаторы) для исчислений, построенных в каждой из глав книги.

Эти реализации представляют собой среду для экспериментов с примерами, приведенными в книге, и для проверки ответов на упражнения. Они написаны с упором на читабельность и расширяемость. Студенты в моих курсах успешно использовали их в качестве основы как для простых упражнений, требующих реализации, так и для курсовых проектов более солидного размера. Эти реализации написаны на OCaml. Компилятор OCaml доступен бесплатно по адресу http://caml.inria.fr, и на большинстве платформ устанавливается безо всякого труда.

Читателям стоит также знать о существовании Types Forum, списка рассылки, посвященного всем аспектам систем типов и их реализации. Список модерируется, так что в нем обеспечиваются относительно малый объем и высокая доля полезного сигнала по отношению к шуму в объявлениях и дискуссиях. Архивы и инструкции для подписчиков можно найти по адресу http://www.cis.upenn.edu/~bcpierce/types.

Благодарности

Читатели, которые найдут эту книгу полезной, должны прежде всего быть благодарны четырем учителям — Луке Карделли, Бобу Харперу, Робину Милнеру и Джону Рейнольдсу, — которые научили меня почти всему, что я знаю о языках программирования и типах.

Остаток своих знаний я приобрел в основном в совместных проектах; помимо Луки, Боба, Робина и Джона, среди моих партнеров в этих проектах были Мартин Абади, Гордон Плоткин, Рэнди Поллак, Дэвид Н. Тёрнер, Дидье Реми, Давиде Санджорджи, Адриана Компаньони, Мартин Хофман, Джузеппе Кастанья, Мартин Стеффен, Ким Брюс, Наоки Кобаяси, Харуо Хосоя, Ацуси Игараси, Филип Уодлер, Питер Бьюнеман, Владимир Гапеев, Майкл Левин, Питер Сьюэлл, Джером Вуийон и Эйдзиро Сумии. Совместная работа послужила для меня не только источником понимания, но и удовольствия от работы над этой темой.

Структура и организация этого текста стали лучше в результате консультаций по педагогике с Торстеном Альтеркирхом, Бобом Харпером и Джоном Рейнольдсом, а сам текст выиграл от замечаний и исправлений, авторами которых были Джим Александер, Джош Бердин, Тони Боннер, Джон Танг Бойланд, Дэйв Кларк, Диего Дайнезе, Оливье Данви, Мэттью Дэвис, Владимир Гапеев, Боб Харпер, Эрик Хилсдейл, Харуо Хосоя, Ацуси Игараси, Роберт Ирвин, Такаясу Ито, Асаф Кфури, Майкл Левин, Василий Литвинов, Пабло Лопес Оливас, Дэйв Маккуин, Нарсисо Марти-Олиет, Филипп Менье, Робин Милнер, Матти Нюкянен, Гордон Плоткин, Джон Превост, Фермин Рейг, Дидье Реми, Джон Рейнольдс, Джеймс Рили, Охад Роде, Юрген Шлегельмильх, Алан Шмитт, Эндрю Схонмакер, Олин Шиверс, Педрита Стивенс, Крис Стоун, Эйдзиро Сумии, Вэл Тэннен, Джером Вуийон и Филип Уодлер (я прошу прощения, если кого-то случайно забыл включить в этот список). Лука Карделли, Роджер Хиндли, Дэйв Маккуин, Джон Рейнольдс и Джонатан Селдин поделились исторической перспективой по отношению к некоторым запутанным вопросам.

Участники моих аспирантских семинаров в Индианском университете в 1997 и 1998 годах и в Пенсильванском университете в 1999 и 2000 годах работали с ранними версиями этой книги; их реакции и комментарии помогли мне придать ей окончательную форму. Боб Прайор и его сотрудники в издательстве MIT Press весьма профессионально провели рукопись через все многочисленные стадии публикации. Дизайн книги основан на макросах L^AT_EX, которые разработал для MIT Press Кристофер Маннинг.

Доказательства программ настолько скучны, что социальные механизмы математики на них не работают.Ричард Де Милло, Ричард Липтон и Алан Перлис, 1979 …Так что на социальные механизмы при верификации рассчитывать не стоит.Дэвид Дилл, 1999 Формальные методы не будут иметь существенного влияния до тех пор, пока их не смогут использовать люди, их не понимающие.приписывается Тому Мелхэму

Chapter 1 Введение

1.1 Типы в информатике

Современная технология программного обеспечения располагает широким репертуаром формальных методов, которые помогают добиться, чтобы система вела себя в соответствии с какой-либо спецификацией ее поведения, явной или неявной. На одном конце шкалы находятся мощные конструкции, такие как логика Хоара, языки алгебраической спецификации программ, модальные логики и денотационная семантика. Все они способны выразить требования к корректности программ чрезвычайно общего вида, однако часто очень трудны в использовании и требуют от программистов большой подготовки. На другом конце располагаются методы намного более скромные — настолько скромные, что автоматические программы проверки могут быть встроены в компиляторы, компоновщики или автоматические анализаторы программ, и применять их могут даже программисты, незнакомые с теориями, на которых они основаны. Примером такого облегченного формального метода могут служить программы проверки моделей, инструменты для поиска ошибок в конечных системах вроде интегральных схем или коммуникационных протоколов. Другой пример — приобретающий сейчас популярность мониторинг исполнения, набор приемов, позволяющих системе динамически обнаруживать, что работа какого-либо из ее компонентов расходится со спецификацией. Однако самый популярный и испытанный облегченный формальный метод – системы типов, основная тема этой книги.

Подобно многим другим терминам, используемым в больших сообществах, <<систему типов>> трудно определить так, чтобы покрывалось неформальное использование этих слов в среде разработчиков и реализаторов языков программирования, и чтобы определение было одновременно достаточно конкретным для работы с ним. Одно из возможных определений такое:

Несколько деталей заслуживают пояснения. Во-первых, это определение выделяет системы типов как инструмент для рассуждений о программах. Такой выбор слов отражает ориентацию этой книги на системы типов, используемые в языках программирования. В более общем смысле слова, термин системы типов (или теория типов) относится к намного более обширной области исследований в логике, математике и философии. В этом смысле слова типы были впервые формально описаны в начале 1900-х годов как средство избежать логических парадоксов, угрожавших основаниям математики, например, парадокса Рассела (Russell 1902). В течение двадцатого века типы превратились в один из стандартных инструментов логики, особенно в теории доказательств (см. Gandy 1976 и Hindley 1997), и пропитали собой язык философии и науки. В этой области основными достижениями были исходная Расселовская ветвящаяся теория типов (Whitehead and Russell, 1910), простая теория типов Рэмсея (Ramsey 1925) — основа для простого типизированного лямбда-исчисления Чёрча (Church 1940), — конструктивная теория типов Мартина-Лёфа (Martin-Löf 1973, 1984) и чистые системы типов Бенарди, Терлоу и Барендрегта (Benardi 1988, Terlouw 1989 и Barendregt 1992).

Даже внутри науки информатики существуют две различных ветви, где изучаются системы типов. Более практическая, где исследуются приложения к языкам программирования, является основной темой этой книги. Более абстрактная ветвь изучает соответствия между различными <<чистыми типизированными лямбда-исчислениями>> и разновидностями логики, через соответствие Карри-Ховарда (§9.4). В этих сообществах используются похожие понятия, системы записи и методы, однако имеются важные различия в ориентации. Например, исследования по типизированному лямбда-исчислению обычно имеют дело с системами, где гарантируется завершение для всякого правильно типизированного вычисления, в то время как большинство языков программирования жертвуют этим свойством, чтобы иметь возможность работать с инструментами вроде рекурсивных функций.

Еще одним важным свойством предложенного определения является упоминание классификации термов — синтаксических составляющих, — в соответствии со значениями, которые они породят, будучи вычисленными. Систему типов можно рассматривать как статическое приближение к поведению программы во время выполнения. (Более того, типы термов обычно вычисляются композиционально, то есть тип выражения зависит только от типов его подвыражений.)

Иногда слово <<статический>> добавляется явным образом — например, говорят о <<языках программирования со статической типизацией>>, — чтобы отличить анализ, производимый при компиляции, который мы рассматриваем здесь, от динамических или латентных типов в языках вроде Scheme (Sussman and Steele 1975; Kelsey, Clinger and Rees, 1998; Dybvig 1996), где при помощи тегов типов во время выполнения различаются различные виды структур в куче. Термин <<динамическая типизация>>, по нашему мнению, неверен (его следовало бы заменить на <<динамические проверки>>), но такое употребление является стандартным.

Будучи статическими, системы типов по необходимости консервативны: они способны однозначно доказать отсутствие определенных нежелательных видов поведения, но не могут доказать их наличие, и, следовательно, иногда вынуждены отвергать программы, которые на самом деле при выполнении ведут себя подобающим образом. Например, программа

будет отвергнута как неверно типизированная, даже если ⟨сложная проверка⟩ всегда выдает значение истина, поскольку статический анализ неспособен это заметить. Противоречие между консервативностью и выразительностью — важный фактор при разработке систем типов. Желание позволить как можно большему числу программ проходить проверку через присвоение более точно определенных типов их выражениям служит основной движущей силой в нашей научной дисциплине.

Подобным образом, относительно незамысловатые виды анализа, воплощенные в большинстве систем типов, неспособны запретить всякое нежелательное поведение в программах; они гарантируют только то, что программы свободны от определенных видов ошибок. Например, большинство систем типов могут статически убедиться, что аргументами элементарных арифметических операций всегда служат числа, что объект-получатель при вызове метода всегда имеет соответствующий метод, и т. п., но не могут проверить, что второй аргумент в операции деления не равен нулю, или что индексы при обращениях к массиву не выходят за границы.

Виды плохого поведения, которые в данном языке могут быть исключены при помощи типов, часто называют ошибками типов времени выполнения. Важно помнить, что набор таких ошибок зависит от выбора языка: несмотря на то, что между ошибками времени выполнения в разных языках есть существенное пересечение, в принципе каждая система типов сама указывает, какие именно ошибки она намерена предотвратить. Безопасность (или корректность) системы типов должна определяться по отношению к её собственному набору ошибок времени выполнения.

Виды неправильного поведения, выявляемые через анализ типов, не ограничиваются низкоуровневыми ошибками вроде вызова несуществующих методов: системы типов используют также для обеспечения высокоуровневой модульности и для защиты целостности абстракций, определяемых пользователем. Нарушения сокрытия информации, например, прямое обращение к полям объекта, чья реализация должна быть абстрактной, являются ошибками типа в той же мере, как и, скажем, обращение к целому числу как к указателю, приводящее к краху работы программы.

Процедуры проверки типов обычно встроены в компиляторы или компоновщики. Следовательно, они должны быть способны выполнять свою работу автоматически, без ручного вмешательства или взаимодействия с программистом, — т. е., они должны представлять собой вычислительно разрешимый анализ. Остается, однако, множество способов требовать указаний от программиста в виде явных аннотаций типов в программах. Обычно эти аннотации остаются достаточно простыми, чтобы программы было легче писать и читать. В принципе, однако, в аннотациях типов можно выразить полное доказательство, что программа соответствует некоторой произвольной спецификации; в этом случае, программа проверки типов превращается в программу проверки доказательств. В таких технологиях, как Расширенная Статическая Проверка (Extended Static Checking; Detlefs, Leino, Nelson and Saxe, 1998), стирается грань между системами типов и методами всеобъемлющей верификации программ. Эти методы реализуют полностью автоматизированную проверку для некоторого широкого класса желательных свойств, основываясь в работе на <<достаточно легковесных>> аннотациях программы.

Точно так же, нам прежде всего интересны методы, которые не просто в принципе поддаются автоматизации, но к которым прилагаются эффективные алгоритмы проверки типов. Впрочем, можно спорить, что именно достойно называться эффективным. Даже в широко используемых системах типов, вроде ML (Damas and Milner, 1982), время проверки в некоторых патологических случаях может быть громадным (Henglein and Marison 1991). Имеются даже языки, где задача проверки или реконструкции типов не является разрешимой, но где есть алгоритмы, которые ведут к быстрому останову <<в большинстве случаев, представляющих практический интерес>> (напр., Pierce and Turner 2000; Nadathur and Miller 1988; Pfenning 1994).

1.2 Для чего годятся типы

1.2.1 Выявление ошибок

Самое очевидное достоинство статической проверки типов — это то, что она помогает раньше обнаружить некоторые ошибки в программах. Рано обнаруженные ошибки можно немедленно исправить, и они не прячутся долгое время, чтобы потом неожиданно всплыть, когда программист занят чем-то совершенно другим — или даже после того, как программа выпущена для потребителей. Более того, часто ошибки можно более точно описать при проверке типов, а не во время выполнения, когда их последствия могут обнаружиться не сразу, а спустя некоторое время после того, как программа съезжает с правильного пути.

На практике статическая проверка типов обнаруживает удивительно широкий спектр ошибок. Программисты, работающие в языках с богатой системой типов, часто замечают, что их программы имеют тенденцию <<просто работать>> после того, как пройдут проверку типов, чаще, чем, как им самим кажется, они имеют право ожидать. Одно из возможных объяснений состоит в том, что не только тривиальные неточности (скажем, когда программист забывает преобразовать строку в число, прежде чем извлечь квадратный корень), но и более глубокие концептуальные ошибки (например, пропуск граничного условия в сложном разборе случаев, или смешение единиц измерения в научном вычислении) часто проявляются как несоответствия на уровне типов. Сила этого эффекта зависит от выразительности системы типов и от решаемой программистской задачи: программы, работающие с большим набором структур данных (скажем, программы обработки символьной информации, типа компиляторов) дают больше пищи для проверки типов, чем программы, где работа идет лишь с несколькими простыми типами, скажем, научные вычислительные задачи (хотя и тут могут оказаться полезны тонкие системы типов, поддерживающие анализ размерностей (Kennedy 1994)).

Извлечение максимальной выгоды из системы типов, как правило, требует от программиста некоторого внимания и готовности использовать возможности языка в полной мере; например, если в сложной программе все структуры данных закодированы как списки, компилятор не сможет оказать такую же помощь, как если для каждой из них определяется тип данных или абстрактный тип. В системы типов могут быть встроены специальные <<трюки>>, позволяющие выражать в виде типов информацию о структуре данных.

Для некоторых видов программ процедура проверки типов может служить инструментом сопровождения. Например, программист, которому требуется изменить определение сложной структуры, может не искать вручную все места в программе, где требуется изменить код, имеющий дело с этой структурой. Как только изменяется определение типа данных, во всех этих фрагментах кода возникают ошибки типов, и их можно найти путем простого прогона компилятора и исправления тех мест, где ломается проверка типов.

1.2.2 Абстракция

Еще один вид пользы, которую системы типов приносят в процессе разработки программ — это поддержание дисциплины программирования. В частности, в контексте построения крупномасштабных программных систем, системы типов являются стержнем языков описания модулей, при помощи которых упаковываются и связываются компоненты больших систем. Типы появляются в интерфейсах модулей (или близких по смыслу структур, таких, как классы); в сущности, сам интерфейс можно рассматривать как <<тип модуля>>, содержащий информацию о возможностях, которые модуль предоставляет — своего рода частичный контракт между разработчиками и пользователями.

Разбиение больших систем на модули с ясно определенными интерфейсами приводит к более абстрактному стилю проектирования, когда интерфейсы разрабатываются и обсуждаются отдельно от их окончательной реализации. Как правило, более абстрактный стиль мышления повышает качество проектов.

1.2.3 Документация

Типы полезны также при чтении программ. Объявления типов в заголовках процедур и интерфейсах модулей представляют собой разновидность документации и дают ценные указания о поведении программы. Более того, в отличие от описаний, упрятанных в комментарии, такая документация не может устареть, поскольку она проверяется при каждом прогоне компилятора. Эта роль типов особенно существенна в сигнатурах модулей.

1.2.4 Безопасность языков

К сожалению, термин <<безопасный язык>> еще более расплывчат, чем <<система типов>>. Несмотря на то, что, как правило, программисты могут при взгляде на язык сказать, является ли он безопасным, их мнения о том, что именно представляет собой типовая безопасность, подвержены сильному влиянию со стороны языкового сообщества, к которому они принадлежат. Неформально, впрочем, можно определить безопасные языки как такие, которые не позволяют программисту сломать систему.

Немного уточняя интуитивное определение, можно сказать, что безопасный язык — это язык, который защищает свои собственные абстракции. Всякий язык высокого уровня предоставляет программисту абстрактный взгляд на работу машины. Безопасность означает, что язык способен гарантировать целостность этих абстракций, а также абстракций более высокого уровня, вводимых при помощи описательных средств языка. Например, язык может предоставлять массивы, с операциями доступа к ним и обновления, как абстракцию нижележащей машинной памяти. Программист, использующий такой язык, ожидает, что массив можно модифицировать только через явное использование операций обновления — а не, скажем, путем записи в память за границами какой-либо структуры данных. Подобным образом, ожидается, что к переменным со статической областью видимости можно обратиться только изнутри этой области, что стек вызовов действительно ведет себя как стек и т. д. В безопасном языке с такими абстракциями можно обращаться абстрактно; в небезопасном нельзя: чтобы полностью понять, как программа может себя повести, требуется держать в голове множество разнообразных низкоуровневых деталей, например, размещение структур данных в памяти и порядок их выделения компилятором. В предельном случае программы, написанные на небезопасных языках, могут поломать не только свои собственные структуры данных, но и структуры своей среды исполнения; при этом результаты могут быть совершенно непредсказуемыми.

Безопасность языка — это не то же самое, что статическая безопасность типов. Можно достичь безопасности языка при помощи системы типов, но можно добиться ее и с помощью проверок на стадии выполнения, которые отлавливают бессмысленные операции в момент, когда производится попытка их исполнить, и останавливают программу или порождают исключение. К примеру, Scheme является безопасным языком, несмотря на отсутствие статической системы типов.

С другой стороы, в небезопасных языках часто имеются статические проверки типов, которые <<по возможности>> отлавливают хотя бы самые очевидные программистские огрехи. Впрочем, такие языки не могут считаться и безопасными с точки зрения типов, поскольку в общем случае они не могут гарантировать, что программы с правильными типами ведут себя правильно — проверка типов в таком языке может предположить наличие ошибок во время выполнения (что, безусловно, лучше, чем ничего), но не доказать их отсутствие.

Можно объяснить отсутствие языков в правой нижней клетке таблицы тем, что, когда имеются средства для проверки большинства операций на безопасность при выполнении, нетрудно проверять их все. (На самом деле, существует несколько языков с динамической проверкой, например, некоторые диалекты Бейсика для микрокомпьютеров с минимальными операционными системами, где имеются низкоуровневые примитивы для чтения и записи произвольных ячеек памяти, и при помощи этих операций можно нарушить целостность среды выполнения.)

Как правило, невозможно достичь безопасности выполнения при помощи только лишь статической типизации. Например, все языки, указанные как безопасные в таблице, динамически проверяют проверку выхода за границы массивов.¹Подобным образом, иногда языки со статической проверкой типов предоставляют операции (скажем, нисходящее преобразование типов в Java — см. §15.5), чьи правила проверки типов некорректны — безопасность языка достигается при помощи динамической проверки каждого употребления такой конструкции.

Безопасность языка редко бывает абсолютной. Безопасные языки часто предоставляют программистам <<черные ходы>>, например, вызовы функций, написанных на других, возможно небезопасных, языках. Иногда такие черные ходы даже содержатся в ограниченном виде внутри самого языка — Obj.magic в OCaml (Leroy 2000), Unsafe.cast в Нью-Джерсийской реализации Стандартного ML, и т. п. Языки Modula-3 (Cardelli et al. 1989; Nelson 1991) и C^# (Wille 2000) идут еще дальше и включают в себя <<небезопасные подъязыки>>, предназначенные для реализации низкоуровневых библиотек вроде сборщиков мусора. Особые возможности этих подъязыков можно использовать только в модулях, явно отмеченных словом unsafe <<небезопасный>>.

Карделли (Cardelli 1996) представляет несколько иную точку зрения на безопасность языка и проводит различие между диагностируемыми и недиагностируемыми ошибками времени выполнения. Диагностируемая ошибка вызывает немедленную остановку вычисления (или порождает исключение, которое можно обработать внутри программы), в то время как недиагностируемая ошибка может позволить вычислению продолжаться (по крайней мере некоторое время). Примером недиагностируемой ошибки может служить обращение к данным за пределами массива в языке C. С этой точки зрения, безопасный язык — это такой, который предотвращает недиагностируемые ошибки во время выполнения.

Еще одна точка зрения основана на понятии переносимости; ее можно выразить лозунгом <<Безопасный язык полностью определяется руководством программиста>>. Назовем определением языка набор вещей, которые программист должен понимать, чтобы уметь предсказывать поведение любой программы на языке. Тогда руководство программиста для языка вроде C не представляет собой определение, поскольку поведение некоторых программ (скажем, тех, где встречается непроверенное обращение к массивам или используется арифметика указателей) невозможно предсказать, не зная, как конкретный компилятор C располагает структуры в памяти и т. п., и при этом одна и та же программа может вести себя по-разному, будучи обработана разными компиляторами. Напротив, руководства по Java, Scheme и ML определяют (с различной степенью строгости) точное поведение любой программы, написанной на этих языках. Программа с правильной типизацией получит одни и те же результаты в любой корректной реализации этих языков.

1.2.5 Эффективность

Первые системы типов в информатике, начиная с 50-х годов в таких языках, как Фортран (Backus 1981), были введены для того, чтобы улучшить эффективность вычислений путем различения арифметических выражений с целым значением и с вещественным значением; это позволяло компилятору использовать различные представления чисел и порождать соответствующие машинные команды для элементарных операций. В безопасных языках можно достичь большей эффективности, избегая множества динамических проверок, которые иначе потребовались бы для обеспечения безопасности (можно статически доказать, что проверка всегда даст положительный результат). В наше время большинство высокопроизводительных компиляторов существенным ообразом опираются при оптимизации и порождении кода на информацию, собранную процедурой проверки типов. Даже компиляторы для языков без типовых систем как таковых проделывают большую работу, чтобы получить приближения к этой информации о типах.

Выигрыш в эффективности на основе информации о типах может возникнуть в неожиданных местах. Например, недавно было показано, что не только решения о генерации кода, но и представление указателей в параллельных научных вычислениях может быть улучшено с помощью информации, порождаемой при проверке типов. Язык Titanium (Yelick et al. 1998) использует вывод типов для анализа области видимости указателей и способен принимать измеримо лучшие решения на основе этих данных, чем программисты, оптимизирующие программы вручную. Компилятор ML Kit с помощью мощного алгоритма вывода регионов (Gifford, Jouvelot and Sheldon 1987; Jouvelot and Gifford 1991; Talpin and Jouvelot 1992; Tofte and talpin 1994, 1997; Tofte and Birkedal 1998) заменяет большинство вызовов сборщика мусора (в некоторых программах все вызовы) стековыми операциями управления памятью.

1.2.6 Другие приложения

Системы типов, помимо традиционных областей применения в программировании и проектировании языков, в последнее время используются в информатике и близких дисциплинах несколькими другими способами. Мы упомянем кое-какие из них.

Все большее значение приобретает использование систем типов в области безопасности компьютеров и сетей. Например, статическая типизация лежит в основе модели безопасности Java и архитектуры автоматического конфигурирования (plug and play) сетевых устройств JINI (Arnold et al. 1999), а также играет ключевую роль в методике <<кода, содержащего доказательство>> (Proof Carrying Code, Necula and Lee 1996, 1998; Necula 1997). В то же время, многие основополагаюшие идеи, появившиеся в среде специалистов по безопасности, получают развитие с точки зрения языков программирования, и часто выглядят как разновидности анализа типов (напр., Abadi, Banerjee, Heintze and Riecke 1999; Abadi 1999; Leroy and Rouaix 1998; и т. п.). С другой стороны, растет интерес к прямому приложению теории языков программирования в области компьютерной безопасности (напр., Abadi 1999; Sumii and Pierce 2001).

Алгоритмы проверки и вывода типов встречаются во многих инструментах анализа программ помимо компиляторов. Например, AnnoDomini, утилита преобразования программ на Коболе с точки зрения Проблемы 2000 года, построена на основе механизма вывода типов в стиле ML (Eidorff et al. 1999). Методы вывода типов использовались также в инструментах для анализа псевдонимов (O’Callahan and Jackson 1997) и анализа исключений (Leroy and Passaux 2000).

При автоматическом доказательстве теорем системы типов — обычно очень мощные, основанные на зависимых типах, — используются для представления логических утверждений и доказательств. Несколько популярных средств поддержки построения доказательств прямо основаны на теории типов, включая Nuprl (Constable et al. 1986), Lego (Luo and Pollack 1992; Pollack 1994), Coq (Barras et al. 1997) и Alf (Magnusson and Nordström 1994). Констебль (Constable 1994) и Пфеннинг (Pfenning 1999) содержат обсуждение истории этих систем.

Растет интерес к системам типов и в сообществе специалистов по базам данных, в связи с популярностью <<сетевых метаданных>> в форме Определений Типа Документов (Document Type Definitions, XML 1998) и других видов схем (таких, как новый стандарт XML-Schema, XS 2000) для описания структурированных данных на XML. Новые языки для запросов к XML и обработки XML-данных обладают мощными статическими системами типов, прямо основанными на этих языках схем (Hosoya and Pierce 2000; Hosoya, Vouillon and Pierce 2001; Hosoya and Pierce 2001; Relax 2000; Schields 2001).

Совершенно отдельная область приложения систем типов — вычислительная лингвистика, где типовые лямбда-исчисления лежат в основе таких формализмов, как категориальная грамматика (van Benthem 1995; van Benthem and Meulen 1997; Ranta 1995, и т. д.).

1.3 Системы типов и проектирование языков

Встраивание системы типов в существующий язык, который не разрабатывался с расчетом на проверку типов, может оказаться непростой задачей; в идеальном случае, проектирование языка должно идти одновременно с проектированием системы типов.

Одна из причин этого в том, что языки без систем типов — даже безопасные языки с динамическими проверками, — как правило, имеют конструкции или идиоматические приемы, которые осложняют проверку типов или даже делают ее невозможной. В типизированных же языках сама система типов часто рассматривается как основа языкового проекта и организующий принцип, и относительно него оценивается всякое другое решение разработчика.

Еще одним фактором служит то, что, как правило, ситнаксис типизированных языков сложнее, чем у нетипизированных, поскольку приходится принимать во внимание объявления типов. Построить красивый и понятный синтаксис проще, если учитывать все эти трудности сразу.

Утверждение, что типы должны являться неотъемлемой частью языка программирования, стоит отдельно от вопроса, в каких случаях программист должен явным образом указывать аннотации типа, а в каких случаях их может вычислить компилятор. Хорошо спроектированный типизированный язык никогда не будет требовать от программиста вручную выписывать длинные и утомительные декларации типов. Впрочем, существуют различные мнения по вопросу, какое количесство явной информации считать чрезмерным. Создатели языков семейства ML тщательно старались свести аннотации к самому минимуму, добывая недостающую информацию с помощью вывода типов. В языках из семейства C, включая Java, принят несколько более многословный стиль.

1.4 Краткая история

Самые ранние системы типов в информатике использовались для отображения очень простых различий в представлении чисел с фиксированной и плавающей точкой (например, в Фортране). В конце 1950-х и начале 1960-х эта классификация была расширена на структурированные данные (массивы записей и т. п.) и функции высшего порядка. В начале 1970-х появились еще более сложные понятия (параметрический полиморфизм, абстрактные типы данных, системы модулей и наследование), и системы типов превратились в отдельное направление исследований. В то же время специалисты по информатике обнаружили связь между системами типов в языках программирования и типами, изучаемыми в математической логике, и это привело к плодотворному взаимодействию между этими областями, продолжающемуся по сей день.

На Рис. 1.1 представлена краткая (и чрезвычайно неполная!) хронология основных достижений в истории систем типов в информатике. Курсивом отмечены открытия в области логики, чтобы показать важность этого направления. Ссылки на работы, указанные в правой колонке, можно найти в библиографии.

1.5 Дополнительная литература

Я пытался сделать эту книгу самодостаточной, но она далека от полного охвата; дисциплина теории типов слишком широка, введение в нее можно построить с различных точек зрения, и все их невознможно отобразить в одной книге. В этом разделе я перечисляю несколько других вводных текстов.

В обзорных статьях Карделли (Cardelli 1996) и Митчелла (Mitchell 1990b) содержится краткое введение в дисциплину. Статья Барендрегта (Barendregt 1992) предназначена скорее для математиков. Объемный учебник Митчелла <<Основания языков программирования>> (Mitchell, Foundations for Programming Languages, 1996) описывает основы лямбда-исчисления, несколько систем типов и многие вопросы семантики. Основное внимание уделяется семантике, а не подробностям реализации. Книга Рейнольдса <<Теории языков программирования>> (Reynolds Theories of Programming Languages, 1998b) — это обзор теории языков программирования, предназначенный для аспирантов и включающий изящное описание полиморфизма, наследования и типов-пересечений. <<Структура типизированных языков программирования>> Шмидта (Schmidt, The Structure of Typed Programming Languages, 1994) развивает основные понятия систем типов в контексте проектирования языков, и включает несколько глав по обыкновенным императивным языкам программирования. Монография Хиндли <<Основы теории простых типов>> (Hindley, Basic Simple Type Theory, 1997) представляет собой замечательное собрание результатов, полученных в теории простого типизированного лямбда-исчисления и близкородственных систем. Описание скорее глубокое, нежели широкое по охвату.

<<Теория объектов>> Абади и Карделли (Abadi and Cardelli, A Theory of Objects, 1996) развивает во многом тот же материал, что и настоящая книга, с меньшим упором на вопросы реализации. Вместо этого она подробно описывает применение основных идей для построения теории оснований объектно-ориентированного программирования. Книга Кима Брюса <<Основания объектно-ориентированных языков: типы и семантика>> (Kim Bruce, Foundations of Object-Oriented Languages: Types and Semantics, 2002) покрывает приблизительно тот же материал. Введение в теорию объектно-ориентированных систем типов можно также найти в книгах Палсберга и Шварцбаха (Palsberg and Schwartzbach, 1994) и Кастаньи (Castagna 1997).

Семантические основы как бестиповых, так и типизированных языков подробно рассмотрены в учебниках Гантера (Gunter 1992), Уинскеля (Winskel 1993) и Митчелла (Mitchell 1996). Кроме того, операционная семантика детально описана в книге Хеннесси (Hennessy 1990). Основания теории типов в рамках математической теории категорий можно найти во множестве источников, включая книги Якобса (Jacobs 1999), Асперти и Лонго (Asperti and Longo 1997) и Кроула (Crole 1994); краткое введение доступно в <<Основах теории категоий для специалистов по информатике>> (Pierce, Basic Category Theory for Computer Scientists, 1991a).

Книга Жирара, Лафонта и Тейлора <<Доказательства и типы>> (Girard, Lafont and Taylor, Proofs and Types, 1989) посвящена логическим вопросам теории типов (соответствие Карри-Ховарда и т. п.). Кроме того, она включает описание Системы F, сделанное ее создателем, и приложение по линейной логике. Связи между типами и логикой исследуются также в книге <<Вычисление и дедукция>> Пфеннинга (Pfenning, Computation and Deduction, 2001). <<Теория типов и функциональное программирование>> Томпсона (Thompson, Type Theory and Functional Programming, 1991) и <<Конструктивные основания функциональных языков>> Тёрнера (Turner, Constructive Foundations for Functional Languages, 1991) посвящены связям между функциональным программированием (в смысле <<чисто функционального программирования>>, как в языках Haskell и Miranda) и конструктивной теорий типов, рассматриваемой с точки зрения логики. Множество вопросов теории доказательств, имеющих отношение к программированию, рассмотрены в книге <<Теория типов и автоматическая дедукция>> Гобольт-Ларрека и Макки (Goubault-Laurrecq and Mackie, Proof Theory and Automated Deduction, 1997). История типов в логике и философии более подробно описана в статьях Констебля (Constable 1998), Уодлера (Wadler 2000), Юэ (Huet 1990) и Пфеннинга (Pfenning 1999), в диссертации Лаана (Laan 1997) и в книгах Граттан-Гиннесса (Grattan-Guinness 2001) и Соммаруги (Sommaruga 2000).

Как выясняется, чтобы избежать досадных ошибочных утверждений о корректности типов в языках программирования, требуется немалая доля тщательного анализа. В результате возникла формальная дисциплина классификации, описания и исследования систем типов. Лука Карделли (1996)

Chapter 2 Математический аппарат

Прежде, чем начать, нам нужно договориться об используемых обозначениях и упомянуть несколько базовых математических утверждений. Большинство читателей может бегло проглядеть эту главу и затем возвращаться к ней по мере необходимости.

2.1 Множества, отношения и функции

Определение 1 Мы пользуемся стандартными обозначениями для множеств: фигурные скобки, когда элементы множества перечисляются явным образом ({…}) или когда оно задается через <<выделение>> на основе другого множества ({x ∈ S | … }), ∅ для пустого множества, S \ T для теоретико-множественной разности S и T (множество элементов S, не являющихся элементами T). Мощность (количество элементов) множества S обозначается |S|. Множество всех подмножеств S обозначается ℘(S).

Определение 2 Множество натуральных чисел {0, 1, 2, 3, 4, 5,…} обозначается символом ℕ. Множество называется счетным, если между его элементами и натуральными числами существует взаимно-однозначное соответствие.

Определение 3 n-местное отношение на наборе множеств S₁, S₂, …, S_n — это множество R ⊆ S₁ × S₂ × … × S_n n-ок элементов S₁,… S_n. Если (s₁,…,s_n) ∈ R, где s₁ ∈ S₁, … s_n ∈ S_n, то говорится, что s₁, … s_n связаны отношением R.

Определение 4 Одноместное отношение на множестве S называется предикатом на S. Говорится, что P истинен на s ∈ S, если s ∈ P. Чтобы подчеркнуть эту интуицию, часто мы будем писать P(s) вместо s ∈ P, рассматривая P как функцию, переводящую элементы S в истинностные значения.

Определение 5 Двуместное отношение R на множествах S и T называется бинарным отношением. Часто мы будем писать s R t вместо (s,t) ∈ R. Если S и T совпадают (назовем это множество U), мы будем говорить, что R — бинарное отношение на U.

Определение 6 Чтобы облегчить чтение, многоместные (трех- и более) отношения часто записываются в <<смешанном>> синтаксисе, когда элементы отношения разделяются последовательностью символов, и эти символы вместе образуют имя отношения. Например, отношение типизации для простого типизированного лямбда-исчисления из Главы 9 записывается как Γ ⊢ s : T — такая формула означает <<тройка (Γ, s, T) находится в отношении типизации>>.

Определение 7 Областью определения отношения R между множествами S и T называется множество элементов s ∈ S, таких. что (s,t) ∈ R для какого-либо t. Область определения R обозначается dom(R). Областью значений R называется множество элементов t ∈ T, таких, что (s,t) ∈ R для какого-либо s. Область значений R обозначается range(R).

Определение 8 Отношение R на множествах S и T называется частичной функцией из S в T, если из (s,t₁) ∈ R и (s, t₂) ∈ R следует t₁ = t₂. Если, кроме того, dom(R) = S, то R называется всюду определенной (тотальной) функцией, или просто функцией, из S в T.

Определение 9 Частичная функция R из S в T определена на аргументе s ∈ S, если s ∈ dom(R), и не определена в противном случае. Запись f(x)↑ или f(x) = ↑ означает <<f не определена на x>>, а f(x)↓ означает <<f определена на x>>.

В некоторых главах, посвященных программной реализации систем типов, нам также потребуется определять функции, которые на некоторых аргументах терпят неудачу (см., например, Рис. 22.2). Важно отличать неудачу (частный случай разрешенного, наблюдаемого результата) от расхождения; функция, способная потерпеть неудачу, может быть либо частичной (т. е., может также расходиться), либо всюду определенной (т. е., она всегда либо возвращает результат, либо терпит неудачу) — в сущности, часто нам будет нужно доказывать тотальность такой функции. Если f возвращает неудачу при применении к x, мы будем писать f(x) = неудача.

С формальной точки зрения, функция из S в T, которая может вернуть неудачу, является на самом деле функцией из S в T ∪ {неудача} (мы предполагаем, что неудача не входит во множество T).

Определение 10 Пусть R — бинарное отношение на множестве S, а P — предикат на S. Если из s R s′ и P(s) следует P(s′), то говорится, что R сохраняет P.

2.2 Упорядоченные множества

Определение 1 Бинарное отношение R на множестве S рефлексивно, каждый элемент S связан отношением R с самим собой — то есть, для всех s ∈ S, s R s (или (s,s) ∈ R). Отношение R симметрично, если для всех s,t ∈ S из s R t следует t R s. Отношение R транзитивно, если из s R t и t R u следует s R u. Отношение R антисимметрично, если из s R t и t R s следует s=t.

Определение 2 Рефлексивное и транзитивное отношение R на множестве S называется предпорядком на S. (Всякий раз, когда мы говорим о <<предупорядоченном множестве S>>, мы имеем в виду какой-то конкретный предпорядок на S.) Предпорядки обычно обозначаются символами ≤ или ⊑. Запись s < t значит s ≤ t ∧ s ≠ t.

Если предпорядок (на S) антисимметричен, то он называется частичным порядком на S. Частичный порядок ≤ называется линейным порядком на S, если для любых s,t ∈ S выполняется либо s ≤ t, либо t ≤ s.

Определение 3 Пусть ≤ — частичный порядок на S, а s и t — элементы S. Элемент j ∈ S называется объединением (или точной верхней гранью) s и t, если

s ≤ j и t ≤ j, а также
для всякого k ∈ S, если s ≤ k и t ≤ k, то j ≤ k.

Подобным образом, элемент m ∈ S называется пересечением (или точной нижней гранью) s и t, если

m ≤ s и m ≤ t, а также
для всякого n ∈ S, если n ≤ s и n ≤ t, то n ≤ m.

Определение 4 Рефлексивное, симметричное и транзитивное отношение на множестве S называется отношением эквивалентности на S.

Определение 5 Пусть R — бинарное отношение на множестве S. Рефлексивное замыкание R — это наименьшее рефлексивное отношение R′, содержащее в себе R. (<<Наименьшее>> здесь означает, что, если имеется какое-то другое рефлексивное отношение R″, включающее все пары из R, то R′ ⊆ R″.) Подобным образом, транзитивное замыкание R — это наименьшее транзитивное отношение R′, содержащее R. Часто транзитивное замыкание R обозначается R⁺. Рефлексивно-транзитивное замыкание R — это наименьшее рефлексивное и транзитивное отношение, содержащее R. Часто оно обозначается R^*.

Упражнение 6 [★★ ¬→] Предположим, нам дано отношение R на множестве S. Определим отношение R′ так:

R′ = R ⋃ { (s,s) | s ∈ S }

То есть, R′ содержит все пары из R плюс все пары вида (s,s). Покажите, что R′ является рефлексивным замыканием R.

Упражнение 7 [★★ ¬→] Вот более конструктивный способ определить транзитивное замыкание отношения R. Сначала мы определяем следующую последовательность множеств пар:

R₀	=	R
R_i+1	=	R_i ⋃ { (s,u) \| для какого-либо t, (s,t) ∈ R_i и (t,u) ∈ R_i}

То есть, на каждом шаге i+1 мы добавляем к R_i все пары, которые можно получить <<за один шаг транзитивности>> из пар, входящих в R_i. Наконец, определим отношение R⁺ как объединение всех R_i:

R⁺ =

∪

R_i

Покажите, что R⁺ на самом деле является транзитивным замыканием R — т. е., что оно удовлетворяет условиям, заданным в Определении 5

Упражнение 8 [★★ ¬→] Пусть R — бинарное отношение на множестве S, и это отношение сохраняет предикат P. Докажите, что R^* также сохраняет P.

Определение 9 Пусть у нас есть предпорядок ≤ на множестве S. Убывающая цепочка на ≤ есть последовательность s₁, s₂, s₃, … элементов S, такая, что каждый элемент последовательности строго меньше предшествующего: s_i+1 < s_i для всякого i. (Цепочки могут быть конечными или бесконечными, однако для нас представляют больший интерес бесконечные, как видно из следующего определения.)

Определение 10 Пусть у нас есть множество S с предпорядком ≤. ≤ называется полным, если он не содержит бесконечных убывающих цепочек. Например, обычный порядок на натуральных числах, 0 < 1 < 2 < 3 < …, является полным, а тот же самый порядок на целых числах, … < −3 < −2 < −1 < 0 < 1 < 2 < 3 < … — нет. Иногда мы не упоминаем ≤ явно и просто называем S вполне упорядоченным множеством.

2.3 Последовательности

Определение 1 Последовательность записывается путем перечисления элементов через запятую. Запятая используется как для добавления элемента к последовательности в начало (вроде лисповского cons) или конец, так и для склеивания двух последовательностей (вроде лисповского append). Например, если символ a обозначает последовательность 3,2,1, символ b обозначает последовательность 5,6, то 0,a — это последовательность 0,3,2,1, запись a,0 обозначает последовательность 3,2,1,0, а запись b,a обозначает 5,6,2,3,1. (Использование запятой для двух разных операций — аналогов cons и append, — не создает путаницы, если нам не нужно вести речь о последовательностях последовательностей.) Последовательность чисел от 1 до n обозначается 1..n (через две точки). Запись |a| означает длину последовательности a. Пустая последовательность обозначается знаком • или пробелом. Одна последовательность называется перестановкой другой, если они содержат одни и те же элементы, возможно, в разном порядке.

2.4 Индукция

Доказательства по индукции встречаются в теории языков программирования очень часто, как и в большинстве разделов информатики. Многие из этих доказательств основаны на одном из следуюших принципов:

Аксиома 1 [Принцип обыкновенной индукции на натуральных числах] Пусть P — предикат, заданный на множестве натуральных чисел. Тогда

Если P(0)
и для любого i, из P(i) следует P(i+1),
то P(n) выполняется для всех n.

Аксиома 2 [Принцип полной индукции на натуральных числах] Пусть P — предикат от натуральных чисел. Тогда

Если для каждого натурального числа n,
предполагая P(i) для всех i<n,
мы можем показать P(n),
то P(n) выполняется для всех n.

Определение 3 Лексикографический (или <<словарный>>) порядок на парах натуральных чисел определяется следующим образом: (m,n) ≤ (m′,n′) тогда и только тогда, когда либо m < m′, либо m=m′ и n ≤ n′.

Аксиома 4 [Принцип лексикографической индукции] Пусть P — предикат от пар натуральных чисел. Тогда

Если для каждой пары натуральных чисел (m,n),
предполагая P(m′,n′) для всех (m′,n′) < (m,n),
мы можем показать P(m,n),
то P(m,n) выполняется для всех m,n.

Принцип лексикографической индукции служит основой для доказательств со вложенной индукцией, где какой-либо пункт индуктивного доказательства использует индукцию <<внутри себя>>. Этот принцип можно распространить на индукцию по тройкам, четверкам и т. д. (Индукция по парам нужна достаточно часто; по тройкам она иногда оказывается полезной; по четверкам и далее почти не встречается.)

В Теореме 4 вводится еще один вариант доказательств по индукции, называемый структурная индукция. Он особенно хорош, когда доказываются утверждения о древовидных структурах вроде термов или деревьях вывода типов. Математические основания индуктивных рассуждений будут более подробно рассмотрены в Главе 21. Мы увидим, что все упомянутые принципы индукции являются частными проявлениями единой более общей идеи.

2.5 Справочная литература

Если понятия, перечисленные в этой главе, оказались для Вас незнакомыми, вероятно, имеет смысл ознакомиться со справочной литературой. Существует множество вводных курсов. В частности, книга Винскела (Winskel 1993) помогает развить интуицию в вопросах индукции. Начальные главы в книге Дейви и Пристли (Davey and Priestley 1990) содержат замечательный обзор по упорядоченным множествам. Хэлмос (Halmos 1987) служит хорошим введением в базовую теорию множеств.

Доказательство — это воспроизводимый опыт в деле убеждения.Джим Хорнинг

Chapter 3 Бестиповые арифметические выражения

Чтобы вести подробный разговор о системах типов и их свойствах, нам для начала нужно научиться формальным образом работать с некоторыми более простыми характеристиками языков программирования. В частности, требуются четкие, ясные и математически точные механизмы, чтобы описывать синтаксис и семантику программ и строить о них рассуждения.

В этой и следующей главе мы разрабатываем такие механизмы для маленького языка, работающего с числами и логическими значениями. Сам язык настолько прост, что почти не стоит рассмотрения, однако с его помощью мы вводим некоторые базовые понятия — абстрактный синтаксис, индуктивные определения и доказательства, вычисление и моделирование ошибок времени выполнения. В главах с 5 по 7 те же самые шаги проделываются для намного более мощного языка — бестипового лямбда-исчисления. Кроме того, там нам приходится иметь дело со связыванием имен и подстановками. Далее, в Главе 8, мы начинаем собственно изучение типов, возвращаясь к простому языку из этой главы и с его помощью вводя основные понятия статической типизации. В Главе 9 эти понятия распространяются на лямбда-исчисление.

3.1 Введение

В языке этой главы имеется лишь несколько синтаксических конструкций: булевские константы true (истина) и false (ложь), условные выражения, числовая константа 0, арифметические операции succ (следующее число) и pred (предыдущее число) и операция-тест iszero, которая возвращает true, будучи применена к 0, и false, когда применяется к любому другому числу. Эти конструкции можно компактно описать следующей грамматикой.

Правила, которыми мы пользуемся при записи этой грамматики (и при записи грамматик на протяжении всей этой книги) близки к стандартной форме Бэкуса-Наура (см. Aho, Sethi and Ullman, 1986). В первой строке (t ::=) объявляется, что мы определяем множество термов, и что мы будем употреблять букву t для обозначения произвольного терма. Всюду, где встречается символ t, можно подставить любой терм. Курсив справа — просто комментарии.

Символ t в правых частях правил грамматики называется метапеременной. Это переменная в том смысле, что t служит в качестве заместителя какого-нибудь конкретного терма, но это <<мета>>-переменная, поскольку она является переменной не объектного языка — простого языка программирования, чей синтаксис мы сейчас описываем, — а метаязыка, — знаковой системы, которая служит для описания. (На самом деле, в нашем теперешнем объектном языке даже нет переменных; мы их введем в Главе 5.) Приставка meta- происходит из мета-математики, отрасли логики, которая изучает математические свойства систем, предназначенных для математических и логических рассуждений (в частности, языков программирования). Оттуда же происходит термин метатеория; он означает совокупность истинных утверждений, которые мы можем сделать о какой-либо логической системе (или о языке программирования), а в расширенном смысле — исследование таких утверждений. Таким образом, выражения вроде <<метатеория наследования>> в этой книге могут пониматься как <<формальное исследование свойств систем с наследованием>>.

На протяжнии этой книги мы будем использовать метапеременную t, а также близкие к ней буквы, скажем, s, u и r, и варианты вроде t₁ или s′, для термов объектного языка, которым мы занимаемся в данный момент; далее будут введены и другие буквы для обозначения выражений других синтаксических категорий. Полный список соглашений по использованию метапеременных можно найти в Приложении B.

Пока что слова терм и выражение обозначают одно и то же. Начиная с Главы 8, когда мы станем изучать исчисления, обладающие более богатым набором синтаксических категорий (таких, как типы), словом выражение мы будем называть любые синтаксические объекты (в том числе выражения-термы, выражения-типы, выражения-виды и т. п.), а терм будет употребляться в более узком смысле, для конструкций, которые обозначают вычисления (т. е., выражения, которые можно подставить вместо метапеременной t).

Программа на нашем нынешнем языке — это всего лишь терм, построенный при помощи перечисленных выше конструкций. Вот несколько примеров программ, вместе с результатами их вычисления. Для краткости мы используем стандартные арабские цифры для записи чисел, которые формально представляются как набор вложенных применений операции succ к 0. Например, succ(succ(succ(0))) записывается как 3.

Символом |> на протяжении всей книги обозначаются результаты вычисления примеров. (Для краткости результаты опускаются, когда они очевидны или не играют никакой роли.) При верстке результаты автоматически вставляются реализацией системы, которая в данный момент рассматривается (в этой главе arith); напечатанные результаты представляют собой настоящий вывод системы.¹

Составные аргументы succ, pred и iszero в примерах приведены, для удобства чтения, в скобках.¹ Скобки не упоминаются в грамматике термов; она определяет только абстрактный синтаксис. Разумеется, присутствие скобок или их отсутствие играет весьма малую роль в чрезвычайно простом языке, с которым мы сейчас имеем дело: обычно скобки служат для разрешения неоднозначностей в грамматике, но в нашей грамматике неоднозначностей нет — любая последовательность символов может быть разобрана максимум одним способом. Мы вернемся к обсуждению абстрактного синтаксиса и скобок в Главе 5 (стр. ??).

Результатом вычислений служат термы некоторого простого вида: это всегда будут либо булевские константы, либо числа (вложенные вызовы succ ноль или более раз с аргументом 0). Такие термы называются значениями, и они будут играть особую роль при формализации порядка вычисления термов.

Заметим, что синтаксис термов позволяет образовывать термы сомнительного вида, вроде succ true или if 0 then 0 else 0. Мы поговорим о таких термах позднее — в сущности, именно их наличие делает этот крошечный язык интересным для наших целей, поскольку они являются примерами таких бессмысленных программ, которых мы хотим избегать при помощи системы типов.

3.2 Синтаксис

Есть несколько эквивалентных способов определить синтаксис нашего языка. Один из них мы уже видели — это грамматика на странице ??. Грамматика эта, в сущности, всего лишь сокращенная форма записи следующего индуктивного определения:

Определение 1 [Термы, индуктивно]: Множество термов — это наименьшее множество T такое, что:

{true, false, 0} ⊆ T;
если t₁ ∈ T, то { succ t₁, pred t₁, iszero t₁} ⊆ T;
если t₁ ∈ T, t₂ ∈ T, t₃ ∈ T, то if t₁ then t₂ else t₃ ∈ T.

Такие индуктивные определения чрезвычайно часто встречаются при исследовании языков программирования, так что имеет смысл остановиться и рассмотреть наше определение более подробно. Первый пункт говорит нам, какие простые выражения содержатся в T. Второй и третий пункты указывают правила, с помощью которых мы можем определять, что некоторые сложные выражения также содержатся в T. Наконец, слово <<наименьшее>> говорит, что в T нет никаких элементов, кроме требуемых этими тремя пунктами.

Подобно грамматике на странице ??, это определение ничего не говорит об использовании скобок для выделения составных подтермов. С формальной точки зрения, мы определяем T как множество деревьев, а не множество строк. Скобки в примерах используются для того, чтобы показать, как линейная форма термов, которую мы записываем на бумаге, соотносится с внутренней древовидной формой.

Еще один способ представить то же индуктивное определение термов использует двумерную запись в виде правил вывода, обычную для логических систем в форме <<естественного вывода>>:

Определение 2 [Термы, через правила вывода]: Множество термов определяется следующими правилами:

true ∈ T

false ∈ T

0 ∈ T

t₁ ∈ T

succ t₁ ∈ T

t₁ ∈ T

pred t₁ ∈ T

t₁ ∈ T

iszero t₁ ∈ T

t₁ ∈ T t₂ ∈ T t₃ ∈ T

if t₁ then t₂ else t₃ ∈ T

Первые три правила повторяют первый пункт Определения 1; остальные четыре соответствуют пунктам (2) и (3). Каждое правило вывода читается так: <<Если мы установили истинность предпосылок, указанных над чертой, то мы можем вывести заключение под чертой>>. Утверждение, что T является наименьшим множеством, удовлетворяющим этим правилам, часто опускается (как это сделано и здесь).

Стоит упомянуть две терминологические детали. Во-первых, правила без предпосылок (как первые три в нашем определении) часто называют аксиомами. В этой книге термин правило вывода используется как для <<собственно правил вывода>>, где имеется одна или несколько предпосылок, так и для аксиом. Аксиомы обычно записываются без черты, поскольку над ней нечего писать. Во-вторых, если выражаться абсолютно точно, наши <<правила вывода>> на самом деле представляют собой схемы правил, поскольку предпосылки и заключения в них могут содержать метапеременные. С формальной точки зрения, каждая схема представляет бесконечное множество конкретных правил, получаемых путем замены каждой метапеременной различными выражениями, принадлежащими соответствующей синтаксической категории — т. е., в данном случае, вместо каждого t подставляются все возможные термы.

Наконец, то же самое множество термов можно определить и еще немного по-другому, в более <<конкретном>> стиле, явно указав процедуру порождения элементов T.

Определение 3 [Термы, конкретным образом]: Для каждого натурального числа i определяем множество S_i:

S₀ = ∅

S_i+1

	{`true`, `false`, `0`}
⋃	{`succ t`₁, `pred t`₁, `iszero t`₁ \| `t`₁ ∈ S_i}
⋃	{`if t`₁ `then t`₂ `else t`₃ \| `t`₁, `t`₂, `t`₃ ∈ S_i}.

Наконец, пусть

S =

∪

S_i.

S₀ пусто; S₁ содержит только константы; S₂ содержит константы и выражения, которые можно построить из констант путем применения одной из конструкций succ, pred, iszero или if; S₃ содержит все эти выражения плюс те, которые можно построить за одно применение succ, pred, iszero или if к членам S₂; и так далее. S собирает все эти выражения вместе — т. е., все выражения, которые можно получить применением конечного числа арифметических и условных операторов, начиная с констант.

Упражнение 4 [★★]: Сколько элементов содержит S₃?

Упражнение 5 [★★]: Покажите, что множества S_i кумулятивны — то есть, для любого i выполняется S_i ⊆ S_i+1.

Рассмотренные нами определения характеризуют одно и то же множество термов с разных направлений: Определения 1 и 2 просто описывают множество как наименьшее, имеющее некоторые <<свойства замыкания>>; Определение 3 показывает, как построить множество в виде предела последовательности.

Заврешая наше обсуждение, давайте покажем, что эти две точки зрения определяют одно и то же множество. Мы записываем доказательство во всех подробностях, чтобы продемонстрировать, как различные его части соотносятся друг с другом.

Утверждение 6 T = S.
Доказательство: T определяется как наименьшее множество, удовлетворяющее некоторым условиям. Таким образом, достаточно показать, что (а) эти условия выполняются на S; и (б) что любое множество, удовлетворяющее условиям, содержит S как подмножество (т. е, что S — наименьшее множество, удовлетворяющее условиям).

В части (а) нам требуется проверить, что все три условия из Определения 1 выполняются на S. Во-первых, поскольку S₁ = {true, false, 0}, ясно, что S содержит константы. Во-вторых, если t₁ ∈ S, то, поскольку S = ∪_i S_i, должно иметься какое-то i, такое, что t₁ ∈ S_i. Но тогда, по определению S_i+1, мы имеем succ t₁ ∈ S_i+1, а следовательно, succ t₁ ∈ S; подобным образом, pred t₁ ∈ S и iszero t₁ ∈ S. В-третьих, при помощи аналогичного рассуждения, если t₁ ∈ S, t₂ ∈ S, и t₃ ∈ S, то if t₁ then t₂else t₃ ∈ S.

Для части (б) предположим что некоторое множество S′ удовлетворяет всем трем условиям из Определения 1. При помощи полной индукции по i мы докажем, что все S_i ⊆ S′, откуда следует, что S ⊆ S′.

Допустим, что S_j ⊆ S′ для всех j < i; мы должны показать, что S_i ⊆ S′. Поскольку определение S_i состоит из двух пунктов (для i=0 и i > 0), требуется рассмотреть два случая. Если i=0, то S_i = ∅; тогда, тривиальным образом, ∅ ⊆ S′. В противном случае, i = j+1 для некоторого j. Пусть t будет некоторым элементом S_j+1. Поскольку S_j+1 определяется как объединение трех меньших множеств, требуется рассмотреть три возможных случая. (1) Если t — константа, то t ∈ S′ по условию 1. (2) Если t имеет вид succ t₁, pred t₁ или iszero t₁, для некоторого t₁ ∈ S_j, то, по предположению индукции, t₁ ∈ S′, и тогда, по условию 2, t ∈ S′. (3) Если t имеет вид if t₁ then t₂ else t₃ для некоторых t₁, t₂, t₃ ∈ S_j, то, опять же, согласно предположению индукции, t₁, t₂ и t₃ все содержатся в S′, и, по условию 3, в нем содержится и t.

Таким образом, мы показали, что все S_i ⊆ S′. Поскольку S определено как объединение всех S_i, мы имеем S ⊆ S′, и наше доказательство закончено.

Стоит заметить, что доказательство использует полную индукцию по всем натуральным числам, а не более привычный образец <<базовый случай / шаг индукции>>. Для каждого i мы предполагаем, что нужное условие выполняется для всех чисел строго меньше i, и доказываем, что и для i оно тоже выполняется. В сущности, каждый шаг здесь является шагом индукции; единственное, что выделяет случай i=0 – это то, что множество чисел, меньших, чем i, для которых мы можем использовать индуктивное предположение, оказывается пустым. То же соображение будет относиться к большинству индуктивных доказательств на всем протяжении этой книги — особенно к доказательствам по <<структурной индукции>>.

3.3 Индукция на термах

Явная характеризация множества термов T в Утверждении 6 позволяет нам сформулировать важную стратегию для исследования его элементов. Если t ∈ T, то истинно одно из следующих утверждений: (1) t является константой, либо (2) t имеет вид succ t₁, pred t₁ или iszero t₁, причем t₁ по размеру меньше, чем t, либо, наконец (3) t имеет вид if t₁then t₂ else t₃, причем t₁, t₂ и t₃ меньше, чем t. Это наблюдение можно использовать двумя способами: Во-первых, мы можем строить индуктивные определения функций, действующих на множестве термов, и, во-вторых, мы можем давать индуктивные доказательства свойств термов. Например, вот индуктивное определение функции, которая каждому терму ставит в соответствие множество констант, в нем использованных.

Определение 1 Множество констант, встречающихся в терме t (записывается Consts(t)), определяется так:

Consts(`true`)	=	{`true`}
Consts(`false`)	=	{`false`}
Consts(`0`)	=	{`0`}
Consts(`succ t`₁)	=	Consts(`t`₁)
Consts(`pred t`₁)	=	Consts(`t`₁)
Consts(`iszero t`₁)	=	Consts(`t`₁)
Consts(`if t`₁ `then t`₂ `else t`₃)	=	Consts(`t`₁) ⋃ Consts(`t`₂) ⋃ Consts (`t`₃)

Еще одна характеристика терма, которую можно вычислить при помощи индуктивного определения — его размер.

Определение 2 Размер термa t, записываемый size(t), определяется так:

size(`true`)	=	1
size(`false`)	=	1
size(`0`)	=	1
size(`succ t`₁)	=	size(`t`₁) + 1
size(`pred t`₁)	=	size(`t`₁) + 1
size(`iszero t`₁)	=	size(`t`₁) + 1
size(`if t`₁ `then t`₂ `else t`₃)	=	size(`t`₁) + size(`t`₂) + size(`t`₃) +1

Таким образом, размер t — это число вершин в его абстрактном синтаксическом дереве. Подобным образом, глубина терма t, записываемая depth(t), определяется так:

depth(`true`)	=	1
depth(`false`)	=	1
depth(`0`)	=	1
depth(`succ t`₁)	=	depth(`t`₁) + 1
depth(`pred t`₁)	=	depth(`t`₁) + 1
depth(`iszero t`₁)	=	depth(`t`₁) + 1
depth(`if t`₁ `then t`₂ `else t`₃)	=	max(depth(`t`₁), depth(`t`₂), depth(`t`₃)) + 1

Другое, эквивалентное, определение, таково: depth(t) — это наименьшее такое i, что t ∈ S_i согласно Определению 1.

Вот пример индуктивного доказательства, связывающего число констант в терме с его размером. (Само свойство, разумеется, совершенно очевидно. Интерес представляет форма индуктивного рассуждения. Мы ее еще неоднократно встретим.)

Лемма 3 Число различных констант в терме t не больше его размера (т. е., |Consts(t)| ≤ size(t)).
Доказательство: индукция по глубине терма t. Мы предполагаем, что свойство выполняется для всех термов, меньших t, и должны доказать его по отношению к самому t. Требуется рассмотреть три варианта:
Вариант: t – константа.
Свойство выполняется непосредственно: |Consts(t)| = |{t}| = 1 = size(t).
Вариант: t = succ t₁, pred t₁ или iszero t₁
Согласно индуктивному предположению, |Consts(t₁)| ≤ size(t₁). Рассуждаем так: |Consts(t)| = |Consts(t₁)| ≤ size(t₁) < size(t).
Вариант: t = if t₁ then t₂else t₃
Согласно индуктивному предположению, |Consts(t₁)| ≤ size(t₁), |Consts(t₂)| ≤ size(t₂), |Consts(t₃)| ≤ size(t₃). Рассуждаем так:

\|Consts(`t`)\|	=	\|Consts(`t`₁) ⋃ Consts(`t`₂) ⋃ Consts(`t`₃) \|
	≤	\|Consts(`t`₁)\| + \|Consts(`t`₂)\| + \|Consts(`t`₃)\|
	≤	size(`t`₁) + size(`t`₂) + size(`t`₃)
	<	size (`t`)

Принцип, лежащий в основе этого доказательства, можно сформулировать в общем виде. Для полноты мы добавляем еще два подобных принципа, часто используемых в доказательствах утверждений о термах.

Теорема 4 [Принципы индукции по термам] Пусть P — предикат, определенный на множестве термов.

Индукция по глубине:
Если для каждого терма s,
предполагая P(r) для всех r, таких, что depth(r) < depth(s),
мы можем доказать P(s),
то P(s) выполняется для всех s.

Индукция по размеру:
Если для каждого терма s,
предполагая P(r) для всех r, таких, что size(r) < size(s),
мы можем доказать P(s),
то P(s) выполняется для всех s.

Структурная индукция:
Если для каждого терма s,
предполагая P(r) для всех непосредственных подтермов s, мы можем доказать P(s),
то P(s) выполняется для всех s.

Доказательство: Упражнение (★★).

Индукция по глубине или размеру термов аналогична полной индукции на натуральных числах (2). Обыкновенная структурная индукция соответствует принципу обыкновенной индукции на натуральных числах (1), где шаг индукции требует, чтобы P(n+1) выводилось исключительно из предположения P(n).

Подобно различным видам индукции на натуральных числах, выбор конкретного принципа индукции диктуется тем, какой из них приводит к более простой структуре конкретного доказательства — с формальной точки зрения, они равносильны. В простых доказательствах обычно неважно, проводим мы индукцию по глубине, размеру или структуре. С точки зрения стиля, как правило, по возможности предпочитают структурную индукцию, поскольку в таком случае работа ведется прямо с термами, без промежуточного обращения к числам.

Большинство доказательств по индукции на термах имеет одну и ту же структуру. На каждом шаге индукции нам дается терм t, для которого нам нужно продемонстрировать некоторое свойство P, в предположении, что P выполняется на всех его подтермах (или на всех термах меньшего размера). Мы делаем это путем рассмотрения всех возможных форм, которые t может иметь (true, false, 0, условное выражение и т. п.), в каждом случае доказывая, что P должно выполняться на всех термах этого вида. Поскольку единственные фрагменты структуры, которые меняются от одного доказательства к другому, — это детали рассуждений в конкретных случаях, принято опускать повторяющиеся части доказательств, и записывать их таким образом:

Во многих индуктивных доказательствах (включая 3) даже такой уровень подробности чрезмерен: в базовых случаях (для термов t, не имеющих подтермов) P(t) ясно непосредственно, а в индуктивных случаях P(t) выводится путем применения индуктивного предположения к подтермам t и сочетания результатов некоторым очевидным способом. Для читателя оказывается проще воссоздать доказательство на ходу (перебирая правила грамматики и держа в уме индуктивное предположение), чем прочитать явно записанные шаги. В таких ситуациях запись <<индукция по t>> в качестве доказательства более чем приемлема.

3.4 Семантические стили

Сформулировав с математической точностью синтаксис нашего языка, мы должны теперь дать столь же строгое определение тому, как вычисляются термы — т. е., семантике нашего языка. Существует три основных подхода к формализации семантики:

В 60-е и 70-е годы считалось, что операционная семантика уступает двум другим стилям, что с ее помощью можно быстро и без особого труда определить какие-то характеристики языка, но в целом она менее изящна и слаба с математической точки зрения. Однако в 80-е годы более абстрактные методы стали сталкиваться со все более неприятными техническими сложностями,³ и простота и гибкость операционной семантики стали по сравнению с ними выглядеть все более привлекательными — особенно в свете новых достижений, начиная со Структурной Операционной Семантики Плоткина (Plotkin 1981), Естественной Семантики Кана (Kahn 1987) и работ Милнера по Исчислению Взаимодействующих Систем (Calculus of Communicating Systems, CCS; Milner 1980, 1989, 1999). Эти работы ввели в обращение более изящные, чем ранее, формализмы, и показали, как многие мощные методы, изначально разработанные в рамках денотационной семантики, могут быть перенесены на операционную почву. Операционная семантика стала быстроразвивающейся дисциплиной и часто выбирается в качестве средства для определения языков программирования и изучения их свойств. Именно она используется в этой книге.

3.5 Вычисление

Забудем на время о натуральных числах и рассмотрим операционную семантику только булевских выражений. Определение приведено на Рис. 3.1. Рассмотрим его в деталях.

В левом столбце Рис. 3.1 содержится грамматика, в которой определяются два вида выражений. Во-первых, повторяется (для удобства) синтаксис термов. Во-вторых, определяется подмножество термов — множество значений, возможных результатов вычисления. В нашем случае значениями являются только константы true и false. На протяжении всей книги для значений используется метапеременная v.

В правом столбце определяется отношение вычисления⁴ на термах. Оно записывается t → t′ и читается <<t переходит в t′ за один шаг вычисления>>. Интуитивно, если в какой-то момент абстрактная машина находится в состоянии t, то она может произвести шаг вычисления и перейти в состояние t′. Это отношение определяется тремя правилами вывода (или, если хотите, двумя аксиомами и одним правилом: первые два правила не имеют предпосылок).

Первое правило, E-IfTrue, говорит, что, если вычисляется условное выражение, где условием служит константа true, то машина может выкинуть это условное выражение, оставив истинную ветвь t₂ в качестве состояния (т. е., следующего подлежащего вычислению терма). Подобным образом, E-IfFalse говорит, что условное выражение с константой false в качестве условия переходит за один шаг в свою ложную ветвь t₃. Символ E- в названиях этих правил напоминает, что они являются частью отношения вычисления; у правил, определяющих другие отношения, будут в названиях другие префиксы.

Третье правило вычисления, E-If, представляет больше интереса. Оно говорит, что, если условие t₁ переходит за шаг в t′₁, то условное выражение if t₁then t₂ else t₃ целиком переходит за шаг в if t′₁then t₂ else t₃. Рассуждая в терминах абстрактных машин, машина, чье состояние выглядит как if t₁then t₂ else t₃, может за шаг перейти в состояние if t′₁then t₂ else t₃ тогда и только тогда, когда другая машина, чье состояние выглядит просто как t₁, может за шаг перейти в t′₁.

Не менее важно, чем то, что эти правила говорят, то чего они не говорят. Константы true и false ни во что не переходят, поскольку они не присутствуют в левой части никакого правила. Более того, не существует правила, которое бы позволило вычислять истинную или ложную ветвь if-выражения, пока не вычислено условие: например, терм

не переходит в if true then false else true. Единственный разрешенный нам шаг — вычислить сначала внешнее условное выражение, используя E-IfTrue. Такое взаимодействие между правилами определяет конкретную стратегию вычисления для условных выражений, соответствующую привычному порядку вычислений в большинстве языков программирования: чтобы вычислить условное выражение, нужно вычислить его условие; если условие само является условным выражением, требуется вычислить его условие; и так далее. Правила E-IfTrue и E-IfFalse говорят нам, что нужно делать, когда мы достигаем конца этого процесса и обнаруживаем условное выражение, чье условие уже полностью вычислено. В некотором смысле, E-IfTrue и E-IfFalse проделывают работу по вычислению, в то время как E-If помогает определить, где эта работа должна выполняться. Иногда различный характер этих правил подчеркивают, называя E-IfTrue и E-IfFalse рабочими правилами, в то время как E-If является правилом соответствия.

Для того, чтобы выразить нашу интуицию более точно, можно формально определить отношение вычисления так:

Определение 1 Экземпляр правила вывода получается при замене каждой метапеременной одним и тем же термом в заключении правила и во всех его предпосылках (если они есть).

является экземпляром правила E-IfTrue, где оба вхождения t₂ заменяются на true, а t₃ заменяется на if false then false else false.

Определение 2 Правило выполняется на бинарном отношении между термами, если, для каждого экземпляра правила, либо заключение является членом отношения, либо хотя бы одна предпосылка не является.

Определение 3 Одношаговое отношение вычисления есть наименьшее бинарное отношение на термах, на котором выполняются все три правила с Рис. 3.1. Если пара (t, t′) является членом этого отношения, мы говорим, что утверждение (или суждение) о вычислении t → t′ выводимо.

Значение слова <<наименьшее>> в этом определении таково: утверждение t → t′ выводимо тогда и только тогда, когда оно обеспечено правилами: либо это экземпляр одной из аксиом E-IfTrue или E-IfFalse, либо это заключение экземпляра правила E-If с выводимой предпосылкой. Выводимость утверждения можно обосновать через дерево вывода, где листьями служат экземпляры правил E-IfTrue и E-IfFalse, а внутренними вершинами экземпляры правила E-If. Например, если мы введем сокращения

(чтобы вывод помещался на странице), то выводимость утверждения

Может показаться, что странно называть такую структуру деревом; в ней нет никакого ветвления. Действительно, деревья вывода, обосновывающие утверждения о вычислении, всегда будут иметь такую вырожденную форму: поскольку в правилях вычисления всегда не более одной предпосылки, ветвлению в дереве вывода взяться неоткуда. Наша терминология окажется более осмысленной, когда рассмотрение дойдет до других индуктивно определенных отношений, например, типизации — там некоторые правила могут иметь более одной предпосылки.

То, что утверждение о вычислении t → t′ выводимо тогда и только тогда, когда существует дерево вывода с t → t′ в корне, часто оказывается полезным при исследовании свойств отношения вычисления. В частности, это немедленно подсказывает метод доказательства, называемый индукция по выводам. Доказательство следующей теоремы может служить иллюстрацией.

Теорема 4 [Детерминированность одношагового вычисления] Если t → t′ и t → t″, то t′ = t″.
Доказательство: Индукция по выводу t → t′. На каждом шаге индукции мы предполагаем теорему доказанной для всех меньших деревьев вывода, и анализируем правило вычисления, находящееся в корне дерева. (Заметим, что индукция здесь не идет по длине цепочки вычисления: мы смотрим только на один ее шаг. С тем же успехом можно было бы сказать, что индукция проводится по структуре t, поскольку структура <<вывода шага вычисления>> прямо следует структуре редуцируемого терма. Кроме того, мы могли бы точно так же провести индукцию по выводу t → t″.)

Если последний шаг, использованный в выводе t → t′, является экземпляром правила E-IfTrue, то ясно, что t имеет вид if t₁ then t₂else t₃, причем t₁ = true. Но тогда понятно, что последний шаг в выводе t → t″ не может быть E-IfFalse, поскольку невозможно, чтобы одновременно было t₁ = true и t₁ = false. Более того, последнее правило во втором дереве вывода не может быть и E-If, потому что предпосылка этого правила требует t₁ → t′₁ для какого-нибудь t′₁, однако, как мы уже заметили, true не может ни во что перейти. Таким образом, последним правилом во втором дереве вывода может быть только E-IfTrue, откуда немедленно следует t′ = t″.

Точно так же, если последнее правило при выводе t → t′ — экземпляр E-IfFalse, таково же должно быть и последнее правило при выводе t → t″, и нужный результат, опять же, следует непосредственно.

Наконец, если последним при выводе t → t′ применяется E-If, то из формы этого правила можно заключить, что t имеет вид if t₁then t₂ else t₃, причем для некоторого t′₁ выполняется t₁ → t′₁. При помощи таких же рассуждений, что и выше, мы можем заключить, что последним правилом в выводе t → t″ может быть только E-If, откуда ясно, что t имеет вид if t₁ then t₂ else t₃ (это нам уже и так известно), и что для некоторого t″₁ выполняется t₁ → t″₁. Но тогда мы можем применить предположение индукции (поскольку деревья вывода t₁ → t′₁ и t₁ → t″₁ являются поддеревьями выводов t → t′ и t → t″ соответственно) и заключить t′₁ = t″₁. Отсюда видно, что t′ = if t′₁ then t₂ else t₃ = if t″₁then t₂ else t₃ = t″, как нам и требуется.

Упражнение 5 [★] Сформулируйте, в стиле Теоремы 4, принцип индукции, используемый в приведенном выше доказательстве.

Наше одношаговое отношение вычисления показывает, как абстрактная машина переходит от одного состояния к другому при вычислении данного терма. Однако для нас, как для программистов, не меньший интерес представляют окончательные результаты вычисления — т. е. состояния, в которых машина не может сделать никаких дальнейших шагов.

Определение 6 Терм t находится в нормальной форме, если к нему не применимо никакое правило вычисления — т. е., если не существует такого t′, что t → t′. (В качестве сокращения мы иногда будем говорить <<t является нормальной формой>> вместо <<t является термом в нормальной форме>>.)

Мы уже заметили, что в нашей текущей системе true и false — нормальные формы (поскольку во всех правилах вычисления левые части являются условными выражениями, очевидно, невозможно построить экземпляр правила, где в качестве левой части выступала бы true или false). Можно обобщить это наблюдение как свойство всех значений:

Теорема 7 Всякое значение находится в нормальной форме.

Когда мы обогатим свою систему арифметическими выражениями, а в последующих главах и другими конструкциями, мы всегда будем следить, чтобы Теорема 7 оставалась истинной: быть в нормальной форме — часть самого понятия значения, и всякое определение языка, где это не так, безнадежно испорчено.

В нашей теперешней системе верно и обратное утверждение: всякая нормальная форма есть значение. В общем случае это будет не так; в частности, нормальные формы, не являющиеся значениями, будут играть важную роль при анализе ошибок времени выполнения, как мы увидим далее в этой главе при рассмотрении арифметических выражений.

Теорема 8 Если t находится в нормальной форме, то t — значение.
Доказательство: Предположим, что t не является значением. При помощи структурной индукции на t легко показать, что t — не нормальная форма.

Поскольку t не значение, он должен иметь вид if t₁ then t₂ else t₃ для некоторых t₁, t₂, t₃. Рассмотрим возможные формы t₁.

Если t₁ = true, то, очевидно, t не является нормальной формой, поскольку он подпадает под левую часть правила E-IfTrue. Так же и с t₁ = false.

Если t₁ не равен ни true, ни false, то он не является значением. В таком случае применимо предположение индукции, и оно говорит, что t₁ — не нормальная форма, а именно, что существует некий терм t′₁, такой, что t₁ → t′₁. Но тогда мы можем применить правило E-If, получая t → if t′₁ then t₂ else t₃. Таким образом, t не нормальная форма.

Иногда оказывается удобно рассматривать несколько шагов вычисления как один большой переход между состояниями. Для этого мы определяем отношение многошагового вычисления, которое сопоставляет данному терму все термы, получаемые из него за ноль или более шагов.

Определение 9 Отношение многошагового вычисления →^* — это рефлексивно-транзитивное замыкание отношения (одношагового) вычисления. То есть, это наименьшее отношение, такое, что (1) если t → t′, то t →^* t′, (2) для всех t выполняется t →^* t, и (3) если t →^* t′ и t′ →^* t″, то t →^* t″.

Упражнение 10 [★] Переформулируйте Определение 9 в виде набора правил вывода.

Наличие явного способа записи для многошагового вычисления облегчает формулировку утверждений вроде следующего:

Теорема 11 [Единственность нормальных форм] Если t →^* u и t →^* u’, причем и u, и u’ — нормальные формы, то u = u’.
Доказательство: Теорема следует из детерминированности одношагового вычисления (4).

Последнее свойство вычислений, которое мы рассмотрим, прежде чем обратиться к арифметическим выражениям, таково: каждый терм можно вычислить и получить значение. Понятно, что это еще одна характеристика, которой могут не обладать более богатые языки, где, например, могут быть рекурсивные определения функций. Даже в языках, где такое свойство есть, его доказательство обычно намного сложнее, чем, то, что мы увидим сейчас. В Главе 12 мы вернемся к этому вопросу и покажем, как система типов может служить хребтом доказательства гарантии завершения для некоторых языков.

Большинство доказательств гарантии завершения в информатике имеют одну и ту же базовую структуру.⁵ Сначала мы выбираем некоторое вполне упорядоченное множество S и функцию f, переводящую <<машинные состояния>> (в нашем случае — термы) в элементы S. Затем мы показываем, что всякий раз, когда машинное состояние t может перейти в другое состояние t′, выполняется неравенство f(t′) < f(t). Теперь мы можем заметить, что бесконечная цепочка шагов вычисления, начинающаяся с t, может быть переведена в бесконечную убывающую последовательность элементов S. Поскольку S вполне упорядочено, такая бесконечная убывающая цепочка существовать не может, а, соответственно, не может быть и бесконечной последовательности шагов вычисления. Функцию f часто называют мерой завершения отношения вычисления.

Теорема 12 [Завершение вычислений] Для каждого терма t существует нормальная форма t′, такая, что t →^* t′.
Доказательство: Достаточно заметить, что каждый шаг вычисления уменьшает размер терма, и что размер может служить мерой завершения, поскольку обычный порядок на натуральных числах является полным.

Упражнение 13 [Рекомендуется,★★]

Предположим, мы добавили к правилам на Рис. 3.1 еще одно:
if true then t₂ else t₃ → t₃ (E-Funny)

Какие из теорем 4, 7, 8, 11 и 12 остаются истинными?
Теперь допустим, что мы добавляем такое правило:
t₂ → t′₂ (E-Funny2)

if t₁ then t₂ else t₃ → if t₁ then t′₂ else t₃

Какие теоремы сохраняются в этом случае? Требуется ли модифицировать какие-либо доказательства?

Следующей нашей задачей будет расширить понятие вычисления на арифметические выражения. Рис. 3.2 демонстрирует новые компоненты определения. (Пометка в правом верхнем углу Рис. 3.2 напоминает, что определение расширяет 3.1, а не рассматривается независимо.)

Как и раньше, определение термов просто повторяет то, что мы уже видели в §3.1. Определение значений несколько интереснее, поскольку здесь приходится вводить новую категорию числовых значений. Интуиция такова: окончательным результатом вычисления арифметического выражения может быть число, и под числом понимается либо 0, либо значение-последователь числа (но не последователь произвольного значения: succ true должно считаться ошибкой, а не значением).

Правила вычисления в правом столбце Рис. 3.2 следуют той же схеме, что и на Рис. 3.1. Четыре рабочих правила (E-PredZero, E-PredSucc, E-IszeroZero и E-IszeroSucc) показывают, как операторы pred и iszero действуют на числовые значения, а три правила соответствия (E-Succ, E-Pred и E-IsZero) перенаправляют вычисление в <<первый>> подтерм составного терма.

Строго говоря, сейчас надо было бы повторить Определение 3 (<<одношаговое отношение вычисления на арифметических выражениях есть наименьшее отношение, удовлетворяющее всем экземплярам правил на Рис. 3.1 и 3.2…>>). Чтобы не тратить место на такого рода служебные определения, обычно считают, что правила вывода сами по себе представляют определение, а формулировка <<наименьшее отношение, содержащее все экземпляры…>> подразумевается.

В этих правилах важную роль играет синтаксическая категория числовых значений (nv). Например, в E-PredSucc требование, чтобы левая часть имела вид pred (succ nv₁), а не просто pred (succ t₁), приводит к тому, что это правило нельзя использовать для перевода pred (succ (pred 0)) в pred 0, поскольку для такого шага потребовалось бы заменить метапеременную nv₁ на терм pred 0, который не является числовым значением. В результате единственный разрешенный шаг при вычислении терма pred (succ (pred 0)) имеет дерево вывода

Упражнение 14 [★★] Покажите, что Теорема 4 верна и для отношения вычисления на арифметических выражениях: если t → t′ и t → t″, то t′ = t″.

Формализация операционной семантики языка заставляет нас указать поведение всех термов, включая, в нашем теперешнем языке, термы вроде pred 0 и succ false. По правилам Рис. 3.2, предшествующее число от 0 определяется как 0. С другой стороны, последователь false не вычисляется никак (другими словами, этот терм является нормальной формой). Такие термы мы называем тупиковыми.

Определение 15 Терм называется тупиковым, если он в нормальной форме, но не является значением.

Понятие <<тупика>> представляет ошибки времени выполнения в нашей простой машине. С интуитивной точки зрения, оно описывает ситуации, когда операционная семантика не знает, что делать дальше, поскольку программа оказалась в <<бессмысленном>> состоянии. В более конкретной реализации языка такие состояния могут соответствовать различного рода ошибкам: обращениям по несуществующему адресу, попыткам выполнить запрещенную машинную команду и т. п. Мы объединяем все эти виды неправильного поведения под единой вывеской <<тупикового состояния>>.

Упражнение 16 [Рекомендуется,★★★]
Другой способ формализовать бессмысленные состояния абстрактной машины состоит в том, чтобы ввести новый терм wrong (<<неправильное значение>>) и дополнить операционную семантику правилами, которые бы явным образом порождали wrong во всех ситуациях, которые в тепершней семантике приводят к тупику. А именно, мы вводим две новые синтаксические категории

`badnat`	::=	нечисловые нормальные формы
	`wrong`	ошибка времени выполнения
	`true`	константа <<истина>>
	`false`	константа <<ложь>>
`badbool`	::=	небулевские нормальные формы
	`wrong`	ошибка времени выполнения
	`nv`	числовое значение

и дополняем отношение вычисления следующими правилами:

`if badbool then t`₁ `else t`₂ → `wrong`	(E-If-Wrong)
`succ badnat` → `wrong`	(E-Succ-Wrong)
`pred badnat` → `wrong`	(E-Pred-Wrong)
`iszero badnat` → `wrong`	(E-IsZero-Wrong)

Покажите, что эти два подхода к формализации ошибок времени выполнения согласуются между собой. Для этого надо (1) найти способ точно выразить интуитивную идею, что <<два подхода согласуются>>, и (2) доказать это. Как это часто бывает при изучении языков программирования, сложность заключается в формулировании точного утверждения, подлежащего доказательству — само доказательство после этого построить нетрудно.

Упражнение 17 [Рекомендуется,★★★]
Существует два популярных стиля операционной семантики. В этой книге используется так называемая семантика с малым шагом, поскольку опеределение отношения вычисления показывает, как отдельные шаги вычисления используются для переписывания частей терма, кусочек за кусочком, пока в конце концов не получится значение. Поверх этого отношения мы определяем многошаговое отношение вычисления, которое позволяет нам говорить о том, как термы (за много шагов) вычисляются и дают значения. Альтернативный этому стиль, назывемый семантика с большим шагом (или, иногда, естественная семантика), прямо определяет понятие <<терм такой-то при вычислении дает такое-то значение>>, записываемое t ⇓ v. Правила с большим шагом для нашего языка с булевскими и арифметическими выражениями выглядят так:

v ⇓ v (B-Value)

t₁ ⇓ true t₂ ⇓ v₂

if t₁ then t₂ else t₃ ⇓ v₂

(B-IfTrue)

t₁ ⇓ false t₃ ⇓ v₃

if t₁ then t₂ else t₃ ⇓ v₃

(B-IfFalse)

t₁ ⇓ nv₁

succ t₁ ⇓ succ nv₁

(B-Succ)

t₁ ⇓ 0

pred t₁ ⇓ 0

(B-PredZero)

t₁ ⇓ succ nv₁

pred t₁ ⇓ nv₁

(B-PredSucc)

t₁ ⇓ 0

iszero t₁ ⇓ true

(B-IszeroTrue)

t₁ ⇓ succ nv₁

iszero t₁ ⇓ false

(B-IszeroFalse)

Покажите, что семантика с малым шагом и с большим шагом для нашего языка дают один и тот же результат, т. е., t →^* v тогда и только тогда, когда t ⇓ v.

Упражнение 18 [★★¬→]
Предположим, что нам захотелось поменять стратегию вычисления для нашего языка, так, чтобы ветви then и else в условном выражении вычислялись (в указанном порядке) до того, как вычислится само условие. Покажите, как нужно изменить правила вычисления, чтобы добиться такого поведения.

3.6 Дополнительные замечания

Понятия абстрактного и конкретного синтаксиса, синтаксического анализа и т. п. объясняются в большом количестве учебников по компиляторам. Индуктивные определения, системы правил вывода и доказательства по индукции рассмотрены более подробно в книгах Винскеля (Winskel 1993) и Хеннесси (Hennessy 1990).

Стиль операционной семантики, которым мы здесь пользуемся, восходит к техническому докладу Плоткина (Plotkin 1981). Стиль с большим шагом (17) был разработан Каном (Kahn 1987). Более подробно они описаны у Астезиано (Astesiano 1991) и у Хеннесси (Hennessy 1990).

Структурную индукцию ввел в информатику Берсталл (Burstall 1969).

В.: Зачем доказывать свойства языков программирования? Если в определениях нет ошибок, доказательства почти всегда получаются очень скучными.
О.: В определениях почти всегда есть ошибки. Автор неизвестен

Chapter 4 Реализация арифметических выражений на языке ML

¹ С формальными определениями, вроде тех, которые мы видели в предыдущей главе, работать часто проще, если интуиции, которые за ними стоят, <<укоренены>> в конкретной реализации. В этой главе мы описываем основные компоненты интерпретатора для нашего языка логических и арифметических выражений. (Те читатели, кто не хочет возиться с реализациями программ проверки типов, могут пропустить эту главу и все последующие, где в заглавии упоминается <<реализация на ML>>.)

Код, представленный здесь (и во всех программах в этой книге) написан на популярном языке из семейства ML (Gordon, Milner and Wadsworth 1979), называемом Objective Caml, или, сокращенно, OCaml (Leroy 2000; Cousineau and Mauny 1998). Используется лишь небольшое подмножество языка OCaml; все программы должно быть несложно перевести на большинство других языков. Основные требования к языку — автоматическое управление памятью (сборка мусора) и легкость определения рекурсивных функций через сопоставление с образцом на структурных типах данных. Другие функциональные языки, например, Стандартный ML (Milner, Tofte, Harper and MacQueen 1997), Haskell (Hudak et al. 1992; Thompson 1999) или Scheme (Kelsey, Clinger and Rees 1998; Dybvig 1996) (с каким-либо расширением для сопоставления с образцом) вполне удобны. Языки со сборкой мусора, но без сопоставления, например, Java (Arnold and Gosling 1996) или чистая Scheme, для наших задач несколько тяжеловаты. Языки, где нет ни того, ни другого, как в C (Kernighan and Ritchie 1998) подходят еще меньше.¹

4.1 Синтаксис

Сначала требуется определить OCaml-овский тип, представляющий термы. Механизм задания типов OCaml-а делает эту задачу простой: следующее объявление — прямой перевод грамматики со стр. ??.

Конструкторы от TmTrue до TmIsZero называют различные виды вершин в синтаксических деревьях типа term; тип, следующий за словом of, для каждого вида указывает количество поддеревьев, которые будут подчиняться вершине данного вида.

Каждая вершина абстрактного синтаксического дерева снабжена значением типа info, которое описывает место (номер символа и имя файла), откуда происходит эта вершина. Эта информация создается процедурой синтаксического анализа при чтении входного файла, и используется функциями распечатки, чтобы сообщать пользователю местонахождение ошибки. С точки зрения основных алгоритмов вычисления, проверки типов и т. п., эту информацию можно было бы и вовсе не хранить; она включена в листинги, чтобы читатели, которым захочется самим поэкспериментировать с реализациями, видели код точно в таком виде, как он напечатан в книге.

При определении отношения вычисления нам придется проверять, является ли терм числовым значением:

Это типичный пример OCaml-овского рекурсивного определения с сопоставлением: isnumericval определяется как функция, которая, будучи вызвана с аргументом TmZero, воазвращает true; будучи применена к TmSucc с поддеревом t1, вызывает себя рекурсивно с аргументом t1, чтобы проверить, является ли он числовым значением; а будучи вызвана с любым другим аргументом, возвращает false. Знаки подчеркивания в некоторых образцах — метки <<неважно>>, они сопоставляются с любым термом, который стоит в указанном месте; в первых двух предложениях с их помощью игнорируются аннотации info, а в последнем предложении с ее помощью сопоставляется любой терм. Ключевое слово rec говорит компилятору, что определение функции рекурсивно — т. е., что идентификатор isnumericval в теле функции относится к самой функции, которую сейчас определеяют, а не к какой-либо более ранней переменной с тем же именем.

Заметим, что ML-код в приведенном определении при верстке немного <<украшен>>, как для простоты чтения, так и для сохранения стиля примеров из лямбда-исчисления. В частности, мы используем настоящий символ стрелки →, а не двухсимвольную последовательность ->. Полный список типографских соглашений можно найти на веб-сайте книги.

Аналогично выглядит функция, проверяющая, является ли терм значением:

В третьем предложении встречается <<условный образец>>: он сопоставляется с любым термом t, но только если булевское выражение isnumericval t возвращает значение <<истина>>.

4.2 Вычисление

Реализация отношения вычисления точно следует правилам одношагового вычисления из Рис. 3.1 и 3.2. Как мы видели, эти правила определяют частичную функцию, которая, будучи применена к терму, не являющемуся значением, выдает следующий шаг вычисления этого терма. Если функцию попытаться применить к значению, она никакого результата не выдает. При переводе правил вычисления на OCaml нам нужно решить, как действовать в таком случае. Один очевидный вариант состоит в том, чтобы написать функцию одношагового вычисления eval1 так, чтобы она вызывала исключение, если ни одно из правил невозможно применить к терму, полученному в качестве параметра. (Другой способ действий был бы заставить вычислитель возвращать значение типа term option, которое бы показывало, было ли вычисление успешным, и если да, то каков результат; это тоже работало бы, но потребовало бы больше служебного кода.) Сначала мы определяем исключение, которое можно вызывать, если не применимо ни одно правило:

Теперь можно написать саму функцию одношагового вычисления.

Заметим, что в нескольких местах мы собираем термы заново, а не переделываем уже существующие. Поскольку эти новые термы не присходят из пользовательского исходного файла, аннотации info в них не имеют смысла. В таких термах мы используем константу dummyinfo. Для сопоставления с аннотациями в образцах всегда используется переменная fi (file information, <<информация о файле>>).

Еще одна существенная деталь в определении eval1 — использование явных выражений when в образцах, чтобы представить эффект имен метапеременных вроде v и nv в правилах, определяющих отношение вычисления на Рис. 3.1 и 3.2. Например, в выражении для вычисления TmPred(_,TmSucc(_,nv1)), семантика OCaml-овских образцов позволяет nv1 сопоставляться с каким угодно термом, а это не то, чего мы хотим; добавление when (isnumericval nv1) ограничивает правило так, чтобы оно запускалось только тогда, когда терм, соответствующий nv1, на самом деле является числовым значением. (Мы, в принципе, могли бы переписать исходные правила вывода в таком же стиле, как образцы ML, переводя неявные ограничения, основанные на именах метапеременных, в явные условия применения правил:

При этом пострадала бы компактность и читабельность правил.)

Наконец, функция eval берет терм и находит его нормальную форму, применяя eval1 циклически. Если eval1 возвращает новый терм t', мы вызываем eval рекурсивно, чтобы продолжить вычисление, начиная с t'. Когда, наконец, eval1 достигнет состояния, где не применимо никакое правило, она вызывает исключение NoRuleApplies. При этом eval вылетает из цикла и возвращает последний терм последовательности.²

Разумеется, наш простой вычислитель написан так, чтобы упростить сравнение с математическим определением вычисления, а не так, чтобы находить нормальные формы как можно быстрее. Несколько более эффективный алгоритм можно получить, если взять за основу правила вычисления <<с большим шагом>>, как предлагается в Упражнении 2.

Упражнение 2 [Рекомендуется,★★★¬→]:
Измените определение функции eval в программе arith, используя стиль с большим шагом из Упражнения 17.

4.3 Что осталось за кадром

Разумеется, в любом интерпретаторе и компиляторе — даже в очень простом, — много модулей помимо того, что мы обсудили здесь. На самом деле вычисляемые термы изначально хранятся в файлах как последовательности символов. Их нужно считать из файловой системы, перевести в последовательность лексем при помощи лексического анализатора, потом с помощью синтаксического анализатора собрать из них абстрактные синтаксические деревья, и только тогда скормить функциям вычисления, которые мы видели в этой главе. Более того, после вычисления нужно распечатать результаты.

Интересующиеся читатели могут исследовать код всего интерпретатора на OCaml.

Chapter 5 Бестиповое лямбда-исчисление

В этой главе определяется бестиповое, или чистое, лямбда-исчисление, и рассматриваются его основные свойства. Бестиповое лямбда-исчисление служит вычислительной основой, <<почвой>>, на которой произрастает большинство систем типов, описываемых в оставшейся части книги.¹

В середине 60-х годов Питер Ландин сделал наблюдение, что сложный язык программирования можно изучать, сформулировав для него небольшое базовое исчисление, которое выражает самые существенные механизмы языка, и дополнив его набором удобных производных конструкций, чье поведение описывается путем перевода на язык базового исчисления (Landin 1964, 1965, 1966; см. также Tennent 1981). В качестве базового языка Ландин использовал лямбда-исчисление, формальную систему, изобретенную в 1920-е годы Алонсо Чёрчем (Church 1936, 1941), где все вычисление сводится к элементарным операциям — определению функции и ее применению. Под влиянием идей Ландина, а также новаторских работ Джона Маккарти по языку Lisp (McCarthy 1959, 1981), лямбда-исчисление стало широко использоваться для спецификации свойств языков программирования, в разработке и реализации языков, и в исследовании систем типов. Важность этого исчисления основывается на том, что его можно одновременно рассматривать как простой язык программирования, на котором можно описывать вычисления, и как математический объект, о котором можно доказывать строгие утверждения.

Лямбда-исчисление — лишь одно из нескольких базовых исчислений, используемых для подобных целей. Пи-исчисление Милнера, Пэрроу и Уокера (Milner, Parrow and Walker 1992, 1991) завоевало популярность как базовый язык для определения семантики языков параллельных вычислений с обменом сообщениями, а исчисление объектов Абади и Карделли (Abadi and Cardelli 1996) выражает суть объектно-ориентированных языков. Большинство идей и методов, которые мы опишем и разработаем для лямбда-исчисления, можно без особого труда перенести и на эти другие исчисления. Один из опытов в этом направлении представлен в Главе 19.

Лямбда-исчисление можно расширить и обогатить нескольими способами. Во-первых, часто бывает удобно добавить особый конкретный синтаксис для чисел, кортежей, записей и т. п., чье поведение, в принципе, можно смоделировать и в базовом языке. Интереснее добавить более сложные свойства, такие, как изменяемые ссылочные ячейки или нелокальную обработку исключений. Эти свойства можно внести в базовый язык, только если использовать достаточно тяжеловесный перевод. Такие расширения в конце концов приводят к языкам вроде ML (Gordon, Milner and Wadsworth 1979; Milner, Tofte and Harper, 1990; Weis, Aponte, Laville, Mauny and Suárez 1989; Milner, Tofte, Harper and macQueen 1997), Haskell (Hudak et al., 1992) или Scheme (Sussman and Steele 1975; Kelsey, Clinger and Rees 1998). Как мы увидим в последующих главах, расширения базового языка часто связываются с расширениями системы типов.

5.1 Основы

Процедурная (или функциональная) абстракция является ключевым свойством почти всех языков программирования. Вместо того, чтобы переписывать одно и то же вычисление раз за разом, мы пишем процедуру или функцию, которая проделывает это вычисление в общем виде, в зависимости от одного или нескольких именованных параметров, а затем при необходимости вызываем эту процедуру, в каждом случае задавая значения параметров. К примеру, для программиста естественно взять длинное вычисление с повторяющимися частями вроде

и переписать его как factorial(5) + factorial(7) - factorial(3), где

Для каждого неотрицательного числа n подстановка аргумента n в функцию factorial дает в результате факториал n. Если мы будем писать <<λn. ...>> как сокращение для <<функция, которая, для каждого n, дает …>>, то определение factorial можно переформулировать как

Теперь factorial(0) означает <<функция λn. if n=0 then 1 else ..., примененная к аргументу 0>>, то есть, <<значение, которое получается, если аргумент n в теле функции (λn. if n=0 then 1 else ...) заменить на 0>>, то есть, <<if 0=0 then 1 else ...>>, то есть, 1.

Лямбда-исчисление (или λ-исчисление) воплощает такой способ определения и применения функций в наиболее чистой форме. В лямбда-исчислении все является функциями: аргументы, которые функции принимают — тоже функции, и результат, возвращаемый функцией — опять-таки функция.

Синтаксис лямбда-исчисления признает три вида термов.¹ Переменная x сама по себе терм; абстракция переменной x в терме t₁, что записывается как λx.t₁, тоже терм; и, наконец, применение терма t₁ к терму t₂ — третий вид термов. Эти способы построения термов выражаются следующей грамматикой:

В следующих подразделах исследуются некоторые детали этого определения.

5.1.1 Абстрактный и конкретный синтаксис

При обсуждении синтаксиса языков программирования полезно бывает различать два уровня² структуры. Конкретный (или поверхностный) синтаксис языка относится к строкам символов, которые читают и пишут программисты. Абстрактный синтаксис — это намного более простое внутреннее представление программ в виде размеченных деревьев (они называются абстрактные синтаксические деревья или АСД). Представление в виде дерева делает структуру термов непосредственно очевидной, и поэтому его естественно использовать для сложной обработки, которая нужна как при строгом определении языков (и доказательстве их свойств), так и внутри компиляторов и интерпретаторов.

Преобразование из конкретного в абстрактный синтаксис происходит в два этапа. Сначала лексический анализатор (или лексер) переводит последовательность символов, написанных программистом, в последовательность лексем — идентификаторов, ключевых слов, комментариев, символов пунктуации, и т. п. Лексический анализатор убирает комментарии и решает вопросы, связанные с пробельными символами, соглашениями о больших/маленьких буквах, а также форматах для числовых и символьных констант. После этого синтаксический анализатор переводит последовательность лексем в абстрактное синтаксическое дерево. При синтаксическом анализе соглашения о приоритете и ассоциативности операторов помогают уменьшить необходимость загромождать поверхностное представление программ скобками, явно указывающими структуру составных выражений. Например, * связывает сильнее, чем +, так что анализатор интерпретирует выражение без скобок 1+2*3 как левое абстрактное синтаксическое дерево, а не как правое:

В этой книге мы обращаем основное внимание на абстрактный, а не на конкретный синтаксис. Грамматики, вроде той, которую мы привели для лямбда-термов, должны рассматриваться как описания разрешенных видов деревьев, а не последовательностей лексем или символов. Разумеется, когда мы будем записывать термы в примерах, определениях, теоремах и доказательствах, нам придется выражать их в конкретной, линейной записи, но мы всегда будем иметь в виду соответствующие абстрактные синтаксические деревья.

Чтобы избежать излишних скобок, для записи лямбда-термов в линейной форме мы принимаем два соглашения. Во-первых, применение лево-ассоциативно, то есть, s t u обозначает то же дерево, что (s t) u:

Во-вторых, тела абстракций простираются направо как можно дальше, так что, например, λx. λy. x y x означает то же самое, что λx. (λy. ((x y) x)):

5.1.2 Переменные и метапеременные

Еще одна тонкость в приведенном определении синтаксиса касается использования метапеременных. Мы будем продолжать использовать метапеременную t (а также s и u, с индесками внизу или без них) как обозначение произвольного терма.³ Подобным образом, x (а также y и z) замещает произвольную переменную. Заметим, что здесь x служит переменной, чьими значениями являются переменные! К сожалению, число коротких имен ограничено, и нам потребуется иногда использовать x, y и т. д. как переменные объектного языка. Впрочем, из контекста всегда будет ясно, что имеется в виду. Например, в предложении <<Терм λx. λy. x y имеет вид λz. s, где z = x, а s = λy. x y>> имена z и s — метапеременные, в то время как x и y — переменные объектного языка.

5.1.3 Область видимости

Последнее, что нам требуется разъяснить в синтаксисе лямбда-исчисления, — область видимости переменных.

Вхождение переменной x называется связанным, если оно находится в теле t абстракции λx. t. (Точнее, оно связано этой абстракцией. Мы можем также сказать, что λx — связывающее определение, чья область видимости t.) Вхождение x свободно, если оно находится в позиции, где оно не связано никакой вышележащей абстракцией переменной x. Например, вхождения x в x y и λy. x y свободны, а вхождения x в λx. x и λz. λx. λy. x (y z) связаны. В (λx. x) x первое вхождение x связано, а второе свободно.

Терм без свободных переменных называется замкнутым; замкнутые термы называют также комбинаторами. Простейший комбинатор, называемый функцией тождества,

ничего не делает, а просто возвращает свой аргумент.

5.1.4 Операционная семантика

В своей чистой форме лямбда-исчисление не имеет никаких встроенных констант и элементарных операторов — ни чисел, ни арифметических операций, ни условных выражений, ни записей, ни циклов, ни последовательного выполнения выражений, ни ввода-вывода, и т. д. Единственное средство для <<вычисления>> термов — применение функций к аргументам (которые сами являются функциями). Каждый шаг вычисления состоит в том, что в терме-применении, где левый член является абстракцией, в теле этой абстракции связанная переменная заменяется на правый член. Записывается это так:

где [x ↦ t₂] t₁₂ означает <<терм, получаемый из t₁₂ путем замены всех свободных вхождений x на t₂>>. Например, терм (λx. x) y за шаг вычисления переходит в y, а терм (λx. x (λx. x)) (u r) переходит в u r (λx. x). Вслед за Чёрчем, терм вида (λx. t₁₂) t₂ называется редексом (reducible expression, <<сокращаемое выражение>>), а операция переписывания редекса в соответствии с указанным правилом называется бета-редукцией.

В течение многих лет разработчики языков программирования и теоретики изучали несколько различных стратегий вычисления в лямбда-исчислении. Каждая стратегия определяет, какой редекс или редексы в терме может сработать на следующем шаге.⁴

Выбор стратегии вычисления при обсужении систем типов почти ни на что не влияет. Вопросы, которые ведут к использованию тех или иных свойств типов, и методы, используемые для ответа на эти вопросы, для всех стратегий практически одинаковы. В этой книге мы используем вызов по значению: во-первых, потому что именно так работает большинство широко известных языков; и, во-вторых, потому что при этом легче всего ввести такие механизмы, как исключения (Глава 14) и ссылки (Глава 13).

5.2 Программирование на языке лямбда-исчисления

Лямбда-исчисление — значительно более мощный формализм, чем кажется на первый взгляд, судя по его крошечному определению. В этом разделе мы продемонстрируем несколько стандартных примеров программирования в этом формализме. Эти примеры приводятся здесь не для того, чтобы предложить использование лямбда-исчисления в качестве полноразмерного языка программирования — во всех распространенных языках те же самые задачи можно решить более понятным и эффективным образом, — а в качестве разминки, чтобы дать читателям почувствовать, как эта система устроена.

5.2.1 Функции с несколькими аргументами

Заметим для начала, что в лямбда-исчисление не встроена поддержка функций с несколькими аргументами. Разумеется, было бы нетрудно ее добавить, однако того же самого результата проще достичь через функции высшего порядка, которые возвращают функции в качестве результата. Допустим, у нас есть терм s с двумя свободными переменными x и y, и мы хотим написать функцию f такую, чтобы она для каждой пары аргументов (v,w) выдавала результат подстановки v вместо x и w вместо y. Мы пишем не f = λ(x,y).s, как мы бы это сделали в более богатом языке, а f = λx.λy.s. А именно, f — это функция, которая, получив значение v для параметра x, выдает функцию, которая, получив значение w для параметра y, выдает нужный результат. После этого мы применяем f к аргументам по одному, получая запись f v w (т. е., (f v) w), которая переходит в ((λy.[x↦s]) w), и далее в [y ↦ w][x ↦ v]s. Такое преобразование функций с несколькими аргументами в функции высшего порядка называется каррированием в честь Хаскелла Карри, современника Чёрча.

5.2.2 Булевские константы Чёрча

Еще одна языковая конструкция, легко кодируемая в лямбда-исчислении — булевские значения и условные выражения. Определим термы tru и fls таким образом:

(Имена этих термов сделаны сокращенными, чтобы они меньше путались с элементарными булевскими константами true и false из Главы 3.)

Можно считать, что термы tru и fls представляют булевские значения <<истина>> и <<ложь>> в том смысле, что с их помощью мы можем выполнять операцию проверки булевского значения на истинность. А именно, мы можем определить комбинатор test, такой, что test b v w переходит в v, если b равно tru, и в w, если b равно fls.

Комбинатор test почти ничего не делает: test b v w просто переходит в b v w. В сущности, само булевское значение является условным выражением: оно принимает два аргумента и выбирает из них либо первый (если это tru), либо второй (если это fls). Например, терм test tru v w редуцируется таким образом:

Несложно также определить операторы вроде логической конъюнкции:

То есть, and — это функция, которая, получив два логических значения b и c, возвращает c, если b равно tru и fls, если b равно fls; таким образом, and b c выдает tru, если и b, и c равны tru, и fls, если либо b, либо c окажутся fls.

Упражнение 1 [★]: Определите логические функции or (<<или>>) и not (<<не>>).

5.2.3 Пары

При помощи булевских констант мы можем закодировать пары значений в виде термов:

А именно, pair v w — функция, которая, будучи применена к булевскому значению b, применяет b к v и w. По определению булевских констант, при таком вызове получится v, если b равняется tru, и w, если b равняется fls, так что функции первой и второй проекции fst и snd можно получить, просто подав в пару соответствующие булевские значения. Вот проверка утверждения fst (pair v w) →^* v:

5.2.4 Числа Чёрча

Представление чисел в виде лямбда-термов лишь ненамного сложней, чем то, что мы уже видели. Определяем числа Чёрча c_o, c₁, c₂, и т. д., таким образом:

и т. д.⁶
А именно, каждое число n представляется комбинатором c_n, принимающим два аргумента, s и z (<<функция следования>> и <<ноль>>), и применяет s к z n раз. Как и в случае с булевскими константами и парами, такое кодирование превращает числа в активные сущности: число n представляется функцией, которая что-то делает n раз — своего рода активная единичная (по основанию 1) запись.

(Читатель мог уже заметить, что c₀ и fls на самом деле являются одним и тем же термом. Такие <<каламбуры>> часто встречаются в языках ассемблера, где одна и та же комбинация битов может представлять множество разных значений — целое число, число с плавающей точкой, адрес, четыре символа и т. п., — в зависимости от того, как биты интерпретируются, а также в низкоуровневых языках вроде C, где 0 и false тоже представляются одинаково.)

Функцию следования на числах Чёрча можно определить так:

Терм scc — комбинатор, который принимает число Чёрча n и возвращает другое число Чёрча, — то есть, возвращает функцию, которая принимает аргументы s и z, и многократно применяет s к z. Нужное число применений s к z мы получаем, сначала передав s и z в качестве аргументов n, а затем явным образом применив s еще раз к результату.

Упражнение 2 [★★]: Найдите еще один способ определить функцию следования на числах Чёрча.

Подобным образом, сложение на числах Чёрча можно определить как терм plus, принимающий в качестве аргументов два числа Чёрча, m и n, и возвращающий еще одно число Чёрча — т. е., функцию, — которая берет аргументы s и z, применяет s к z n раз (передавая s и z в качестве аргументов n), а потом применяет s еще m раз к результату:

Реализация умножения пользуется еще одним трюком: поскольку plus принимает аргументы по одному, применение его к одному аргументу n дает функцию, которая добавляет n к любому данному ей аргументу. Можно передать эту функцию в качестве первого аргумента m, а в качестве второго дать c₀, и это будет означать <<примени функцию, добавляющую n к своему аргументу, m раз в цикле, к нулю>>, т. е., <<сложи вместе m копий числа n>>.

Упражнение 3 [★★]: Возможно ли определить умножение на числах Чёрча без использования plus?

Упражнение 4 [Рекомендуется,★★]: Определите терм для возведения чисел в степень.

Чтобы проверить, является ли число Чёрча нулем, нужно найти какую-то подходящую пару аргументов, которая вернет нам эту информацию — конкретно, нам нужно применить число к паре термов zz и ss, так, чтобы применение ss к zz один или более раз давало fls, а неприменение ни одного раза давало tru. Понятно, что в качестве zz нужно просто взять tru. Для ss мы используем функцию, которая игнорирует свой аргумент и всегда возвращает fls:

Как ни странно, определить вычитание на числах Чёрча намного сложнее, чем сложение. Можно для этого воспользоваться следующей довольно хитрой <<функцией предшествования>>, которая, принимая c₀ как аргумент, возвращает c₀, а принимая c_i+1, возвращает c_i:

Это определение работает, используя m как функцию и применяя с ее помощью m копий функции ss к начальному значению zz. Каждая копия ss берет пару чисел pair c_i c_j как аргумент и выдает пару pair c_j c_j+1 как результат (см. Рис. 5.1). Таким образом, при m-кратном применении к pair c₀ c₀ получается pair c₀ c₀, если m = 0, и pair c_m-1 c_m при положительном m. В обоих случаях, в первом компоненте пары находится искомый предшественник.

Упражнение 5 [★★]: При помощи prd определите функцию вычитания.

Упражнение 6 [★★]: Сколько примерно шагов вычисления (в зависимости от n) требуется, чтобы получить prd c_n?

Упражнение 7 [★★]: Напишите функцию equal, которая проверяет два числа на равенство и возвращает Чёрчеву булевскую константу. Например:

equal c₃ c₃ |> (λt. λf. t) equal c₃ c₂ |> (λt. λf. f)

Подобными же методами можно определить другие распространенные типы данных: списки, деревья, массивы, записи с вариантами, и т. п.

Упражнение 8 [Рекомендуется,★★★]: Список можно представить в лямбда-исчислении через его функцию свертки fold. (В OCaml эта функция называется fold_right; ее иногда еще называют reduce.) Например, список [x, y, z] становится функцией, которая принимает два аргумента c и n, и возвращает c x (c y (c z n)). Как будет выглядеть представление nil? Напишите функцию cons, которая принимает элемент h и список (то есть, функцию свертки) t, и возвращает подобное представление списка, получаемого добавлением h в голову t. Напишите функции isnil и head (каждая из них принимает список в качестве параметра). Наконец, напишите функцию tail для такого представления списков (это намного сложнее; придется использовать трюк того же рода, как при определении prd для чисел).

5.2.5 Расширенное исчисление

Мы убедились, что булевские значения, числа и операции над ними могут быть закодированы средствами чистого лямбда-исчисления. Строго говоря, все нужные нам программы мы можем писать, не выходя за рамки этой системы. Однако при работе с примерами часто бывает удобно включить в нее элементарные булевские значения и числа (а может быть, и другие типы данных). В случаях, когда нам нужно совершенно точно указать, с какой системой мы в данный момент работаем, для чистого лямбда-исчисления, определяемого на Рис. 5.3, мы будем использовать обозначение λ, а для системы, в которую добавлены булевские и арифметические выражения с Рис. 3.1 и 3.2 – обозначение λNB.

В λNB у нас есть две разных реализации булевских значений и две реализации чисел: настоящие и закодированные по методам этой главы, и мы можем выбирать между ними при написании программ. Разумеется, между этими двумя реализациями нетрудно написать преобразования. Чтобы перевести булевское значение по Чёрчу в элементарное булевское значение, нужно применить его к значениям true и false:

Для преобразования в обратном направлении используется условное выражение:

Можно встроить эти преобразования в операции высшего порядка. Вот проверка на равенство для чисел Чёрча, возвращающая настоящее логическое значение:

Таким же образом мы можем преобразовать число Чёрча в соответствующее элементарное число, применив его к succ и 0:

Мы не можем напрямую применить m к succ, поскольку сама по себе запись succ не имеет синтаксического смысла: мы определили арифметические выражения так, что succ всегда должен к чему-то применяться. Это требование мы обходим, обернув succ в маленькую функцию, которая всегда возвращает succ от своего аргумента.

Причины, по которым элементарные булевские и числовые значения оказываются полезны при работе с примерами, в основном связаны с порядком вычислений. Рассмотрим, например, терм scc c₁. Исходя из имеющегося обсуждения, мы могли бы ожидать, что он должен при вычислении давать число Чёрча c₂. На самом деле этого не происходит:

Этот терм содержит в себе редекс, котрый при вычислении привел бы нас (за два шага) к c₂, однако согласно правилам вызова по значению мы не имеем на это права, поскольку редекс находится внутри лямбда-абстракции.

Никакой фундаментальной проблемы здесь нет: терм, получающийся при вычислении scc c₁, очевидным образом поведенчески эквивалентен c₂, в том смысле, что применение этого терма к паре аргументов v и w всегда даст тот же результат, что и применение c₂ к тем же аргументам. Однако остаточное вычисление затрудняет проверку, что наша функция scc ведет себя как надо. В случае более сложных арифметических вычислений трудность еще возрастает. Например, times c₂c₂ дает в результате не c₄, а такое чудовищное выражение:

Можно убедиться, что этот терм ведет себя так же, как c₄, с помощью проверки на равенство:

Однако более прямой способ — взять times c₂c₂ и преобразовать в элементарное число:

Функция преобразования дает выражению times c₂c₂ два аргумента, которых оно ожидает, и заставляет все задержанные вычисления в его теле сработать.

5.2.6 Рекурсия

Вспомним, что терм, который не может продвинуться дальше согласно отношению вычисления, называется нормальной формой. Любопытно, что у некоторых термов нет нормальной формы. Например, незавершающийся комбинатор

содержит только один редекс, но шаг вычисления этого редекса дает в результате опять omega! Про термы, не имеющие нормальной формы, говорят, что они не завершаются.

Комбинатор omega можно обобщить до полезного терма, называемого комбинатор неподвижной точки,⁶ и с его помощью можно определять рекурсивные функции, например, factorial.⁷

Подобно omega, комбинатор fix имеет сложную структуру с повторами; глядя на определение, трудно понять, как он работает. Вероятно, лучший способ заработать интуицию о его поведении — рассмотреть его действие в конкретном примере.⁸ Допустим, мы хотим написать рекурсивное определение функции вида h = ⟨тело, содержащее h⟩ — т. е., нам хочется написать определение, в котором правая часть использует ту самую функцию, которую мы определяем, как в определении факториала на странице ??. Идея в том, чтобы рекурсивное определение <<разворачивалось>> там, где оно встретится; скажем, определение факториала, интуитивно,

Этого можно добиться при помощи комбинатора fix, сначала определив g = ⟨тело, содержащееf⟩, а затем h = fix g. Например, функцию факториала можно определить через

На Рис. 5.2 показано, что происходит с термом factorial c₃ при вычислении. Ключевое свойство, которое обеспечивает работу этого вычисления, это fct n →^*g fct n. Таким образом, fct — своего рода <<самовоспроизводящийся автомат>>, который, будучи применен к аргументу n, дает самого себя и n в качестве аргументов g. Там, где первый аргумент встречается в теле g, мы получим еще одну копию fct, которая, будучи применена к аргументу, опять передаст самое себя и аргумент внутрь g, и т. д. Каждый раз, когда мы делаем рекурсивный вызов при помощи fct, мы разворачиваем очередную копию g и снабжаем ее очередными копиями fct, готовыми развернуться еще дальше.

Упражнение 9 [★]: Почему в определении g мы использовали форму if, а не функцию test, работающую с Чёрчевыми булевскими значениями? Покажите, как определить функцию factorial при помощи test вместо if.

Упражнение 10 [★★]: Напишите функцию churchnat, переводящую элементарное натуральное число в представление Чёрча.

Упражнение 11 [Рекомендуется,★★]: С помощью fix и кодирования списков из Упражнения 8 напишите функцию, суммирующую список, состоящий из чисел Чёрча.

5.2.7 Представление

Прежде, чем закончить рассмотрение примеров и заняться формальным определением лямбда-исчисления, следует задаться еще одним последним вопросом: что, строго говоря, означает утверждение, что числа Чёрча представляют обыкновенные числа?

Чтобы ответить на этот вопрос, давайте вспомним, что такое обыкновенные числа. Существует много (эквивалентных) определений; мы в этой книге (Рис 3.2) выбрали такое:

Поведение арифметических операций определяется правилами вычисления на Рис. 3.2. Эти правила говорят нам, например, что 3 следует за 2, и что iszero 0 истинно.

Кодирование по Чёрчу представляет каждый из этих элементов в виде лямбда-терма (то есть, функции):

Собирая все эти утверждения вместе, представим, что у нас есть программа, которая проделывает некоторые сложные численные вычисления и выдает булевский результат. Если мы заменим все числа и арифметические операции лямбда-термами, которые их представляют, и запустим получившуюся программу, мы получим тот же самый результат. Таким образом, с точки зрения воздействия на окончательные результаты программ, нет никакой разницы между настоящими числами и их представлениями по Чёрчу.

5.3 Формальности

В оставшейся части главы мы даем точное определение синтаксиса и операционной семантики лямбда-исчисления. Большая часть необходимой структуры устроена так же, как в Главе 3 (чтобы не повторять всю эту структуру заново, мы здесь определяем только чистое лямбда-исчисление, не дополненние булевскими значениями и числами). Однако операция подстановки терма вместо переменной связана с неожиданными сложностями.

5.3.1 Синтаксис

Как и в Главе 3, абстрактная грамматика, определяющая термы (на стр. ??) должна рассматриваться как сокращенная запись индуктивно определенного множества абстрактных синтаксических деревьев.

Определение 1 [Термы]: Пусть имеется счетное множество имен переменных V. Множество термов — это наименьшее множество T, такое, что

x ∈ T для всех x ∈ V;
Если t₁ ∈ T и x ∈ V, то λx.t₁ ∈ T;
Если t₁ ∈ T и t₂ ∈ T, то t₁ t₂ ∈ T.

Размер терма t можно определить точно так же, как мы это сделали для арифметических выражений в Определении 2. Кроме того, можно дать простое индуктивное определение множества свободных переменных, встречающихся в терме.

Определение 2 Множество свободных переменных терма t (записывается FV(t)) определяется так:

FV(`x`)	=	{`x`}
FV(`λ``x. t`₁)	=	FV(`t`₁) \ {`x`}
FV(`t`₁ `t`₂)	=	FV(`t`₁) ⋃ FV(`t`₂)

Упражнение 3 [★★]: Постройте строгое доказательство утверждения: |FV(t)| ≤ size(t) для любого терма t.

5.3.2 Подстановка

Операция подстановки, когда ее требуется строго определить, оказывается довольно хитроумной. В этой книге мы будем использовать два разных определения, каждое из которых удобно для своих целей. Первое, вводимое нами в этом разделе, краткое и интуитивно понятное, хорошо работает в примерах, в математических определениях и доказательствах. Второе, рассматриваемое в Главе 6, использует более сложную нотацию и зависит от альтернативного <<представления де Брауна>> для термов, где именованные переменные заменяются на числовые индексы, но оно оказывается более удобным для конкретных реализаций ML, которые обсуждаются в последующих главах.

Поучительно придти к определению подстановки, пройдя через пару неудачных попыток. Попробуем сначала самое наивное рекурсивное определение. (С формальной точки зрения, мы определяем функцию [x ↦ s] индукцией по аргументу t.):

Такое определение в большинстве случаев работает правильно. Например, оно дает

что соответствует нашей интуиции о том, как должна себя вести подстановка. Однако при неудачном выборе имен связанных переменных это определение ломается. Например:

Это противоречит базовой интуиции по поводу функциональной абстракции: имена связанных переменных не должны ни на что влиять — функция тождества остается собой, запишем мы ее в виде λx.x, λy.y или λfranz.franz. Если эти термы ведут себя по-разному при подстановке, они себя по-разному поведут и при редукции, а это кажется неправильным.

Ясно, что первая ошибка, которую мы допустили при наивном определениии подстановки, состоит в том, что мы не стали отличать свободное вхождение переменной x в терм t (которое при подстановке нужно заменять) от связанного (которое не нужно). Когда мы достигаем абстракции, связывающей имя x внутри t, операция подстановки должна останавливаться. Это ведет к следующей попытке:

Такой вариант работает лучше, но, опять-таки, не всегда. Посмотрим, например, что получается, когда мы пытаемся подставить терм z вместо переменной x в терме λz.x:

В этот раз мы совершили, в сущности, противоположную ошибку: превратили функцию-константу λz. x в функцию тождества! Это снова случилось оттого, что мы выбрали z в качестве имени связанной переменной в функции-константе, так что что-то мы до сих пор делаем не так.

Ситуация, когда свободные переменные терма s становятся связанными, будучи наивно подставленными в терм t, называется захват переменных. Чтобы избежать его, нужно убедиться, что имена связанных переменных в t отличаются от имен свободных переменных в s. Операция подстановки, которая этого умеет правильно добиваться, называется подстановка, свободная от захвата. (Обычно, когда просто говорят <<подстановка>>, именно такую подстановку и имеют в виду.) Мы можем добиться требуемого эффекта, если добавим еще одно условие ко второму варианту при подстановке в терм-абстракцию:

Теперь почти все правильно: наше определение подстановки делает то, что требуется, когда оно вообще что-то делает. Проблема в том, что последнее изменение превратило подстановку из полной функции в частичную. Например, новое определение не выдает никакого результата для [x ↦ y z](λy. x y): связанная переменная y терма, в который производится подстановка, не равна x, но она встречается как свободная в терме (y z), и ни одна строка определения не применима.

Распространенное решение этой проблемы в литературе по системам типов и лямбда-исчислению состоит в том, что термы рассматриваются <<с точностью до переименования переменных>>. (Чёрч называл операцию последовательного переименования переменных в терме альфа-конверсией. Этот термин употребляется и до сих пор — мы могли бы сказать, что рассматриваем термы <<с точностью до альфа-конверсии>>.)

Соглашение 4 Термы, отличающиеся только именами связанных переменных, взаимозаменимы во всех контекстах.

На пракике это означает, что имя любой λ-связанной переменной можно заменить на другое (последовательно проведя это переименование в теле λ) всегда, когда это оказывается удобным. Например, если мы хотим вычислить [x ↦ y z](λy. x y), мы сначала переписываем (λy. x y) в виде, скажем, (λw. x w). Затем мы вычисляем [x ↦ y z](λw. x w), что дает нам (λw. y z w).

Это соглашение делает наше определение <<все равно что полным>>, поскольку каждый раз, как мы пытаемся его применить к аргументам, к которым оно неприменимо, мы можем исправить дело переименованием, так, чтобы все условия выполнялись. В сущности, приняв это соглашение, мы можем сформулировать определение подстановки чуть короче. Мы можем отбросить первый вариант в определении для абстракций, поскольку всегда можно предположить (применяя, если надо, переименование), что связанная переменная y отличается как от x, так и от свободных переменных s. Определение принимает окончательный вид.

Определение 5 [Подстановка]:

[`x` ↦ `s`]`x`	=	`s`
[`x` ↦ `s`]`y`	=	`y`	если `y` ≠ `x`
[`x` ↦ `s`](`λ``y. t`₁)	=	`λ``y.` `[``x` `↦` `s``]``t`₁	если `y` ≠ `x` и `y` ∉ FV(`s`)
[`x` ↦ `s`](`t`₁ `t`₂)	=	([`x` ↦ `s`]`t`₁) ([`x` ↦ `s`]`t`₂)

5.4 Операционная семантика

Операционная семантика лямбда-термов вкратце представлена на Рис. 5.3. Множество значений в этом исчислении более интересно, чем было в случае арифметических выражений. Поскольку вычисление (с вызовом по значению) останавливается, когда достигает лямбды, значениями являются произвольные лямбда-термы.

Отношение вычисления показано в правом столбце рисунка. Как и в случае арифметических выражений, имеется два типа правил: рабочее правило E-AppAbs и правила соответствия E-App1 и E-App2.

Обратите внимание, как выбор метапеременных в этих правилах помогает управлять порядком вычислений. Поскольку v₂ может относиться только к значениям, левая сторона правила E-AppAbs соотвтествует всем применениям термов, где терм-аргумент является значением. Точно так же, E-App1 относится к тем применениям, где левая часть не является значением, поскольку t₁ может обозначать любой терм, но предпосылка правила требует, чтобы t₁ был способен совершить шаг вычисления. Напротив, E-App2 не срабатывает, пока левая часть не станет значением, которое может быть обозначено метапеременной v. Взятые вместе, эти правила полностью определяют порядок вычисления терма вида (t₁ t₂): сначала работает E-App1, пока t₁ не сведется к значению, затем E-App2 применяется до тех пор, пока значением не окажется t₂, и, наконец, само применение обрабатывается правилом E-AppAbs.

Упражнение 1 [★★]:
Модифицируйте эти правила, чтобы описать три другие стратегии вычисления: полную бета-редукцию, нормальный порядок и ленивое вычисление.

Заметим, что в чистом лямбда-исчислении единственные возможные значения — это лямбда-абстракции, так что, если E-App1 доводит t₁ до значения, это значение должно быть лямбда-абстракцией. Разумеется, это утверждение перестает работать, как только мы добавляем в язык другие конструкции, скажем, элементарные булевские значения, поскольку при этом у нас появляются новые виды значений.

Упражнение 2 [★★,¬→]:
В Упражнении 16 дается альтернативное представление операционной семантики булевских и арифметических выражений, где тупиковые термы дают при вычислении особую константу wrong. Распространите эту семантику на λNB.

Упражнение 3 [★★]:
В Упражнении 17 вводится стиль вычисления арифметических выражений <<с большим шагом>>, где базовое отношение вычисления означает <<терм t при вычислении дает окончательный результат v>>. Покажите, как сформулировать правила вычисления лямбда-термов в этом стиле.

5.5 Дополнительные замечания

Бестиповое лямбда-исчисление было разработано Чёрчем и его коллегами в 20-е и 30-е годы (Church 1941). Стандартный текст по всем вопросам бестипового лямбда-исчисления – книга Барендрегта (Barenddregt 1984); Хиндли и Селдин (Hindley and Seldin 1986) уже по охвату, но легче для чтения. Статья Барендрегта (Barendregt 1990) в Справочнике по теоретической информатике представляет собой краткий обзор. Сведения о лямбда-исчислении можно найти также во множестве учебников по функциональным языкам программирования (Abelson and Sussman 1985; Friedman, Wand and Haynes 2001; Peyton Jones and Lester 1992) и по семантике языков программирования (напр., Schmidt 1986; Gunter 1992; Winskel 1993; Mitchell 1996). Систематический метод кодирования различных структур данных в виде лямбда-термов описан в статье Бёма и Берардуччи (Böhm and Berarducci 1985).

Несмотря на название, Карри не признавал за собой чести быть изобретателем каррирования. Часто ее приписывают Шёнфинкелю (Schönfinkel 1924), однако основная идея была уже известна нескольким математикам 19-го века, включая Фреге и Кантора.

Возможно, у системы найдутся приложения не только в роли логического исчисления. Алонсо Чёрч, 1932

Chapter 6 Представление термов без использованиия имен

В предыдущей главе мы работали с термами <<с точностью до переименования связанных переменных>>. У нас действовало общее соглашение, что связанные переменные можно в любой момент переименовать, чтобы провести подстановку или если новое имя по каким-то другим причинам оказывается удобнее. В сущности, <<внешний вид>> имени связанной переменной можно задать какой нам понравится. Такое соглашение отлично работает при обсуждении основных идей лямбда-исчисления, оно помогает понятно записывать доказательства, однако при реализации исчисления в виде программы нам нужно иметь для каждого терма единое представление; в частности, требуется решить, как будут представлены вхождения переменных. Есть несколько способов решить эту задачу:¹

Каждая из этих схем имеет свои преимущества, и выбор между ними до некоторой степени дело вкуса (в серьезных реализациях компиляторов действуют еще соображения производительности, но нас они сейчас не волнуют). Мы выбираем третий вариант, который, по нашему опыту, будет лучше масштабироваться, когда нам потребуется работать с некоторыми более сложными интерпретаторами из этой книги. Одна из причин этого в том, что, будучи реализован с ошибками, он обычно завершается аварийно, а не выдает неверные ответы. Это позволяет нам обнаруживать и исправлять ошибки достаточно быстро. Напротив, известны случаи, когда в реализациях, основанных на именованных переменных, неправильное поведение длилось месяцы и годы. Наша реализация использует хорошо известный метод, изобретенный Николасом де Брауном (de Bruijn 1972).

6.1 Термы и контексты

Идея де Брауна состояла в том, чтобы представлять термы более естественным — пусть и менее читабельным, — образом, заставив вхождения переменных прямо указывать на их связывающие определения, всесто того, чтобы называть их по имени. Для этого можно заменить именованные переменные натуральными числами, где число k означает <<переменная, связанная k-й охватывающей λ>>. Например, обыкновенный терм λx.x соответствует безымянному терму λ.0, а λx.λy. x (y x) соответствует λ.λ. 1 (0 1). Безымянные термы иногда еще называют термами де Брауна, а нумерованные переменные в них называются индексами де Брауна.¹ Разработчики компиляторов для того же понятия используют термин <<статические расстояния>>.

Упражнение 1 [★]: Для каждого из следующих комбинаторов

c₀ = λs. λz. z; c₂ = λs. λz. s (s z); plus = λm. λn. λs. λz. m s (n s z); fix = λf. (λx. f(λy. (x x) y)) (λx. f(λy. (x x) y)); foo = (λx. (λx. x)) (λx. x);

запишите соответствующий безымянный терм.

Формально мы определяем синтаксис безымянных термов почти так же, как определялся синтаксис обыкновенных термов (5.3.1). Единственная разница состоит в том, что требуется внимательно следить, сколько свободных переменных может содержать каждый терм. То есть, требуется отличать множества термов без свободных переменных (называемых 0-термами), термов, где максимум одна свободная переменная (1-термы), и так далее.

Определение 2 [Термы]: Пусть T — наименьшее семейство множеств {T₀, T₁, T₂, …}, такое, что

k ∈ T_n, если 0 ≤ k < n;
если t₁ ∈ T_n и n > 0, то λ.t₁ ∈ T_n−1;
если t₁ ∈ T_n и t₂ ∈ T_n, то (t₁ t₂) ∈ T_n.

(Заметим, что мы имеем здесь стандартное индуктивное определение, только определяем семейство множеств, индексируемое числами, а не одно множество.) Элементы каждого T_n называются n-термами.

Элементы T_n — это термы с не более, чем n переменных, пронумерованных от 0 до n−1: каждый данный элемент T_n не обязан содержать свободные переменные со всеми этими номерами, и вообще не обязан иметь какие-либо свободные переменные. В частности, если t замкнут, он является элементом T_n для любого n.

Заметим, что всякий (замкнутый) обыкновенный терм имеет ровно одно представление де Брауна, и что два обыкновенных терма эквивалентны с точностью до переименования связанных переменных тогда и только тогда, когда у них одинаковые представления де Брауна.

Чтобы работать с термами, содержащими свободные переменные, нам потребуется понятие контекста именования. Например, допустим, нам нужно представить в виде безымянного терма λx. y x. Мы знаем, что делать с x, но не знаем, как вести себя с y, поскольку неизвестно, как <<далеко>> эта переменная будет определена, и какой ей сопоставить номер. Решение состоит в том, чтобы выбрать, раз и навсегда, присвоение (называемое контекстом именования) индексов де Брауна свободным переменным, и последовательно использовать это присвоение, когда требуется выбрать номер для свободной переменной. Например, предположим, что мы решили работать в следующем контексте именования:

Тогда x (y z) будет представлен как 4 (3 2), в то время как λw. y w будет представлен как λ. 4 0, а λw.λa.x как λ.λ.6.

Поскольку порядок, в котором переменные следуют в Γ, однозначно определяет их числовые индексы, мы можем кратко записать контекст в виде последовательности.

Определение 3 Допустим, x₀,… x_n — имена переменных из V. Контекст именования Γ = x_n, x_n−1, … x₁, x₀ присваивает каждой x_i индекс де Брауна i. Заметим, что самая правая переменная в контексте получает индекс 0; это соответствует тому, как мы считаем λ-связывания — справа налево, — когда преобразуем именованный терм в безымянный. Множество {x_n, …, x₀} переменных, упомянутых в Γ, мы обозначаем dom(Γ).

Упражнение 4 [★★★,¬→]: Постройте альтернативную конструкцию множеств n-термов в стиле Определения 3, и покажите (как в Утверждении 6), что ваше определение эквивалентно имеющемуся.

Упражнение 5 [Рекомендуется,★★★]:

Определите функцию removenames_Γ(t), которая принимает контекст именования Γ и обыкновенный терм t (где FV(t) ⊆ dom(Γ)), и порождает соответствующий безымянный терм.
Определите функцию restorenames_Γ(t), которая принимает безымянный терм t и контекст Γ, и порождает обыкновенный терм. (В процессе вам придется <<выдумывать>> имена переменных, связанных абстракциями в t. Можете предположить, что имена в V попарно различаются, и что множество имен переменных V упорядочено, так что имеет смысл говорить <<возьмем первое имя переменной, которое еще не содержится в dom(Γ)>>.)

Эта пара функций должна иметь свойство

removenames_Γ(restorenames_Γ(t)) = t

для всякого безымянного терма t, а также

restorenames_Γ(removenames_Γ(t)) = t

с точностью до переименования связанных переменных, для всякого обыкновенного терма t.

Строго говоря, нельзя говорить о <<каком-то t ∈ T>> — всегда нужно указывать, сколько свободных переменных t разрешено иметь. На практике, впрочем, у нас всегда будет в распоряжении некоторый заранее заданный контекст именования Γ; мы будем несколько вольно обращаться с нотацией и писать t ∈ T, имея в виду t ∈ T_n, где n – длина Γ.

6.2 Сдвиг и подстановка

Нашей следующей задачей будет определить операцию подстановки ([k↦ s]t) на безымянных термах. Для этого потребуется вспомогательная операция, называемая <<сдвиг>>, перенумеровывающая индексы свободных переменных в терме.

Когда подстановка проникает внутрь λ-абстракции, к примеру, [1 ↦ s](λ.2) (т. е., [t ↦ s]λy.x, если предположить, что 1 – индекс переменной x во внешнем контексте), контекст, в котором происходит подстановка, становится на одну переменную длиннее исходного; требуется увеличить индексы свободных переменных в s, чтобы в новом контексте они ссылались на те же переменные, что и раньше. Однако делать это нужно осторожно: нельзя просто увеличить на единицу все индексы переменных s, потому что при этом сдвинулись бы и связанные переменные внутри s. Например, пусть s = 2 (λ.0) (т. е., s = z (λw.w), если 2 — индекс z во внешнем контексте). В этом случае нам требуется сдвинуть 2, но не 0. Функция сдвига, описанная ниже, принимает параметр <<отсечения>> c, управляющий тем, какие переменные сдвигаются. Он может быть 0 (что означает, что сдвигать надо все переменные), и увеличивается каждый раз, когда функция сдвига пересекает границу абстракции. Таким образом, при вычислении ↑_c^d(t) мы знаем, что терм t происходит изнутри c слоев абстракции по отношению к исходному аргументу ↑^d. Получается, что все идентификаторы k < c внутри t связаны в исходном аргументе и сдвигу не подлежат, а идентификаторы k ≥ c свободны, и их нужно сдвинуть.

Определение 1 [Сдвиг]: Сдвиг терма t на d позиций с отсечением c, обозначаемый ↑_c^d(t), определяется так:

↑_c^d(k)

⎧
⎪
⎨
⎪
⎩

`k`	если `k` < c
`k` + d	если `k` ≥ c

↑_c^d(λ.t₁) = λ. ↑_c+1^d(t₁)

↑_c^d(t₁ t₂) = ↑_c^d(t₁) ↑_c^d(t₂)

Запись ↑^d(t) означает ↑₀^d(t).

Упражнение 2 [★]:

Чему равняется ↑² (λ.λ. 1 (0 2))?
Чему равняется ↑² (λ. 0 1 (λ. 0 1 2))?

Упражнение 3 [★★,¬→]: Покажите, что, если t является n-термом и, если d<0, все свободные переменные t не меньше |d|, то ↑_c^d(t) является max(n+d,0)-термом.

Теперь мы готовы определить оператор подстановки [j ↦ s]t. Когда мы используем подстановку, обычно нас интересует подстановка последней переменной в контексте (т. е., j = 0), поскольку именно этот случай нам нужен, чтобы определить операцию бета-редукции. Однако для того, чтобы подставить значение переменной 0 в терме, который является лямбда-абстракцией, требуется уметь подставить значение переменной 1 в теле этой абстракции. Таким образом, определение подстановки должно работать с произвольной переменной.

Определение 4 [Подстановка]:Подстановка терма s вместо переменной номер j в терме t, что записывается [j ↦ s]t, определяется следующим образом:

[j ↦ s] k

⎧
⎨
⎩

`s`	если k = j
`k`	в противном случае

[j ↦ s] (λ.t₁) = λ. [j+1 ↦ ↑¹s]t₁

[j ↦ s] (t₁ t₂) = ([j ↦ s] t₁ [j ↦ s] t₂)

Упражнение 5 [★]: Переведите следующие примеры подстановок в безымянную форму, предполагая глобальный контекст Γ = a, b, и вычислите результаты подстановки по Определению 4. Соответствуют ли ответы исходному определению подстановки на обыкновенных термах из §5?

[b ↦ a] (b (λx.λy.b))
[b ↦ a (λz. a)] (b (λx.b))
[b ↦ a] (λb. b a)
[b ↦ a] (λa. b a)

Упражнение 6 [★★,¬→]: Покажите, что если s и t — n-термы, и j ≤ n, то [j ↦ s]t — n-терм.

Упражнение 7 [★,¬→]: Возьмите лист бумаги и, не глядя на определения подстановки и сдвига, сочините их заново.

Упражнение 8 [Рекомендуется,★★★]: Определение подстановки на безымянных термах должно быть согласовано с нашим неформальным определением подстановки на обыкновенных термах. (1) Какую теорему нужно доказать, чтобы строго обосновать это утверждение? (2) Докажите ее.

6.3 Вычисление

Единственное, что нам требуется сделать, чтобы определить отношение вычисления на безымянных термах — изменить правило бета-редукции, чтобы оно использовало нашу новую операцию подстановки (это единственное правило в старой системе, которое упоминает имена переменных).

Нетривиальная деталь состоит в том, что редукция редекса <<съедает>> связанную переменную: при редукции из ((λx.t₁₂)v₂ в [x ↦ v₂]t₁₂ связанная переменная x исчезает. Таким образом, переменные в результате подстановки надо перенумеровать, чтобы отразить тот факт, что x больше не является частью контекста. Например:

Точно так же, требуется сдвинуть переменные в v₂ перед подстановкой в t₁₂, поскольку терм t₁₂ определен в более крупном контексте, чем v₂. Собирая все эти соображения вместе, получаем правило бета-редукции такого вида:

Остальные правила остаются такими же, как и раньше (Рис. 5.3).

Упражнение 1 [★]: Нужно ли нам волноваться, что отрицательный сдвиг в правиле создаст неправомерные термы с отрицательными индексами переменных?

Упражнение 2 [★★★]: В исходной статье де Брауна содержалось два способа добиться безымянного представления термов: индексы де Брауна, которые нумеруют связывающие выражения <<изнутри наружу>>, и уровни де Брауна, которые нумеруют связывающие выражения <<снаружи внутрь>>. Например, терм λx. (λy. x y) x представляется индексами де Брауна в виде λ. (λ. 1 0) 0, а уровнями де Брауна в виде λ. (λ. 0 1) 0. Определите этот вариант с должной строгостью, и покажите, что представления термов с использованием индексов и уровней изоморфны (т. е., каждое из них можно однозначно восстановить, исходя из другого).

Chapter 7 Реализация лямбда-исчисления на ML

В этой главе мы конструируем интерпретатор для бестипового лямбда-исчисления, основываясь на интерпретаторе для арифметических выражений из Главы 4, а также на подходе к связыванию переменных и к подстановке из Главы 6.

Выполняемый вычислитель бестиповых лямбда-термов может быть получен путем простого перевода на OCaml определений из предыдущих глав. Как и в Главе 4, мы демонстрируем только базовые алгоритмы, игнорируя вопросы лексического и синтаксического анализа, ввода-вывода и тому подобные детали.¹

7.1 Термы и контексты

Тип данных, представляющий абстрактные синтаксические деревья для термов, можно получить путем прямого перевода Определения 2:

Представлением переменной является число — это индекс де Брауна. Представление абстракции содержит только терм для тела абстракции. Применение содержит два терма, один из которых применяется к другому.

Определение, которое реально используется в нашем интерпретаторе, впрочем, содержит несколько больше информации. Во-первых, как и раньше, полезно каждый терм снабдить элементом типа info, где записано, из какой позиции в файле терм был считан, чтобы программы распечатки ошибок могли направить пользователя (или даже пользовательский текстовый редактор, автоматически) к точному месту, где произошла ошибка.

Во-вторых, для целей отладки, полезно хранить в каждой вершине-переменной дполнительное число, для проверки целостности. Соглашение будет такое: в этом втором числовом поле всегда содержится полная длина контекста, где встретилась эта переменная.

Каждый раз при распечатке переменной мы будем проверять, что это число совпадает с реальной длиной контекста, где мы находимся; если это не так, значит, где-то мы забыли добавить операцию сдвига.

Последнее улучшение тоже относится к распечатке. Несмотря на то, что внутри термы представляются через индексы де Брауна, пользователю, они, очевидно, в таком виде показываться не должны: мы должны преобразовывать из обыкновенного представления в безымянное во время чтения, а во время распечатки преобразовывать термы обратно в обыкновенную форму. В этом нет ничего сложного, однако проделывать это совсем наивным образом не стоит (скажем, порождая для всех переменных совершенно новые имена), поскольку тогда имена связанных переменных в печатаемых термах будет никак не связан с именами из исходной программы. Можно справиться с этой трудностью, если хранить при каждой абстракции строку-подсказку об имени связанной переменной.

Основная работа с термами (в частности, подстановка) ничего интересного с этими строками проделывать не будет: они просто переносятся в результат в исходной форме, безо всякой заботы о совпадении имен, захвате переменных, и т. д. Когда программе распечатки требуется породить новое имя для связанной переменной, она сначала пытается использовать подсказку; если окажется, что это имя противоречит какому-либо имени, уже используемому в текущем контексте, процедура распечатки пытается породить похожее имя, добавляя штрихи, пока, в конце концов, не найдется имя, которое в текущем контексте никто не использовал. Такое правило обеспечивает, что напечатанный терм будет всегда очень похож на то, чего ожидает пользователь, с точностью до нескольких штрихов.

который представляет собой просто список строк и соответствующих им связываний. Пока что связывания совершенно тривиальны

и не несут никакой дополнительной информации. Однако позднее (в Главе 10) мы введем другие варианты в определение типа binding, и они будут отслеживать сведения о типе, связанном с переменной, и другую подобную информацию.

Процедура распечатки зависит также от нескольких низкоуровневых функций: pr выдает строку в стандартный поток вывода; ctxlength возвращает длину контекста; index2name находит строковое имя переменной по ее индексу. Самая интересная из этих функций, pickfreshname, принимает контекст ctx и имя-подсказку x, находит имя x’, похожее на x и не встречающееся в ctx, добавляет x’ к контексту ctx, получая при этом новый контекст ctx’, и возвращает пару, состоящую из x’ и ctx’.

Настоящая процедура печати в интерпретаторе untyped с веб-сайта книги выглядит несколько сложнее, поскольку принимает во внимание еще несколько деталей. Во-первых, она по возможности избегает печатать скобки, следуя соглашению, что применение право-ассоциативно, а тела абстракций простираются насколько возможно вправо. Во-вторых, она порождает форматные команды для низкоуровневого модуля красивой печати (OCaml-овской библиотеки Format), который принимает решения о переводах строк и отступах.

7.2 Сдвиг и подстановка

Определение сдвига (1) переводится на OCaml чуть ли не посимвольно.

Внутренний сдвиг ↑_c^d(t) здесь представлен вызовом внутренней функции walk c t. Поскольку d не меняется, нет нужды передавать ее в каждый вызов walk: когда нам это требуется в варианте с переменной внутри walk, мы просто используем внешнее связывание d. Сдвиг верхнего уровня ↑^d(t) представляется выражением termShift d t. (Заметим, что сама функция termShift не помечена как рекурсивная, поскольку единственное, что она делает — вызывает один раз walk.)

Подобным образом, функция подстановки получается почти напрямую из Определения 4:

Подстановка [j ↦ s]t терма s вместо переменной с номером j в терме t записывается здесь как termSubst j s t. Единственное отличие от исходного определения подстановки состоит в том, что весь сдвиг s мы производим сразу, в ветви TmVar, вместо того, чтобы сдвигать s на единицу каждый раз, когда проходим через связывание. При этом получается, что аргумент j во всех вызовах walk один и тот же, и мы можем опустить его во внутреннем определении.

Читатель может заметить, что определения termShift и termSubst весьма похожи, и отличаются только действием, производимым, когда процесс достигает переменной. Интерпретатор untyped, доступный на веб-сайте книги, использует эту похожесть и выражает как сдвиг, так и подстановку в качестве частных случаев более общей функции tmmap. Принимая терм t и функцию onvar, onmap выдает терм той же формы, что t, только каждая переменная заменяется результатом вызова onvar от этой переменной. Такой трюк в более крупных исчислениях избавляет нас от довольно большого количества повторений; подробности можно найти в §25.2.

В операционной семантике лямбда-исчисления единственное место, где используется подстановка — правило бета-редукции. Как мы уже замечали, это правило на самом деле проводит несколько операций: терм, подставляемый вместо связанной переменной, сначала сдвигается на единицу, а затем результат сдвигается на единицу вниз, чтобы отразить исчезновение использованной связанной переменной. Следующее определение описывает эту последовательность действий:

7.3 Вычисление

Как и в Главе 4, функция вычисления зависит от вспомогательного предиката isval:

Функция одношагового вычисления прямо кодирует правила вычисления, но при этом, помимо терма, принимает дополнительным аргументом контекст ctx. В нашей теперешней функции eval1 этот контекст не используется, но некоторые более сложные вычислители в последующих главах будут к нему обращаться.

Функция многошагового вычисления такая же, как раньше, за исключением аргумента ctx:

Упражнение 1 [Рекомендуется,★★★¬→]: Измените реализацию, чтобы она использовала стиль вычисления с <<большим шагом>>, введенный в Упражнении 17.

7.4 Дополнительные замечания

Реализация подстановок, представленная в этой главе, хотя и достаточна для целей нашей книги, но далека от идеала. В частности, правило бета-редукции в нашем интерпретаторе <<энергично>> подставляет значение аргумента вместо связанной переменной в теле процедуры. Интерпретаторы (и компиляторы) функциональных языков, где оптимизируется скорость, а не простота чтения кода, используют другую стратегию: вместо того, чтобы производить подстановку, они просто записывают информацию о связи между именем переменной и значением аргумента во вспомогательной структуре данных, называемой окружение, и эта структура передается вместе с вычисляемым термом. Достигая переменной, мы ищем ее значение в текущем окружении. Такую стратегию можно смоделировать, если рассматривать окружение как своего рода явную подстановку — т. е., перевести механизм подстановки из метаязыка в объектный язык, сделать его частью синтаксиса термов, с которыми работает вычислитель, а не внешней операцией на термах. Явные подстановки появились в исследовании Абади, Карделли, Куриена и Леви (Abadi, Cardelli, Curien and Lévy 1991a) и стали с тех пор активной областью исследований.

Если Вы что-то реализовали в программе, это еще не значит, что Вы это поняли. Брайан Кантвелл Смит

Chapter 8 Типизированные арифметические выражения

В Главе 3 мы с помощью простого языка булевских и арифметических выражений продемонстрировали основные инструменты для точного описания синтаксиса и вычислений. Теперь мы возвращаемся к этому языку и дополняем его статическими типами. Подобно Главе 3, сама по себе система типов совершенно тривиальна, однако она поможет нам познакомиться с понятиями, которые затем будут использоваться на протяжении всей книги.¹

8.1 Типы

Напомним синтаксис арифметических выражений:

В Главе 3 мы видели, что при вычислении терма может либо получиться значение…

Лекция	Тема	Материал

1.	Обзор курса; история; административные формальности	1, (2)
2.	Предварительная информация: синтаксис, операционная семантика	3, 4
3.	Введение в лямбда-исчисление	5.1, 5.2
4.	Формализация лямбда-исчисления	5.3, 6.7
5.	Типы; простое типизированное лямбда-исчисление	8, 9, 10
6.	Простые расширения; производные формы	11
7.	Дальнейшие расширения	11
8.	Нормализация	12
9.	Ссылки; исключения	13, 14
10.	Наследование	15
11.	Метатеория наследования	16, 17
12.	Императивные объекты	18
13.	Облегченная Java	19
14.	Рекурсивные типы	20
15.	Метатеория рекурсивных типов	21
16.	Метатеория рекурсивных типов	21
17.	Реконструкция типов	22
18.	Универсальный полиморфизм	23
19.	Экзистенциональный полиморфизм; АТД	24, (25)
20.	Ограниченная квантификация	26, 27
21.	Метатеория ограниченной квантификации	28
22.	Операторы над типами	29
23.	Метатеория F_ω	30
24.	Наследование высшего уровня	31
25.	Чисто функциональные объекты	32
26.	Лекция про запас

★	Контрольный вопрос	от 30 секунд до 5 минут
★★	Простое	≤ 1 час
★★★	Средней сложности	≤ 3 часа
★★★★	Тяжелое	> 3 часов

	Статическая проверка	динамическая проверка
Безопасные	ML, Haskell, Java и т. п.	Лисп, Scheme, Perl, Postscript и т. п.
Небезопасные	C, C++ и т. п.

1870-е	истоки формальной логики	Frege (1879)
1900-е	формализация математики	Whitehead and Russell (1910)
1930-е	бестиповое лямбда-исчисление	Church (1941)
1940-е	простое типизированное лямбда-исчисление	Church (1940), Curry and Feys (1958)
1950-е	Фортран	Backus (1981)
	Алгол-60	Naur et al. (1963)
1960-е	проект Automath	de Bruijn (1980)
	Симула	Birtwistle et al. (1979)
	соответствие Карри-Ховарда	Howard (1980)
	Алгол-68	van Wijngaarden et al. (1975)
1970-е	Паскаль	Wirth (1971)
	Теория типов Мартина-Лёфа	Martin-Löf (1973, 1982)
	Системы F, F^ω	Girard (1972)
	Полиморфное лямбда-исчисление	Reynolds (1974)
	CLU	Liskov et al. (1981)
	полиморфный вывод типов	Milner (1978), Damas and Milner (1982)
	ML	Gordon, Milner and Wadsworth (1979)
	типы-пересечения	Coppo and Dezani (1978)
		Coppo, Dezani and Sallé (1979), Pottinger (1980)
1980-е	проект NuPRL	Constable et al. (1986)
	наследование	Reynolds (1980), Cardelli (1984), Mitchell (1984a)
	АТД как экзистенциальные типы	Mitchell and Plotkin (1988)
	исчисление конструкций	Coquand (1985), Coquand and Huet (1988)
	линейная логика	Girard (1987), Girard et al. (1988)
	ограниченная квантификация	Cardelli and Wegner (1985)
		Curien and Ghelli (1992), Cardelli et al. (1994)
	Эдинбургская Логическая Конструкция	Harper, Honsell and Plotkin (1992)
	Forsythe	Reynolds (1985)
	чистые системы типов	Terlouw (1989), Berardi (1988), Barendregt (1991)
	зависимые типы и модульность	Burstall and Lampson (1984), MacQueen (1986)
	Quest	Cardelli (1991)
	системы эффектов	Giffod et al. (1987), Talpin and Jouvelot (1992)
	переменные строк; расширяемые записи	Wand (1987), Rémy (1989)
		Cardelli and Mitchell (1991)
1990-е	наследование высших порядков	Cardelli (1990), Cardelli and Longo (1991)
	типизированные промежуточные языки	Tarditi, Morrisett et al. (1996)
	исчисление объектов	Abadi and Cardelli (1996)
	полупрозрачные типы и модульность	Harper and Lillibridge (1994), Leroy (1994)
	типизированный язык ассемблера	Morrisett et al. (1998)

`t ::=`		термы:
	`x`	переменная
	`λx. t`	абстракция
	`t t`	применение

`t`	::=		термы:
		`true`	константа <<истина>>
		`false`	константа <<ложь>>
		`if t then t else t`	условное выражение
		`0`	константа <<ноль>>
		`succ t`	следующее число
		`pred t`	предыдущее число
		`iszero t`	проверка на ноль

	`id (id (λz.` `id z))`
→	`id` `(id (λz.z))`
→	`id (λz.z)`
→	`λz.z`
¬→

	`id (id (λz. id z))`
→	`id (λz. id z)`
→	`λz. id z`
→	`λz.z`
¬→

	`id` `(id (λz. id z))`
→	`id (λz. id z)`
→	`λz. id z`
¬→

	`test tru v w`
=	`(λl.` `λm.` `λn. l m b) tru` `v w`	по определению
→	`(λm.` `λn. tru m b) v` `w`	редукция подчеркнутого выражения
→	`(λn. tru v b) w`	редукция подчеркнутого выражения
→	`tru v w`	редукция подчеркнутого выражения
=	`(λt.` `λf. t) v` `w`	по определению
→	`(λf. v) w`	редукция подчеркнутого выражения
→	`v`	редукция подчеркнутого выражения

	`fst (pair v w)`
=	`fst ((λf.λs.λb. b f s) v` `w)`	по определению
→	`fst ((λs.λb. b v s) w)`	редукция подчеркнутого выражения
→	`fst (λb. b v w)`	редукция подчеркнутого выражения
=	`(λp. p tru) (λb. b v w)`	по определению
→	`(λb. b v w) tru`	редукция подчеркнутого выражения
→	`tru v w`	редукция подчеркнутого выражения
→^*	`v`	как показано ранее.

	`factorial c`₃
=	`fix g c`₃
→	`h h c`₃
	где `h =` `λx. g (λy. x x y)`
→	`g fct c`₃
	где `fct =` `λy. h h y`
→	`(λn. if realeq n c`₀
	`then c`₁
	`else times n (fct (prd n)))`
	`c`₃
→	`if realeq c`₃ `c`₀
	`then c`₁
	`else times c`₃ `(fct (prd c`₃`)))`
→^*	`times c`₃ `(fct (prd c`₃`))`
→^*	`times c`₃ `(fct c′`₂`)`
	где `c′`₂ поведенчески эквивалентен `c`₂
→^*	`times c`₃ `(g fct c′`₂`)`
→^*	`times c`₃ `(times c′`₂ `(g fct c′`₁`))`
	где `c′`₁ поведенчески эквивалентен `c`₁
	(те же шаги повторяются для `g fct c′`₂)
→^*	`times c`₃ `(times c′`₂`(times c′`₁ `(g fct c′`₀`)))`
	где `c′`₀ поведенчески эквивалентен `c`₀
	(таким же образом)
→^*	`times c`₃ `(times c′`₂`(times c′`₁ `(if realeq c′`₀ `c`₀`then c`₁
	`else …)))`
→^*	`times c`₃ `(times c′`₂ `(times c′`₁ `c`₁`))`
→^*	`c′`₆
	где `c′`₆ поведенчески эквивалентен `c`₆

[`x` ↦ `s`]`x`	=	`s`
[`x` ↦ `s`]`y`	=	`y`	если `y` ≠ `x`
[`x` ↦ `s`]`(λy. t`₁`)`	=	`λy.` `[x` `↦` `s]t`₁
[`x` ↦ `s`](`t`₁ `t`₂)	=	([`x` ↦ `s`]`t`₁) ([`x` ↦ `s`]`t`₂)

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

Бенджамин Пирс

Предисловие

Предполагаемая аудитория

Цели

Структура книги

Требуемая подготовка

Примерный план курса

Упражнения

Типографские соглашения

Электронные ресурсы

Благодарности

Chapter 1 Введение

1.1 Типы в информатике

1.2 Для чего годятся типы

1.2.1 Выявление ошибок

1.2.2 Абстракция

1.2.3 Документация

1.2.4 Безопасность языков

1.2.5 Эффективность

1.2.6 Другие приложения

1.3 Системы типов и проектирование языков

1.4 Краткая история

1.5 Дополнительная литература

Chapter 2 Математический аппарат

2.1 Множества, отношения и функции

2.2 Упорядоченные множества

2.3 Последовательности

2.4 Индукция

2.5 Справочная литература

Part I Бестиповые системы

Chapter 3 Бестиповые арифметические выражения

3.1 Введение

3.2 Синтаксис

3.3 Индукция на термах

3.4 Семантические стили

3.5 Вычисление

3.6 Дополнительные замечания

Chapter 4 Реализация арифметических выражений на языке ML

4.1 Синтаксис

4.2 Вычисление

4.3 Что осталось за кадром

Chapter 5 Бестиповое лямбда-исчисление

5.1 Основы

5.1.1 Абстрактный и конкретный синтаксис

5.1.2 Переменные и метапеременные

5.1.3 Область видимости

5.1.4 Операционная семантика

5.2 Программирование на языке лямбда-исчисления

5.2.1 Функции с несколькими аргументами

5.2.2 Булевские константы Чёрча

5.2.3 Пары

5.2.4 Числа Чёрча

5.2.5 Расширенное исчисление

5.2.6 Рекурсия

5.2.7 Представление

5.3 Формальности

5.3.1 Синтаксис

5.3.2 Подстановка

5.4 Операционная семантика

5.5 Дополнительные замечания

Chapter 6 Представление термов без использованиия имен

6.1 Термы и контексты

6.2 Сдвиг и подстановка

6.3 Вычисление

Chapter 7 Реализация лямбда-исчисления на ML

7.1 Термы и контексты

7.2 Сдвиг и подстановка

7.3 Вычисление

7.4 Дополнительные замечания

Part II Простые типы

Chapter 8 Типизированные арифметические выражения

8.1 Типы

Part I
Бестиповые системы

Part II
Простые типы