Пирс Б. Типы в языках программирования

Подождите немного. Документ загружается.

3.5. Вычисление 41

B N (бестиповое) Расширяет B (3.1)

Новый синтаксис

t ::= . . . термы:

0 константа ноль

succ t следующее число

pred t предыдущее число

iszero t проверка на ноль

v ::= . . . значения:

nv числовое значение

nv ::= . . . числовые значения:

0 константа ноль

succ nv значение-последователь

Новые правила вычисления t t

succ t

(E-Succ)

pred 0 0 (E-PredZero)

pred (succ nv

) nv

(E-PredSucc)

pred t

(E-Pred)

iszero 0 true (E-IszeroZero)

iszero (succ nv

) false (E-IszeroSucc)

iszero t

(E-IsZero)

Рис. 3.2. Арифметические выражения (NB)

1. Предположим, мы добавили к правилам на Рис. 3.1 еще одно:

if true then t

else t

(E-Funny)

Какие из теорем 3.5.4, 3.5.7, 3.5.8, 3.5.11 и 3.5.12 остаются истинными?

2. Теперь допустим, что мы добавляем такое правило:

if t

then t

else t

if t

then t

else t

(E-Funny2)

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

тельства?

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

Рис. 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.5.3 («одношаговое отношение вычис-

ления на арифметических выражениях есть наименьшее отношение, удовлетворяющее всем экземпля-

рам правил на Рис. 3.1 и 3.2. . . »). Чтобы не тратить место на такого рода служебные определения,

обычно считают, что правила вывода сами по себе представляют определение, а формулировка «наи-

меньшее отношение, содержащее все экземпляры. . . » подразумевается.

В этих правилах важную роль играет синтаксическая категория числовых значений (nv). Например,

в E-PredSucc требование, чтобы левая часть имела вид pred (succ nv

), а не просто pred (succ t

приводит к тому, что это правило нельзя использовать для перевода pred (succ (pred 0)) в pred 0,

поскольку для такого шага потребовалось бы заменить метапеременную nv

на терм pred 0, который

rev. 104

42 3.5. Вычисление

не является числовым значением. В результате единственный разрешенный шаг при вычислении терма

pred (succ (pred 0)) имеет дерево вывода

pred 0 0

E-PredZero

succ (pred 0) succ 0

E-Succ

pred (succ (pred 0)) pred (succ 0)

E-Pred

Упражнение 3.5.14 Покажите, что Теорема 3.5.4 верна и для отношения вычисления на ариф-

метических выражениях: если t t и t t , то t t .

Формализация операционной семантики языка заставляет нас указать поведение всех термов, вклю-

чая, в нашем теперешнем языке, термы вроде pred 0 и succ false. По правилам Рис. 3.2, предшеству-

ющее число от 0 определяется как 0. С другой стороны, последователь false не вычисляется никак

(другими словами, этот терм является нормальной формой). Такие термы мы называем тупиковыми.

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

чением.

Понятие «тупика» представляет ошибки времени выполнения в нашей простой машине. С интуитив-

ной точки зрения, оно описывает ситуации, когда операционная семантика не знает, что делать дальше,

поскольку программа оказалась в «бессмысленном» состоянии. В более конкретной реализации языка

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

адресу, попыткам выполнить запрещенную машинную команду и т. п. Мы объединяем все эти виды

неправильного поведения под единой вывеской «тупикового состояния».

Упражнение 3.5.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) доказать это. Как это часто бывает при изучении языков программирования,

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

само доказательство после этого построить нетрудно.

rev. 104

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

Упражнение 3.5.17 Рекомендуется,

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

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

отдельные шаги вычисления используются для переписывания частей терма, кусочек за кусочком,

пока в конце концов не получится значение. Поверх этого отношения мы определяем многошаговое

отношение вычисления, которое позволяет нам говорить о том, как термы (за много шагов) вычис-

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

(или, иногда, естественная семантика), прямо определяет понятие «терм такой-то при вычислении

дает такое-то значение», записываемое t v. Правила с большим шагом для нашего языка с булев-

скими и арифметическими выражениями выглядят так:

v v (B-Value)

true t

if t

then t

else t

(B-IfTrue)

false t

if t

then t

else t

(B-IfFalse)

succ t

succ nv

(B-Succ)

pred t

(B-PredZero)

succ nv

pred t

(B-PredSucc)

iszero t

true

(B-IszeroTrue)

succ nv

iszero t

false

(B-IszeroFalse)

Покажите, что семантика с малым шагом и с большим шагом для нашего языка дают один и тот

же результат, т. е., t v тогда и только тогда, когда t v.

Упражнение 3.5.18

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

ветви then и else в условном выражении вычислялись (в указанном порядке) до того, как вычис-

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

поведения.

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

Понятия абстрактного и конкретного синтаксиса, синтаксического анализа и т. п. объясняются в

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

доказательства по индукции рассмотрены более подробно в книгах Винскеля (Winskel 1993) и Хеннесси

(Hennessy 1990).

Стиль операционной семантики, которым мы здесь пользуемся, восходит к техническому докладу

Плоткина (Plotkin 1981). Стиль с большим шагом (3.5.17) был разработан Каном (Kahn 1987). Более

подробно они описаны у Астезиано (Astesiano 1991) и у Хеннесси (Hennessy 1990).

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

rev. 104

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

В.: Зачем доказывать свойства

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

Если в определениях нет

ошибок, доказательства почти

всегда получаются очень

скучными.

О.: В определениях почти

всегда есть ошибки.

Автор неизвестен

rev. 104

Глава 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-а делает эту задачу простой: следующее объявление — прямой перевод грамматики со стр. 29.

type term =

Tm True of info

| TmFalse of info

| TmIf of info * term * term * term

| TmZero of info

| TmSucc of info * term

| TmPred of info * term

| Tm IsZero of info * term

Конструкторы от TmTrue до TmIsZero называют различные виды вершин в синтаксических деревьях

типа term; тип, следующий за словом of, для каждого вида указывает количество поддеревьев, которые

будут подчиняться вершине данного вида.

Код из этой главы хранится в веб-репозитории http://www.cis.upenn.edu/~bcpierce/tapl под названием arith. Там

же можно найти инструкции по скачиванию и запуску интерпретаторов.

Разумеется, языковые вкусы бывают разные, и хороший программист способен работать с любым инструментом; Вы

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

занята программа проверки типов, ручное управление памятью (в особенности) утомительно и чревато ошибками.

46 4.2. Вычисление

Каждая вершина абстрактного синтаксического дерева снабжена значением типа info, которое опи-

сывает место (номер символа и имя файла), откуда происходит эта вершина. Эта информация создается

процедурой синтаксического анализа при чтении входного файла, и используется функциями распе-

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

вычисления, проверки типов и т. п., эту информацию можно было бы и вовсе не хранить; она включена

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

код точно в таком виде, как он напечатан в книге.

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

чением:

let rec i s n u m e r i c v a l t = match t with

Tm Zero (_) -> true

| TmSucc (_ , t1 ) -> isnumericval t1

| _ -> false

Это типичный пример OCaml-овского рекурсивного определения с сопоставлением: isnumericval

определяется как функция, которая, будучи вызвана с аргументом TmZero, воазвращает true; будучи

применена к TmSucc с поддеревом t1, вызывает себя рекурсивно с аргументом t1, чтобы проверить,

является ли он числовым значением; а будучи вызвана с любым другим аргументом, возвращает false.

Знаки подчеркивания в некоторых образцах — метки «неважно», они сопоставляются с любым термом,

который стоит в указанном месте; в первых двух предложениях с их помощью игнорируются аннотации

info, а в последнем предложении с ее помощью сопоставляется любой терм. Ключевое слово rec говорит

компилятору, что определение функции рекурсивно — т. е., что идентификатор isnumericval в теле

функции относится к самой функции, которую сейчас определеяют, а не к какой-либо более ранней

переменной с тем же именем.

Заметим, что ML-код в приведенном определении при верстке немного «украшен», как для просто-

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

настоящий символ стрелки , а не двухсимвольную последовательность ->. Полный список типограф-

ских соглашений можно найти на веб-сайте книги.

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

let rec isval t = match t with

Tm True (_) -> true

| TmFalse (_) -> true

| t when isnumericval t -> true

| _ -> false

В третьем предложении встречается «условный образец»: он сопоставляется с любым термом t, но

только если булевское выражение isnumericval t возвращает значение «истина».

4.2. Вычисление

Реализация отношения вычисления точно следует правилам одношагового вычисления из Рис. 3.1

и 3.2. Как мы видели, эти правила определяют частичную функцию, которая, будучи применена к

терму, не являющемуся значением, выдает следующий шаг вычисления этого терма. Если функцию

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

ния на OCaml нам нужно решить, как действовать в таком случае. Один очевидный вариант состоит в

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

если ни одно из правил невозможно применить к терму, полученному в качестве параметра. (Другой

способ действий был бы заставить вычислитель возвращать значение типа term option, которое бы по-

казывало, было ли вычисление успешным, и если да, то каков результат; это тоже работало бы, но

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

вать, если не применимо ни одно правило:

exc e p tion N o R u l e A p p l i e s

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

rev. 104

4.2. Вычисление 47

let rec eval1 t = match t with

TmIf (_ , TmTrue (_) , t2 , t3 ) ->

| TmIf (_ , TmFalse (_) , t2 , t3 ) ->

| TmIf ( fi ,t1 , t2 , t3 ) ->

let t1 ’ = eval1 t1 in

TmIf ( fi , t1 ’ , t2 , t3 )

| TmSucc ( fi , t1 ) ->

let t1 ’ = eval1 t1 in

Tm Succ (fi , t1 ’)

| TmPred (_ , TmZero (_ )) ->

Tm Zero ( dummyi n fo )

| TmPred (_ , TmSucc (_ , nv1 )) when ( isnumericval nv1 ) ->

nv1

| TmPred ( fi , t1 ) ->

let t1 ’ = eval1 t1 in

Tm Pred (fi , t1 ’)

| Tm IsZero (_ , TmZero ( _)) ->

Tm True ( dummyi n fo )

| Tm IsZero (_ , TmSucc (_ , nv1 )) when ( isnumericval nv1 ) ->

Tm False ( dummyinf o )

| Tm IsZero (fi , t1 ) ->

let t1 ’ = eval1 t1 in

TmI sZero ( fi , t1 ’)

| _ ->

raise NoRuleApplies

Заметим, что в нескольких местах мы собираем термы заново, а не переделываем уже существу-

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

info в них не имеют смысла. В таких термах мы используем константу dummyinfo. Для сопоставления с

аннотациями в образцах всегда используется переменная fi (ﬁle information, «информация о файле»).

Еще одна существенная деталь в определении eval1 — использование явных выражений when в об-

разцах, чтобы представить эффект имен метапеременных вроде v и nv в правилах, определяющих отно-

шение вычисления на Рис. 3.1 и 3.2. Например, в выражении для вычисления TmPred(_,TmSucc(_,nv1)),

семантика OCaml-овских образцов позволяет nv1 сопоставляться с каким угодно термом, а это не то,

чего мы хотим; добавление when (isnumericval nv1) ограничивает правило так, чтобы оно запускалось

только тогда, когда терм, соответствующий nv1, на самом деле является числовым значением. (Мы, в

принципе, могли бы переписать исходные правила вывода в таком же стиле, как образцы ML, переводя

неявные ограничения, основанные на именах метапеременных, в явные условия применения правил:

— числовое значение

pred (succ t

) t

(E-PredSucc)

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

Наконец, функция eval берет терм и находит его нормальную форму, применяя eval1 циклически.

Если eval1 возвращает новый терм t’, мы вызываем eval рекурсивно, чтобы продолжить вычисле-

ние, начиная с t’. Когда, наконец, eval1 достигнет состояния, где не применимо никакое правило, она

вызывает исключение NoRuleApplies. При этом eval вылетает из цикла и возвращает последний терм

последовательности.

let rec eval t =

Мы пишем eval таким образом из соображений читаемости, однако на самом деле помещать обработчик исключений

try внутрь рекурсивного цикла в ML не рекомендуется.

Упражнение 4.2.1 :

Почему? Как было бы правильнее написать eval?

rev. 104

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

try let t ’ = eval1 t

in eval t ’

with N o R u l e A p p l ie s -> t

Разумеется, наш простой вычислитель написан так, чтобы упростить сравнение с математическим

определением вычисления, а не так, чтобы находить нормальные формы как можно быстрее. Несколько

более эффективный алгоритм можно получить, если взять за основу правила вычисления «с большим

шагом», как предлагается в Упражнении 4.2.2.

Упражнение 4.2.2 Рекомендуется, :

Измените определение функции eval в программе arith, используя стиль с большим шагом из

Упражнения 3.5.17.

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

Разумеется, в любом интерпретаторе и компиляторе — даже в очень простом, — много модулей по-

мимо того, что мы обсудили здесь. На самом деле вычисляемые термы изначально хранятся в файлах

как последовательности символов. Их нужно считать из файловой системы, перевести в последователь-

ность лексем при помощи лексического анализатора, потом с помощью синтаксического анализатора

собрать из них абстрактные синтаксические деревья, и только тогда скормить функциям вычисления,

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

файловый ввод/вывод

символы

лексический анализ

лексемы

синтаксический анализ

термы

вычисление

значения

печать

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

rev. 104

Глава 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´arez 1989; Milner, Tofte, Harper and macQueen 1997),

Haskell (Hudak et al., 1992) или Scheme (Sussman and Steele 1975; Kelsey, Clinger and Rees 1998). Как

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

системы типов.

Примеры из этой главы являются термами чистого бестипового лямбда-исчисления, λ (см. Рис. 5.3), либо лямбда-

исчисления с добавлением булевских значений и арифметических операций, λNB (3.2). Соответствующая реализация на

OCaml называется fulluntyped.

50 5.1. Основы

5.1. Основы

Процедурная (или функциональная) абстракция является ключевым свойством почти всех языков

программирования. Вместо того, чтобы переписывать одно и то же вычисление раз за разом, мы пишем

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

или нескольких именованных параметров, а затем при необходимости вызываем эту процедуру, в каж-

дом случае задавая значения параметров. К примеру, для программиста естественно взять длинное

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

(5*4*3* 2 * 1 ) + ( 7 * 6 * 5 *4 * 3 * 2 * 1 ) - (3*2*1 )

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

fac t o rial ( n ) = if n =0 then 1 else n * fac t o rial (n -1)

Для каждого неотрицательного числа n подстановка аргумента n в функцию factorial дает в ре-

зультате факториал n. Если мы будем писать «λn. ...» как сокращение для «функция, которая, для

каждого n, дает . . . », то определение factorial можно переформулировать как

fac t o rial = λn . if n =0 then 1 else n * fac t orial (n -1)

Теперь 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

— третий вид термов. Эти способы построения термов выражаются следующей грамматикой:

t ::= термы:

x переменная

λx. t абстракция

t t применение

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

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

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

структуры. Конкретный (или поверхностный) синтаксис языка относится к строкам символов, кото-

рые читают и пишут программисты. Абстрактный синтаксис — это намного более простое внутреннее

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

деревья или АСД ). Представление в виде дерева делает структуру термов непосредственно очевид-

ной, и поэтому его естественно использовать для сложной обработки, которая нужна как при строгом

определении языков (и доказательстве их свойств), так и внутри компиляторов и интерпретаторов.

Преобразование из конкретного в абстрактный синтаксис происходит в два этапа. Сначала лексиче-

ский анализатор (или лексер) переводит последовательность символов, написанных программистом, в

последовательность лексем — идентификаторов, ключевых слов, комментариев, символов пунктуации,

и т. п. Лексический анализатор убирает комментарии и решает вопросы, связанные с пробельными сим-

волами, соглашениями о больших/маленьких буквах, а также форматах для числовых и символьных

Выражение лямбда-терм относится ко всем термам лямбда-исчисления. Лямбда-термы, которые начинаются с λ,

часто называют лямбда-абстракциями.

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

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

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

часто называют внутренним языком, а полный язык, который включает в себя все производные формы, называет-

ся внешним языком. Трансформация из внешнего языка во внутренний выполняется (по крайней мере, концептуально)

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

rev. 104