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

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

3.2. Синтаксис 31

Результатом вычислений служат термы некоторого простого вида: это всегда будут либо булевские

константы, либо числа (вложенные вызовы succ ноль или более раз с аргументом 0). Такие термы

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

термов.

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

true или if 0 then 0 else 0. Мы поговорим о таких термах позднее — в сущности, именно их наличие

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

бессмысленных программ, которых мы хотим избегать при помощи системы типов.

3.2. Синтаксис

Есть несколько эквивалентных способов определить синтаксис нашего языка. Один из них мы уже

видели — это грамматика на странице 29. Грамматика эта, в сущности, всего лишь сокращенная форма

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

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

такое, что:

1. true, false, 0 T ;

2. если t

T , то succ t

, pred t

, iszero t

T ;

3. если t

T , t

T , то if t

then t

else t

T .

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

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

пункт говорит нам, какие простые выражения содержатся в T . Второй и третий пункты указывают

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

жатся в T . Наконец, слово «наименьшее» говорит, что в T нет никаких элементов, кроме требуемых

этими тремя пунктами.

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

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

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

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

Еще один способ представить то же индуктивное определение термов использует двумерную запись

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

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

ми правилами:

true T false T 0 T

succ t

pred t

iszero t

T t

if t

then t

else t

Первые три правила повторяют первый пункт Определения 3.2.1; остальные четыре соответствуют

пунктам (2) и (3). Каждое правило вывода читается так: «Если мы установили истинность предпо-

сылок, указанных над чертой, то мы можем вывести заключение под чертой». Утверждение, что T

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

лано и здесь).

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

три в нашем определении) часто называют аксиомами. В этой книге термин правило вывода исполь-

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

rev. 104

32 3.2. Синтаксис

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

ли выражаться абсолютно точно, наши «правила вывода» на самом деле представляют собой схемы

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

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

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

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

термы.

Наконец, то же самое множество термов можно определить и еще немного по-другому, в более

«конкретном» стиле, явно указав процедуру порождения элементов T .

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

множество S

i 1

true, false, 0

succ t

, pred t

, iszero t

if t

then t

else t

, t

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

пусто; S

содержит только константы; S

содержит константы и выражения, которые можно по-

строить из констант путем применения одной из конструкций succ, pred, iszero или if; S

содержит

все эти выражения плюс те, которые можно построить за одно применение succ, pred, iszero или if

к членам S

; и так далее. S собирает все эти выражения вместе — т. е., все выражения, которые можно

получить применением конечного числа арифметических и условных операторов, начиная с констант.

Упражнение 3.2.4 : Сколько элементов содержит S

Упражнение 3.2.5 : Покажите, что множества S

кумулятивны — то есть, для любого i вы-

полняется S

i 1

Рассмотренные нами определения характеризуют одно и то же множество термов с разных направ-

лений: Определения 3.2.1 и 3.2.2 просто описывают множество как наименьшее, имеющее некоторые

«свойства замыкания»; Определение 3.2.3 показывает, как построить множество в виде предела по-

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

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

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

различные его части соотносятся друг с другом.

Утверждение 3.2.6 T S.

Доказательство: T определяется как наименьшее множество, удовлетворяющее некоторым услови-

ям. Таким образом, достаточно показать, что (а) эти условия выполняются на S; и (б) что любое

множество, удовлетворяющее условиям, содержит S как подмножество (т. е, что S — наименьшее

множество, удовлетворяющее условиям).

В части (а) нам требуется проверить, что все три условия из Определения 3.2.1 выполняются

на S. Во-первых, поскольку S

true, false, 0 , ясно, что S содержит константы. Во-вторых,

если t

S, то, поскольку S

, должно иметься какое-то i, такое, что t

. Но тогда,

по определению S

i 1

, мы имеем succ t

i 1

, а следовательно, succ t

S; подобным образом,

pred t

S и iszero t

S. В-третьих, при помощи аналогичного рассуждения, если t

S, t

и t

S, то if t

then t

else t

Для части (б) предположим что некоторое множество S удовлетворяет всем трем условиям из

Определения 3.2.1. При помощи полной индукции по i мы докажем, что все S

S , откуда следует,

что S S .

Допустим, что S

S для всех j i; мы должны показать, что S

S . Поскольку определение

состоит из двух пунктов (для i 0 и i 0), требуется рассмотреть два случая. Если i 0,

то S

; тогда, тривиальным образом, S . В противном случае, i j 1 для некоторого

rev. 104

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

j. Пусть t будет некоторым элементом S

j 1

. Поскольку S

j 1

определяется как объединение трех

меньших множеств, требуется рассмотреть три возможных случая. (1) Если t — константа, то

t S по условию 1. (2) Если t имеет вид succ t

, pred t

или iszero t

, для некоторого t

то, по предположению индукции, t

S , и тогда, по условию 2, t S . (3) Если t имеет вид if t

then t

else t

для некоторых t

, t

, то, опять же, согласно предположению индукции, t

и t

все содержатся в S , и, по условию 3, в нем содержится и t.

Таким образом, мы показали, что все S

S . Поскольку S определено как объединение всех S

, мы

имеем S S , и наше доказательство закончено.

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

а не более привычный образец «базовый случай / шаг индукции». Для каждого i мы предполагаем,

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

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

случай i 0 – это то, что множество чисел, меньших, чем i, для которых мы можем использовать

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

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

«структурной индукции».

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

Явная характеризация множества термов T в Утверждении 3.2.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. Это наблюдение можно использовать двумя способами: Во-первых, мы можем строить

индуктивные определения функций, действующих на множестве термов, и, во-вторых, мы можем да-

вать индуктивные доказательства свойств термов. Например, вот индуктивное определение функции,

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

Определение 3.3.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

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

— его размер.

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

size true 1

size false 1

size 0 1

size succ t

size t

size pred t

size t

size iszero t

size t

size if t

then t

else t

size t

Таким образом, размер t — это число вершин в его абстрактном синтаксическом дереве. Подобным

rev. 104

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

образом, глубина терма t, записываемая depth t , определяется так:

depth true 1

depth false 1

depth 0 1

depth succ t

depth t

depth pred t

depth t

depth iszero t

depth t

depth if t

then t

else t

max depth t

, depth t

Другое, эквивалентное, определение, таково: depth t — это наименьшее такое i, что t S

согласно

Определению 3.2.1.

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

(Само свойство, разумеется, совершенно очевидно. Интерес представляет форма индуктивного рассуж-

дения. Мы ее еще неоднократно встретим.)

Лемма 3.3.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

size t

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

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

о термах.

Теорема 3.3.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.

rev. 104

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

Структурная индукция:

Если для каждого терма s,

предполагая P r для всех непосредственных подтермов s, мы можем

доказать P s ,

то P s выполняется для всех s.

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

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

(2.4.2). Обыкновенная структурная индукция соответствует принципу обыкновенной индукции на на-

туральных числах (2.4.1), где шаг индукции требует, чтобы P n 1 выводилось исключительно из

предположения P n .

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

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

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

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

предпочитают структурную индукцию, поскольку в таком случае работа ведется прямо с термами, без

промежуточного обращения к числам.

Большинство доказательств по индукции на термах имеет одну и ту же структуру. На каждом шаге

индукции нам дается терм t, для которого нам нужно продемонстрировать некоторое свойство P , в

предположении, что P выполняется на всех его подтермах (или на всех термах меньшего размера). Мы

делаем это путем рассмотрения всех возможных форм, которые t может иметь (true, false, 0, условное

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

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

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

доказательств, и записывать их таким образом:

Доказательство: индукция по t:

Вариант: t true

. . . доказываем P true . . .

Вариант: t false

. . . доказываем P false . . .

Вариант: t if t

then t

else t

. . . доказываем P if t

then t

else t

, используя P t

, P t

и P t

. . .

(И так же для остальных синтаксических форм.)

Во многих индуктивных доказательствах (включая 3.3.3) даже такой уровень подробности чрез-

мерен: в базовых случаях (для термов t, не имеющих подтермов) P t ясно непосредственно, а в ин-

дуктивных случаях P t выводится путем применения индуктивного предположения к подтермам t и

сочетания результатов некоторым очевидным способом. Для читателя оказывается проще воссоздать

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

чем прочитать явно записанные шаги. В таких ситуациях запись «индукция по t» в качестве доказа-

тельства более чем приемлема.

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

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

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

ствует три основных подхода к формализации семантики:

1. Операционная семантика специфицирует поведение языка программирования, определяя для

него простую абстрактную машину. Машина эта «абстрактна» в том смысле, что в качестве

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

rev. 104

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

микропроцессора. Для простых языков состояние машины представляет собой просто терм, а

поведение ее определяется функцией перехода, которая для каждого состояния либо указывает

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

остановившейся. Значением терма t объявляется конечное состояние, которого машина достигает,

будучи запущена с начальным состоянием t.

Иногда полезно дать для одного и того же языка несколько различных операционных семантик

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

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

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

машин при выполнении одной и той же программы в каком-то смысле соответствуют друг другу,

представляет собой доказательство правильности реализации языка.

2. Денотационная семантика смотрит на значение с более абстрактной точки зрения: в качестве

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

тический объект, скажем, число или функция. Построение денотационной семантики для языка

представляет собой нахождение некоторого набора семантических доменов, а также определение

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

подходящих семантических доменов для моделирования различных языковых особенностей при-

вел к возникновению изящной и богатой области исследований, известной как теория доменов.

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

от мелких деталей выполнения программы и концентрирует внимание на основных понятиях

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

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

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

спецификации. Наконец, из свойств выбранного набора семантических доменов часто немедленно

ясно, что некоторые (желательные или нежелательные) вещи в языке невозможны.

3. Аксиоматическая семантика подходит к этим законам напрямую: вместо того, чтобы снача-

ла определить поведение программ (с помощью операционной или денотационной семантики), а

затем строить законы, соответствующие этому поведению, аксиоматические методы принимают

сами законы в качестве определения языка. Значение терма — это то, что о нем можно доказать.

Красота аксиоматических методов в том, что они концентрируют внимание на процессе рассуж-

дений о программах. Именно эта традиция мышления обогатила информатику такими мощными

инструментами, как инварианты.

В 60-е и 70-е годы считалось, что операционная семантика уступает двум другим стилям, что с

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

лом она менее изящна и слаба с математической точки зрения. Однако в 80-е годы более абстрактные

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

и простота и гиб-

кость операционной семантики стали по сравнению с ними выглядеть все более привлекательными —

особенно в свете новых достижений, начиная со Структурной Операционной Семантики Плоткина

(Plotkin 1981), Естественной Семантики Кана (Kahn 1987) и работ Милнера по Исчислению Взаимо-

действующих Систем (Calculus of Communicating Systems, CCS; Milner 1980, 1989, 1999). Эти работы

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

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

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

в качестве средства для определения языков программирования и изучения их свойств. Именно она

используется в этой книге.

Строго говоря, то, что мы здесь описываем, — это так называемая операционная семантика с малым шагом, извест-

ная также как структурная операционая семантика (Plotkin 1981). В Упражнении 3.5.17 вводится альтернативный стиль

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

машины сразу вычисляет окончательное значение терма.

Для денотационной семантики камнем преткновения оказались недетерминистские вычисления и параллелизм; для

аксиоматической семантики — процедуры.

rev. 104

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

B (бестиповое)

Синтаксис

t ::= термы:

true константа «истина»

false константа «ложь»

if t then t else t условное

выражение

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

true константа «истина»

false константа «ложь»

Вычисление t t

if true then t

else t

(E-IfTrue)

if false then t

else t

(E-IfFalse)

if t

then t

else t

if t

then t

else t

(E-If)

Рис. 3.1. Булевские выражения (B)

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

Забудем на время о натуральных числах и рассмотрим операционную семантику только булевских

выражений. Определение приведено на Рис. 3.1. Рассмотрим его в деталях.

В левом столбце Рис. 3.1 содержится грамматика, в которой определяются два вида выражений. Во-

первых, повторяется (для удобства) синтаксис термов. Во-вторых, определяется подмножество термов

— множество значений, возможных результатов вычисления. В нашем случае значениями являются

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

В правом столбце определяется отношение вычисления

на термах. Оно записывается t t и

читается «t переходит в t за один шаг вычисления». Интуитивно, если в какой-то момент абстрактная

машина находится в состоянии t, то она может произвести шаг вычисления и перейти в состояние t .

Это отношение определяется тремя правилами вывода (или, если хотите, двумя аксиомами и одним

правилом: первые два правила не имеют предпосылок).

Первое правило, E-IfTrue, говорит, что, если вычисляется условное выражение, где условием слу-

жит константа true, то машина может выкинуть это условное выражение, оставив истинную ветвь t

качестве состояния (т. е., следующего подлежащего вычислению терма). Подобным образом, E-IfFalse

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

ложную ветвь t

. Символ E- в названиях этих правил напоминает, что они являются частью отношения

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

Третье правило вычисления, E-If, представляет больше интереса. Оно говорит, что, если условие

переходит за шаг в 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 ( if false then false else false ) else true

не переходит в if true then false else true. Единственный разрешенный нам шаг — вычислить

сначала внешнее условное выражение, используя E-IfTrue. Такое взаимодействие между правилами

определяет конкретную стратегию вычисления для условных выражений, соответствующую привыч-

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

ражение, нужно вычислить его условие; если условие само является условным выражением, требуется

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

рианта «с большим шагом», который описан в Упражнении 3.5.17 и напрямую сопоставляет термам их окончательные

значения.

rev. 104

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

вычислить его условие; и так далее. Правила E-IfTrue и E-IfFalse говорят нам, что нужно делать,

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

ностью вычислено. В некотором смысле, E-IfTrue и E-IfFalse проделывают работу по вычислению,

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

рактер этих правил подчеркивают, называя E-IfTrue и E-IfFalse рабочими правилами, в то время

как E-If является правилом соответствия.

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

вычисления так:

Определение 3.5.1 Экземпляр правила вывода получается при замене каждой метапеременной одним

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

Например,

if true then true else ( if false then false else false ) true

является экземпляром правила E-IfTrue, где оба вхождения t

заменяются на true, а t

заменяется

на if false then false else false.

Определение 3.5.2 Правило выполняется на бинарном отношении между термами, если, для каждого

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

не является.

Определение 3.5.3 Одношаговое отношение вычисления есть наименьшее бинарное отношение на

термах, на котором выполняются все три правила с Рис. 3.1. Если пара t, t является членом

этого отношения, мы говорим, что утверждение (или суждение) о вычислении t t выводимо.

Значение слова «наименьшее» в этом определении таково: утверждение t t выводимо тогда и

только тогда, когда оно обеспечено правилами: либо это экземпляр одной из аксиом E-IfTrue или

E-IfFalse, либо это заключение экземпляра правила E-If с выводимой предпосылкой. Выводимость

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

IfTrue и E-IfFalse, а внутренними вершинами экземпляры правила E-If. Например, если мы введем

сокращения

def

if true then false else false

def

if s then true else true

def

if false then true else true

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

if t then false else false if u then false else false

можно обосновать при помощи дерева

s false

E-IfTrue

t u

E-If

if t then false else false if u then false else false

E-If

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

ствительно, деревья вывода, обосновывающие утверждения о вычислении, всегда будут иметь такую

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

в дереве вывода взяться неоткуда. Наша терминология окажется более осмысленной, когда рассмот-

рение дойдет до других индуктивно определенных отношений, например, типизации — там некоторые

правила могут иметь более одной предпосылки.

То, что утверждение о вычислении t t выводимо тогда и только тогда, когда существует дерево

вывода с t t в корне, часто оказывается полезным при исследовании свойств отношения вычисления.

В частности, это немедленно подсказывает метод доказательства, называемый индукция по выводам.

Доказательство следующей теоремы может служить иллюстрацией.

rev. 104

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

Теорема 3.5.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

, однако, как мы

уже заметили, 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 может быть только E-If, откуда ясно, что t имеет вид if t

then t

else

(это нам уже и так известно), и что для некоторого t

выполняется t

. Но тогда мы

можем применить предположение индукции (поскольку деревья вывода t

и t

являются

поддеревьями выводов t t и t t соответственно) и заключить t

. Отсюда видно, что

t if t

then t

else t

if t

then t

else t

t , как нам и требуется.

Упражнение 3.5.5 Сформулируйте, в стиле Теоремы 3.3.4, принцип индукции, используемый в

приведенном выше доказательстве.

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

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

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

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

Определение 3.5.6 Терм t находится в нормальной форме, если к нему не применимо никакое правило

вычисления — т. е., если не существует такого t , что t t . (В качестве сокращения мы иногда

будем говорить «t является нормальной формой» вместо «t является термом в нормальной форме».)

Мы уже заметили, что в нашей текущей системе true и false — нормальные формы (поскольку

во всех правилах вычисления левые части являются условными выражениями, очевидно, невозмож-

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

обобщить это наблюдение как свойство всех значений:

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

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

ми конструкциями, мы всегда будем следить, чтобы Теорема 3.5.7 оставалась истинной: быть в нормаль-

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

испорчено.

В нашей теперешней системе верно и обратное утверждение: всякая нормальная форма есть значе-

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

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

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

rev. 104

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

Теорема 3.5.8 Если t находится в нормальной форме, то t — значение.

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

на t легко показать, что t — не нормальная форма.

Поскольку t не значение, он должен иметь вид if t

then t

else t

для некоторых t

, t

Рассмотрим возможные формы t

Если t

true, то, очевидно, t не является нормальной формой, поскольку он подпадает под

левую часть правила E-IfTrue. Так же и с t

false.

Если t

не равен ни true, ни false, то он не является значением. В таком случае применимо

предположение индукции, и оно говорит, что t

— не нормальная форма, а именно, что существует

некий терм t

, такой, что t

. Но тогда мы можем применить правило E-If, получая t

if t

then t

else t

. Таким образом, t не нормальная форма.

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

между состояниями. Для этого мы определяем отношение многошагового вычисления, которое сопо-

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

Определение 3.5.9 Отношение многошагового вычисления — это рефлексивно-транзитивное за-

мыкание отношения (одношагового) вычисления. То есть, это наименьшее отношение, такое, что

(1) если t t , то t t , (2) для всех t выполняется t t, и (3) если t t и t t , то

t t .

Упражнение 3.5.10 Переформулируйте Определение 3.5.9 в виде набора правил вывода.

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

ний вроде следующего:

Теорема 3.5.11 Единственность нормальных форм Если t u и t u’, причем и u, и u’ —

нормальные формы, то u u’.

Доказательство: Теорема следует из детерминированности одношагового вычисления (3.5.4).

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

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

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

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

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

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

Большинство доказательств гарантии завершения в информатике имеют одну и ту же базовую

структуру.

Сначала мы выбираем некоторое вполне упорядоченное множество S и функцию f , пере-

водящую «машинные состояния» (в нашем случае — термы) в элементы S. Затем мы показываем, что

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

f t f t . Теперь мы можем заметить, что бесконечная цепочка шагов вычисления, начинающаяся

с t, может быть переведена в бесконечную убывающую последовательность элементов S. Поскольку S

вполне упорядочено, такая бесконечная убывающая цепочка существовать не может, а, соответствен-

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

мерой завершения отношения вычисления.

Теорема 3.5.12 Завершение вычислений Для каждого терма t существует нормальная форма

t , такая, что t t .

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

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

является полным.

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

В Главе 12 мы увидим доказательство завершения с несколько более сложной структурой.

rev. 104