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

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

Приложение A

Решения избранных упражнений

3.2.4. Решение: S

i 1

3 3, а S

0. Таким образом, S

59439.

3.2.5. Решение: Достаточно простого доказательства по индукции. При i 0 утверждение очевидно.

При i j 1, для некоторого j 0, мы предполагаем S

, и должны доказать, что S

i 1

—

а именно, для каждого терма t S

требуется показать t S

i 1

. Итак, допустим t S

. Поскольку

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

форм:

1. t true, false, 0 . В этом случае, очевидно, t S

i 1

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

i 1

2. t succ t

, pred t

или iszero t

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

. Поскольку по предположению ин-

дукции S

, мы имеем t

, и, таким образом, по определению S

i 1

, t S

i 1

3. t if t

then t

else t

, где t

, t

. Опять же, поскольку, по предположению индукции,

, имеем t S

i 1

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

i 1

3.3.4. Решение: (Мы приводим доказательство только для принципа индукции по глубине; два других

доказательства строятся аналогично.) Нам известно, что, для любого терма s, если P r для всех

r, s, то P s ; требуется показать, что P s выполняется для всех s. Определим новый предикат Q на

натуральных числах:

Q n s, где depth s n.P s

Теперь при помощи индукции на натуральных числах (2.4.2) доказываем Q n для всех n.

3.5.5. Решение: Допустим, P — предикат на деревьях вывода утверждений о вычислениях.

Если для каждого дерева вывода D,

предполагая P C для всех непосредственных поддеревьев C,

мы можем доказать P D ,

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

3.5.10. Решение:

t t

t t t t

t t

3.5.13. Решение: (1) 3.5.4 и 3.5.11 перестают работать. 3.5.7, 3.5.8 и 3.5.12 сохраняются. (2) Теперь

ломается только 3.5.4; остальные теоремы остаются истинными. Во втором варианте интересно то, что,

381

382

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

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

все дороги ведут в Рим. Доказательство этого утверждения не так уж сложно, хотя уже не настолько

тривиально, как раньше. Главное наблюдение состоит в том, что одношаговое вычисление обладает так

называемым свойством ромба:

Лемма A.0.1 Свойство ромба

Если r s и r t, где s t, то существует терм u, такой, что s u и t u.

Доказательство: Из правил вычисления ясно, что описываемая ситуация может возникнуть,

только если r имеет вид if r

then r

else r

. Доказательство ведется по индукции на паре де-

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

шага в каждом выводе.

Вариант i:

Допустим, r s по E-IfTrue, а r t по E-Funny2. Тогда, исходя из формы этих правил, мы

знаем, что s r

, и что t if true then r

else r

, где r

. Но тогда выбор u r

дает нам

требуемое, поскольку мы знаем, что s r

, и видим, что t r

по правилу E-IfTrue.

Вариант ii:

Допустим, последнее правило в выводе как r s, так и r t — E-If. Из формы E-If мы знаем, что

s имеет вид if r

then r

else r

, а t имеет вид if r

then r

else r

, где r

и r

Но тогда, по предположению индукции, имеется терм r

, такой, что r

и r

. В таком

случае мы можем завершить рассуждение, взяв u if r

then r

else r

и заметив, что s u

и t u по правилу E-If.

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

Доказательство единственности результатов теперь можно провести стандартным методом «стяги-

вания диаграммы». Допустим, r s и r t.

}

. . .

}}

{

. . .

Тогда, используя Лемму A.0.1, мы можем «стянуть вместе» s

и t

}}

}

. . .

}}

{

. . .

rev. 104

383

затем стянуть попарно s

с u

и u

с t

}}

}

}}

. . .

}}

{

. . .

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

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

Отсюда следует, что, если при вычислении r могут получиться значения v и w, то они должны

совпадать (как v, так и w являются нормальными формами, так что единственный способ, чтобы они

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

3.5.14. Решение: Индукция по структуре t.

Вариант: t — значение.

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

Вариант: t succ t

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

вывести t t и t t — правило E-Succ (во всех остальных правилах внешний конструктор левой

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

ями вида t

и t

. По предположению индукции (которое применимо здесь, поскольку t

—

подтерм t), имеем t

. Но тогда succ t

succ t

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

Вариант: t pred t

В этом случае есть три различных правила вычисления (E-Pred, E-PredZero и E-PredSucc), ко-

торые могли бы быть использованы при редукции t к t и t . Заметим, однако, что правила эти не

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

ет левым частям остальных. (Например, если t соответствует E-Pred, значит, t

точно не является

значением, в частности, оно не равно 0 или succ v.) Это дает нам основание считать, что для вывода

t t и t t использовалось одно и то же правило. Если правило было E-Pred, мы, как и в преды-

дущем варианте, используем предположение индукции. Если это было E-PredZero или E-PredSucc,

результат следует непосредственно.

Остальные варианты:

Аналогично.

3.5.16. Решение: Пусть метапеременная t обозначает терм нового вида, включая wrong (а так-

же термы, где wrong встречается как подвыражение), а g обозначает терм исходного вида, где wrong

встретиться не может. Мы будем использовать запись t

t для нового отношения вычисления, ку-

да добавлены правила для wrong, а g

g для старой формы вычисления. Теперь мы можем точно

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

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

wrong, и наоборот. Формально:

Утверждение A.0.2 Для всех термов исходного вида, g, (1) g

v тогда и только тогда, когда g

v, и (2) (g

g , где g находится в тупике) тогда и только тогда, когда (g

wrong).

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

правила не отменяют Теорему 3.5.14:

rev. 104

384

Лемма A.0.3 Расширенное отношение вычисления детерминированно.

Это означает, что во всех случаях, когда g переводится в g в исходной семантике, оно может пере-

вестись в g и в расширенной семантике, и, более того, g — единственный терм, в который g может

перейти в новой семантике.

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

то в расширенной семантике его вычисление приведет к wrong.

Лемма A.0.4 Если g тупиковый терм, то g

wrong.

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

Вариант: g true, false или 0

Такого быть не может (мы предположили, что g тупиковый).

Вариант: g if g

then g

else g

Поскольку g тупиковый, g

должен находиться в нормальной форме (иначе можно было бы приме-

нить E-If). Понятно, что g

не может быть true или false (иначе применимы были бы E-IfTrue

либо E-IfFalse, и g не был бы тупиковым). Рассмотрим оставшиеся варианты:

Подвариант: g

if g

then g

else g

Поскольку g

находится в нормальной форме и при этом, очевидно, не является значением,

он в тупике. Предположение индукции говорит нам, что g

wrong. Отсюда мы можем

построить вывод g

if wrong then g

else g

. Добавляя к этому выводу экземпляр

правила E-If-Wrong, получаем g

wrong, как и требуется.

Подвариант: g

succ g

Если g

является числовым значением, то g

представляет собой badbool, и правило E-

If-Wrong немедленно приводит к g

wrong. В противном случае, по определению, g

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

wrong. На осно-

вании этого вывода можно построить вывод g

if wrong then g

else g

. Добавляя к

нему экземпляр E-If-Wrong, получаем g

wrong.

Другие подварианты:

Аналогично.

Вариант: g succ g

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

находится в нормальной форме,

но не является числовым значением. Есть две возможности: либо g

равен true или false, либо g

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

немедленно приводит к g

wrong; во втором, предположение индукции дает нам g

wrong, и мы

рассуждаем, как раньше.

Остальные варианты:

Аналогично.

Леммы A.0.3 и A.0.4 вместе дают нам направление «только тогда, когда» ( ) части (2) Утвержде-

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

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

вым.

Лемма A.0.5 Если g

t в расширенной семантике, и t содержит в качестве подтерма wrong, то в

исходной семантике g находится в тупике.

Доказательство: несложная индукция на (расширенных) деревьях вывода вычислений.

Сочетая это утверждение с Леммой A.0.3, мы получаем направление «тогда» ( ) Утвержде-

ния A.0.2, часть (2), и доказательство закончено.

3.5.17. Решение: Мы доказываем два направления «тогда и только тогда» по отдельности, в Утвержде-

ниях A.0.7 и A.0.9. В каждом случае, мы начинаем с доказательства технической леммы, сообщающей

нам некоторое полезное свойство вычисления с большим/малым шагом.

rev. 104

385

Лемма A.0.6 Если t

, то if t

then t

else t

if t

then t

else t

(и аналогичным

образом для других конструкторов).

Доказательство: Простая индукция.

Утверждение A.0.7 Если t v, то t v.

Доказательство: Индукция по выводу t v, с разбором вариантов по последнему использованному

правилу.

Вариант B-Value: t v

Утверждение следует непосредственно.

Вариант B-IfTrue: t if t

then t

else t

true

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

true. По Лемме A.0.6,

if t

then t

else t

if true then t

else t

По правилу E-IfTrue, if true then t

else t

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

v. Нуж-

ный нам результат следует из транзитивности .

Остальные сучаи подобны этому.

Лемма A.0.8 Если

if t

then t

else t

то либо t

true и t

v, либо t

false и t

false. Более того, последовательности

вычисления для t

и t

либо t

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

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

Доказательство: Индукция по длине исходной последовательности вычисления. Поскольку условное

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

Проведем разбор вариантов последнего правила, использованного на этом шаге (это должно быть

одно из If-правил).

Вариант E-If: if t

then t

else t

if t

then t

else t

t t

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

true и t

v, либо t

false и t

v. Добавление

начального шага t t к выводу t true или t false дает необходимый результат. Легко

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

Вариант E-IfTrue: if true then t

else t

Утверждение следует немедленно.

Вариант E-IfFalse: if false then t

else t

Утверждение следует немедленно.

Утверждение A.0.9 Если t v, то t v.

Доказательство: Индукция по числу шагов вычисления (с малым шагом) при выводе t v.

Если t v за 0 шагов, значит, t v, и результат следует из B-Value. В противном случае

требуется анализ вариантов формы t.

Вариант: t if t

then t

else t

По Лемме A.0.8, либо (1) t

true и t

v, либо (2) t

false и t

v. Доказательство

в обоих случаях аналогично, так что предположим, для определенности, вариант (1). Лемма A.0.8

утверждает также, что последовательности вычисления для t

true и t

v короче, чем для

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

true и t

v. Теперь мы можем

вывести t v через правило B-IfTrue.

Другие конструкторы термов разбираются аналогично.

4.2.1. Решение: Каждый раз, когда eval вызывает себя рекурсивно, на стек вызовов помещается об-

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

концов стек переполнится. В сущности, из-за того, что рекурсивный вызов eval обернут в try, он пере-

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

версия eval такова:

rev. 104

386

let rec eval t =

let t ’ opt = try Some ( eval1 t) with NoR u l e A p p l i e s -> None in

match t ’ opt with

Some (t ’) -> eval t ’

| None -> t

5.2.1. Решение:

or = λb . λc . b tru c ;

not = λb . b fls tru ;

5.2.2. Решение:

scc2 = λn . λs . λz. n s ( s z );

5.2.3. Решение:

ti mes2 = λm. λn. λs . λz . m ( n s ) z ;

Или же, более компактно:

ti mes3 = λm. λn. λs . m ( n s );

5.2.4. Решение: Опять же, есть более одного способа:

po wer1 = λm. λn. m ( times n ) c

;

po wer2 = λm. λn. m n;

5.2.5. Решение:

sub t r act1 = λm . λn . n prd n;

5.2.6. Решение: Вычисление prd c

занимает O n шагов, поскольку prd строит последовательность

из n пар чисел, а затем выбирает первый элемент последней пары.

5.2.7. Решение: Вот простое решение:

equal = λm . λn.

and ( iszro (m prd n ))

( iszro ( n prd m ));

5.2.8. Решение: Вот решение, которое имел в виду я:

nil = λc . λn. n;

cons = λh . λt . λc. λn. c h (t c n );

head = λl . l (λh .λt.h ) fls ;

tail = λl .

fst ( l (λx. λp. pair ( snd p) ( cons x ( snd p )))

( pair nil nil ));

isnil = λl . l (λh .λt. fls ) tru ;

Вот немного другой подход:

nil = pair tru tru ;

cons = λh . λt . pair fls ( pair h t );

head = λz . fst ( snd z );

tail = λz . snd ( snd z );

isnil = fst ;

5.2.9. Решение: Мы используем if, а не test, для того, чтобы избежать вычисления обеих ветвей

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

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

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

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

применяем все выражение test к аргументу-заглушке, скажем, c

, чтобы заставить выбранную ветвь

вычисляться.

rev. 104

387

ff = λf . λn .

test

( iszro n ) (λx. c

) (λx. ( times n ( f ( prd n )))) c

;

fac t o rial = fix ff ;

equal c

( factor i a l c

);

(λx . λy . x )

5.2.10. Решение: Вот рекурсивное решение:

cn = λf . λm . if isze ro m then c

else scc ( f ( pred m ));

chu r c hnat = fix cn ;

Простая проверка, что оно работает:

equal ( c hurchnat 4) c

;

(λx . λy . x )

5.2.11. Решение:

ff = λf . λl .

test ( isnil l)

(λx . c

) (λx. ( plus ( head l) (f ( tail l )))) c

;

su mlist = fix ff ;

l = cons c

( cons c

nil ));

equal ( sumlis t l ) c

;

(λx . λy . x )

Разумеется, функцию суммирования списка можно написать и без помощи fix:

sumlist’ = λl. l plus c

; equal (sumlist’ l) c

; |> (λx. λy. x)

5.3.3. Решение: Индукция по размеру t. Предположим, что требуемое свойство выполняется для всех

термов меньше t; нужно доказать его для самого t. Нужно рассмотреть три варианта:

Вариант: t x

Следует непосредственно: F V t x 1 size t .

Вариант: t λx.t

Согласно предположению индукции, F V t

size t

. Считаем так:

F V t F V t

x F V t

size t

size t .

Вариант: t t

Согласно предположению индукции, F V t

size t

и F V t

size t

. Считаем так:

F V t F V t

F V t

size t

size t .

5.4.1. Решение: Для полной (недетерминистской) бета-редукции правила таковы:

(E-App1)

(E-App2)

λx.t

(E-Abs)

(λx.t

) t

x t

(E-AppAbs)

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

лений один из вариантов записи правил таков:

rev. 104

388

(E-App1)

nanf

(E-App2)

λx.t

(E-Abs)

(λx.t

) t

x t

(E-AppAbs)

где синтаксические категории нормальной формы, нормальной формы-не абстракции и не-абстракции

определяются так:

nf ::= нормальные формы:

λx.nf

nanf

nanf ::= нормальные формы-не абстракции:

nanf nf

na ::= не-абстракции:

(Это определение по сравнению с остальными выглядит немного неестественно. Обычно нормальный

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

левый, самый внешний редекс».)

Ленивая стратегия определяет значения как произвольные абстракции — так же, как и стратегия

вызова по значению. Правила вычисления таковы:

(E-App1)

(λx.t

) t

x t

(E-AppAbs)

5.4.3. Решение:

λx.t λx.t

λx.t

x v

6.1.1. Решение:

= λ. λ. 0;

= λ. λ. 1 (1 0);

plus = λ. λ. λ. λ. 3 1 (2 1 0);

fix = λ. (λ. 1 (λ. (1 1) 0)) (λ. 1 (λ. (1 1) 0));

foo = (λ. (λ. 0)) (λ. 0);

6.1.5. Решение: Эти две функции можно определить так:

removenames

x = индекс самого правого x в последовательности Γ

removenames

λx.t

= λ. removenames

Γ,x

removenames

= removenames

removenames

restorenames

k = k-е имя в Γ

restorenames

λ.t

= λx.restorenames

Γ,x

где x – первое имя переменной, не входящее в dom Γ

restorenames

= restorenames

restorenames

rev. 104

389

Требуемые свойства функций removenames и restorenames доказываются простой структурной индук-

цией на термах.

6.2.2. Решение:

1. λ. λ. 1 (0 4)

2. λ. 0 3 (λ. 0 1 4)

6.2.5. Решение:

0 1 (0 (λ.λ.2)) = 1 (λ. λ. 3)

т. е., a (λx. λy. a)

0 1 (λ.2) (0 (λ.1)) = (1 (λ.2)) (λ. (2 (λ.3)))

т. е., (a (λz. a)) (λx.(a (λz. a)))

0 1 (λ. 0 2) = λ. 0 2

т. е., λb. b a

0 1 (λ. 1 0) = λ. 2 0

т. е., λa’. a a’

6.2.8. Решение: Пусть имеется контекст именования Γ. Обозначим Γ x индекс переменной x в Γ,

считая справа. Требуемое свойство формулируется как

removenames

x s t Γ x removenames

s removenames

Доказательство строится индукцией по t, при помощи Определений 5.3.5 и 6.2.4, некоторых несложных

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

операций с термами. При рассмотрении абстракции ключевую роль играет Соглашение 5.3.4.

6.3.1. Решение: Единственное, как мог бы возникнуть отрицательный индекс — если бы в сдвигаемом

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

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

вверх, и в нем тоже не может быть вхождений переменной 0).

6.3.2. Решение: Доказательство эквивалентности представлений, использующих индексы и уровни,

можно найти в (Lescanne and Rouyer-Degli 1995). Уровни де Брауна обсуждаются также в (de Bruijn

1972) и (Filinski 1999, раздел 5.2).

8.3.5. Решение: Нет: отказ от этого правила приводит к потере свойства продвижения. Ели нам дей-

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

вызывая исключение (Глава 14), если программа пытается его вычислить, или переопределив тип pred

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

помощью типов-пересечений (§15.7) или зависимых типов (§30.5).

8.3.6. Решение: Вот контрпример: терм (if false then true else 0) не имеет типа, но при вычис-

лении дает правильно типизированный терм 0.

8.3.7. Решение: Свойство сохранения типов для семантики с большим шагом подобно тому, что мы

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

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

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

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

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

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

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

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

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

обычно предпочитают стиль с малым шагом.

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

бочные переходы, как в Упражнении 8.3.8. Этот стиль используют, например, Абади и Карделли в

операционной семантике для своего исчисления объектов (Abadi and Cardelli 1996, стр. 87).

rev. 104

390

8.3.8. Решение: В расширенной семантике тупиковые состояния вообще отсутствуют — всякий терм, не

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

в wrong (это, разумеется, тоже надо доказать), — так что свойство продвижения тривиально. С другой

стороны, теорема о редукции субъекта сообщает нам больше информации, чем раньше. Поскольку у

wrong никакого типа нет, утверждение, что правильно типизированный терм может перейти только

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

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

сохранения.

9.2.1. Решение: Потому что множество типов пустое (в синтаксисе типов нет базового варианта).

9.2.3. Решение: Пример такого контекста:

Γ f : Bool Bool Bool, x:Bool, y:Bool

В общем случае, годится любой контекст вида

Γ f:S T Bool, x:S, y:T

где S и T — произвольные типы. Рассуждения такого рода играют ключевую роль в алгоритме рекон-

струкции типов из Главы 22.

9.3.2. Решение: Предположим, что терм x x имеет тип T, и сведем это предположение к противоречию.

По лемме об обращении, левый подтерм (x) должен иметь тип T

, а правый подтерм (тоже x)

должен иметь тип T. Согласно варианту леммы об обращении, относящемуся к переменным, как x :

, так и x : T

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

одно связывание, имеем T

. Но это невозможно — все типы имеют конечный размер, так

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

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

найти решение для уравнения T

. К этому вопросу мы вернемя в Главе 20.

9.3.3. Решение: Предположим, что Γ t : S и Γ t : T. С помощью индукции по построению

Γ t : T мы докажем, что S T.

Вариант T-Var: t x

где x:T Γ

Согласно пункту 1 леммы об обращении (9.3.1), последнее правило во всяком дереве вывода типа

Γ t : S также должно быть T-Var, и S T.

Вариант T-Abs: t λy:T

T T

Γ, y:T

: T

Согласно пункту 2 леммы об обращении, последнее правило во всяком дереве вывода Γ t : S также

должно быть T-Abs, и в этом дереве вывода должно иметься поддерево с выводом Γ, y:T

: S

причем S T

. По предположению индукции (относительно поддерева с заключением (Γ, y:T

: T

)) получаем S

, откуда немедленно следует S T.

Варианты T-App, T-True, T-False, T-IF: Аналогично.

9.3.9. Решение: Индукция по дереву вывода Γ t : T. На каждом шаге индукции мы предполагаем,

что требуемое свойство выполняется для всех поддеревьев (т. е., если Γ s : S и s s’, то Γ s’ : S,

если Γ s : S доказано как поддерево текущего дерева вывода), и рассматриваем варианты последнего

правила в дереве.

Вариант T-Var: t x x:T Γ.

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

Вариант T-Abs: t λx:T

Не может возникнуть.

Вариант T-App: t t

Γ t

: T

Γ t

: T

T T

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

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

рассмотрим отдельно.

rev. 104