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

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

15.6. Семантика наследования, основанная на преобразованиях типов 161

используемого в C.

T <: T

S-Refl

}



λx:JTK. x

S <: Top

S-Top

}



λx:JSK. unit

:: S <: U C

:: U <: T

S <: T

S-Trans

}



λx:JSK. JC

K (JC

K x)

:: T

<: S

:: S

<: T

S-Arrow

}



λf:JS

K. λx:JT

K. JC

K(f(JC

K x))

i 1..n k

} <: {l

i 1..n

}

S-RcdWidth

}



λr:{l

:JT

i 1..n k

}. {l

=r.l

i 1..n

}

для каждого i C

:: S

<: T

i 1..n

} <: {l

i 1..n

}

S-RcdDepth

}



λr:{l

:JS

i 1..n

}. {l

=JC

K(r.l

)

i 1..n

}

j 1..n

}перестановка{l

i 1..n

}

j 1..n

} <: {l

i 1..n

}

S-RcdPerm

}



λr:{k

:JS

j 1..n

}. {l

=r.l

i 1..n

}

Лемма 15.6.1 Если C :: S <: T, то JCK : JSK JTK.

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

Деревья вывода типизации переводятся подобным же образом. Если D – дерево вывода для утвер-

ждения Γ t : T, то его перевод JDK — терм целевого языка типа JTK. Такая функция перевода

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

rev. 104

162 15.6. Семантика наследования, основанная на преобразованиях типов

университете, которая ее впервые исследовала (Breazu-Tannen, Coquand, Gunter and Scedrov 1991).

x:T Γ

Γ x : T

T-Var

}



:: Γ, x:T

: T

Γ λx:T

: T

T-Abs

}



λx: JT

K. JD

:: Γ t

: T

:: Γ t

: T

Γ t

: T

T-App

}



KJD

для каждого i,D

:: Γ t

: T

Γ {l

i 1..n

} : {l

i 1..n

}

T-Rcd

}



=JD

i 1..n

}

:: Γ t

: {l

i 1..n

}

Γ t

: T

T-Proj

}



K.l

D :: t : S C :: S <: T

Γ t : T

T-Sub

}



JCKJDK

Теорема 15.6.2 Если D :: Γ t : T, то JΓK JDK : JTK, где JΓK — поточечное расширение функции

перевода типов на контексты типизации: J K и JΓ, x:TK JΓK, x:JTK.

Доказательство: Прямолинейная индукция по D, с использованием Леммы 15.6.1 для варианта T-Sub.

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

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

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

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

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

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

тальном компиляторе языка Java, разработанном Йельской группой (League, Shao and Trifonov 1999;

League, Trifonov and Shao 2001).

Упражнение 15.6.3 , : Модифицируйте приведенную нами функцию перевода так, чтобы це-

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

Убедитесь, что по-прежнему выполняется Теорема 15.6.2.

15.6.3. Когерентность

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

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

наш теперешний язык базовыми типами Int, Bool, Float и String. Могут быть полезны следующие

элементарные преобразования:

JBool <: IntK λb:Bool. if b then 1 else 0

JInt <: StringK intToString

JBool <: FloatK λb:Bool. if b then 1.0 else 0.0

JFloat <: StringK floatToString

rev. 104

15.7. Типы-пересечения и типы-объединения 163

Здесь intToString и floatToString — примитивы, порождающие строковое представление чисел. В

иллюстративных целях, предположим, что intToString(1) = "1", а floatToString(1.0) = "1.000".

Предположим теперь, что мы пытаемся вычислить терм

(λx : Strin g . x) true

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

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

включение переводим Bool в Int, и затем в String, показывая, что true — подходящий аргумент для

функции типа String String, либо сначала мы переводим Bool во Float, и оттуда в String. Однако

при переводе этих преобразований в λ получается различное поведение. Если мы переводим true в

Int, получается 1, откуда через intToString выходит строка "1". Однако если мы сначала проведем

преобразование во Float, а затем, через floatToString, в String (следуя структуре дерева вывода

типа, где true : String доказывается через Float), мы получим "1.000". Но "1" и "1.000" – совер-

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

для (λx:String.x) true : String влияет на то, как ведет себя оттранслированная программа! Но

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

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

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

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

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

Определение 15.6.4 Функция перевода J K из деревьев вывода типов одного языка в термы другого

когерентна, если для всякой пары деревьев вывода D

и D

с одним и тем же заключением Γ t : T

переводы JD

K и JD

K являются поведенчески эквивалентными термами целевого языка.

В частности, приведенные выше функции перевода (без базовых типов) когерентны. Чтобы вос-

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

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

floatToString(0.0) "0" и floatToString(1.0) "1".

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

См. работы Рейнольдса (Reynolds 1980), Бреазу-Таннена и др. (Breazu-Tannen et al. 1991), Куриена и

Гелли (Curien and Ghelli 1992) и Рейнольдса (Reynolds 1991).

15.7. Типы-пересечения и типы-объединения

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

ресечения. Типы-пересечения изобретены Коппо, Дезани, Салле и Поттингером (Coppo and Dezani-

Ciancaglini 1978; Coppo, Dezani-Ciancaglini and Sall´e 1979; Pottinger 1980). Доступные введения можно

найти у Рейнольдса (Reynolds 1988, 1998b), Хиндли (Hindley 1992) и Пирса (Pierce 1991b).

Тип-пересечение T

населен термами, принадлежащими обоим типам T

и T

— то есть, T

является, в смысле теории порядков, пересечением (точной нижней гранью) T

и T

. Такая интуиция

отражается в трех новых правилах наследования:

<: T

(S-Inter1)

<: T

(S-Inter2)

S <: T

(S-Inter3)

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

функциональными типами.

S T

<: S (T

) (S-Inter4)

rev. 104

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

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

типы S T

и S T

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

качестве результата как T

, так и T

Мощность понятия типов-пересечений можно продемонстрировать утверждением, что в варианте

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

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

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

вычисление завершается! Отсюда немедленно следует, что проблема реконструкции типов (см. Гла-

ву 22) для исчисления с типами-перечислениями неразешима.

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

вают некоторую форму конечной перегрузки операторов. Например, мы можем присвоить тип (Nat

Nat Nat) (Float Float Float) операции сложения, которая применима как к натураль-

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

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

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

разработчиков языков. Пока что лишь один полноразмерный язык, Forsythe (Reynolds 1988) включа-

ет типы-пересечения в их наиболее общем виде. Ограниченная форма, называемая типы-уточнения,

может оказаться более доступной (Freeman and Pfenning 1991; Pfenning 1993b; Davies 1997).

Двойственное понятие типов-объединений также оказывается весьа полезным. В отличие от типов-

сумм и вариантов (которые также иногда называют «объединениями», что приводит к путанице), T

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

, и множе-

ства значений, принадлежащих к типу T

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

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

но играли важную роль при анализе программ (Palsberg and Pavlopolou 1998), но редко встречались в

языках программирования (важное исключение — Algol 68, см. (van Wijngaarden et al. 1975)). Впрочем,

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

рованных» форматов баз данных вроде XML (Buneman and Pierce 1998; Hosoya, Vouillon and Pierce

2001).

Основное формальное различие между разъединенными (неперекрывающимися) и неразъединен-

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

струкции case: если известно, что значение v имеет тип T

, то мы можем безопасно применять к

нему только те операции, которые имеют смысл как для T

, так и для T

. (Например, если T

и T

—

записи, имеет смысл обращаться к их общим полям.) Бестеговый тип union в языке C служит источ-

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

над элементом типа T

разрешена любая операция, имеющая смысл либо для T

, либо для T

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

Идея наследования в языках программирования восходит к 1960-м годам, к Симуле (Birtwistle, Dahl,

Myhrhaug and Nygaard 1979) и ее родственникам. Первые попытки формального анализа принадлежат

Рейнольдсу (Reynolds 1980) и Карделли (Cardelli 1984).

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

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

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

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

ности, полагаясь на неформальные соглашения (напр., многоточие: «l

...l

»). Недовольство

таким положением дел привело Карделли и Митчелла к разработке исчисления операций над запи-

сями (Cardelli and Mitchell 1991), где макрооперация создания записи с многими полями выражается

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

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

конкатенации записей (Harper and Pierce 1991). Правила типизации для этих операций оказываются

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

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

rev. 104

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

Митчелла остается важным концептуальным ориентиром. Альтернативный анализ записей, основан-

ный на полиморфизме переменных строк, разработан Вандом (Wand 1987, 1988, 1989b), Реми (R´emy

1990, 1989, 1992) и другими, и служит основой объектно-ориентированных конструкций OCaml (R´emy

and Vouillon 1998; Vouillon 2000).

Основная задача, решаемая

теорией типов, состоит в том,

чтобы обеспечить наличие

смысла у программ. Основная

проблема, порождаемая теорией

типов, состоит в том, что

некоторым осмысленным

программам никакого смысла

не приписывается. Поиск более

богатых систем типов

проистекает из этого

противоречия.

Марк Мэнасс

rev. 104

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

rev. 104

Глава 16

Метатеория наследования

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

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

правила в этой системе не управляются синтаксисом — их нельзя просто считать «снизу вверх» и

получить алгоритм проверки типов. Сложности для отношения типизации происходит в основном из-за

правила включения T-Sub, а для отношения наследования — из-за правила транзитивности S-Trans.

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

менная t:

Γ t : S S <: T

Γ t : T

(T-Sub)

Все остальные правила типизации указывают в заключении терм некоторого определенного вида: T-

Abs относится только к лямбда-абстракциям, T-Var только к переменным, и т. д., — а T-Sub при-

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

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

соответствует форме t.

Правило S-Trans ведет к трудностям по той же самой причине — его заключение перекрывается с

заключениями других правил.

S <: U U <: T

S <: T

(S-Trans)

Поскольку S и T — просто метапеременные, в принципе, S-Trans может оказаться последним пра-

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

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

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

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

Это еще не все трудности, связанные с S-Trans. Обе его предпосылки содержат метапеременную

U, которая не упоминается в заключении. Если мы наивно читаем правило снизу вверх, то получается,

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

число типов-кандидатов на роль U бесконечно, надежда на успех при такой стратегии невелика.

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

никающая сложность меньше, чем в случае T-Sub и S-Trans: в правиле S-Refl нет предпосылок, так

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

чиваем немедленно. Тем не менее, это еще один пункт, где наши правила не управляются синтаксисом.

Чтобы справиться со всеми этими проблемами, мы заменяем обыкновенные (декларативные) от-

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

ношение наследования и алгоритмическое отношение типизации. Эти два отношения управляются

В этой главе изучается простое типизированное лямбда-исчисление с наследованием (Рис. 15.1) и записями (Рис. 15.3).

Соответствующий интерпретатор на OCaml называется rcdsub. В §16.3 упоминаются также булевские значения и услов-

ные выражения (8.1); для этого раздела используется интерпретатор joinsub. В §16.4 добавляется тип Bot; соответству-

ющий интерпретатор называется bot.

167

168 16.1. Алгоритмическое отношение наследования

<: Расширяет 15.1 и 15.3

S <: S (S-Refl)

S <: U U <: T

S <: T

(S-Trans)

S <: Top (S-Top)

<: S

<: T

(S-Arrow)

i 1..n

j 1..m

при каждом k

имеем S

<: T

j 1..m

} <: {l

i 1..n

}

(S-Rcd)

Рис. 16.1. Отношение наследования для записей (компактная версия)

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

типизации совпадают со своими алгоритмическими вариантами: утверждение S <: T тогда и только

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

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

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

Алгоритмическое отношение наследования представлено в §16.1, а алгоритмическое отношение ти-

пизации в §16.2. В §16.3 рассматривается особая проблема проверки ветвящихся конструкций вроде

if...then...else, где требуется дополнительная структура (наличие точных верхних граней, объеди-

нений, в отношении наследования). В §16.4 рассматривается минимальный тип Bot.

16.1. Алгоритмическое отношение наследования

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

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

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

, где t

имеет тип T U,

а t

тип S. Задача этой процедуры — опеределить, выводимо ли утверждение S <: T из правил насле-

дования на Рис. 15.1 и 15.3. Задача эта решается путем проверки, принадлежит ли пара (S,T) другому

отношению, обозначаемому S <: T («S является с алгоритмической точки зрения подтипом T»).

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

типов, и содержит те же самые пары типов, что и исходное отношение наследования. Существенное

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

определении алгоритмического отношения нет правил S-Trans и S-Refl.

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

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

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

мы откажемся от S-Trans, нужно добавить правило, объединяющее эти три вида наследования:

i 1..n

j 1..m

при каждом k

имеем S

<: T

j 1..m

} <: {l

i 1..n

}

(S-Rcd)

Лемма 16.1.1 Если S <: T выводится из правил наследования, включая S-RcdDepth, S-RcdWidth и

S-RcdPerm, но не включая S-Rcd, то это утверждение можно также вывести с использованием

S-Rcd (но не S-RcdDepth, S-RcdWidth и S-RcdPerm), и наоборот.

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

Благодаря Лемме 16.1.1, мы можем заменить правила S-RcdDepth, S-RcdWidth и S-RcdPerm

на S-Rcd. Получающаяся система представлена на Рис. 16.1.

Теперь мы можем показать, что в системе с Рис. 16.1 правила рефлексивности и транзитивности

несущественны.

Лемма 16.1.2 1. Для каждого типа S можно вывести S <: S без использования S-Refl.

2. Если выводимо утверждение S <: T, то его можно вывести без использования S-Trans.

Доказательство: Упражнение Рекомендуется, .

rev. 104

16.1. Алгоритмическое отношение наследования 169

Алгоритмическое наследование S <: T

S <: Top (SA-Top)

i 1..n

j 1..m

при каждом k

имеем S

<: T

j 1..m

} <: {l

i 1..n

}

(SA-Rcd)

<: S

<: T

(SA-Arrow)

Рис. 16.2. Алгоритмическое отношение наследования

Упражнение 16.1.3 Как повлияет на эти свойства добавление типа Bool?

Это приводит нас к определению алгоритмического отношения наследования.

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

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

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

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

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

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

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

Утверждение 16.1.5 S <: T тогда и только тогда, когда S <: T.

Доказательство: В обоих направлениях доказательство строится по индукции на деревьях вывода,

с помощтю одной из двух предыдущих лемм.

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

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

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

subtype S, T

если T Top, то истина

иначе если S S

и T T

то subtype T

, S

subtype S

, T

иначе если S {k

j 1..m

} и T {l

i 1..n

то l

i 1..n

j 1..m

для каждого i имеется некоторое j 1..m, такое, что k

и subtype S

, T

иначе ложь

Конкретную реализацию этого алгоритма на языке ML можно найти в Главе 17.

Наконец, нам нужно убедиться, что алгоритмическое отношение наследования всюду определено —

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

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

Утверждение 16.1.6 Если выводимо утверждение S <: T, то функция subtype S, T вернет значе-

ние истина. Если нет, она вернет значение ложь.

Эта теорема, совместно с корректностью и полнотой алгоритмических правил, по существу,

утверждает, что функция subtype служит разрешающей процедурой для декларативного отношения

наследования.

Доказательство: Первое утверждение легко поддается проверке (путем прямолинейной индукции по

дереву вывода S <: T). С другой стороны, так же легко убедиться, что, если subtype S, T возвра-

щает значение истина, выполняется S <: T. Таким оьразом, чтобы проверить второе утвержде-

ние, достаточно показать, что subtype S, T всегда что-то возвращает — т. е., всегда завершается.

rev. 104

170 16.2. Алгоритмическое отношение типизации

Этого мы можем добиться, заметив, что сумма размеров входной пары аргументов S и T всегда

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

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

рекурсивных вызовов невозможна.

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

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

ного, и даже не упоминать декларативное определение. Ответом будет «да», но с оговорками. Разу-

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

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

показать, что отношение типизации (зависящее от отношения наследования) ведет себя должным об-

разом, требуется знать, что отношение наследования рефлексивно и транзитивно, а эти доказательства

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

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

этого мы увидим в Главе 19.)

16.2. Алгоритмическое отношение типизации

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

типизации. Как мы видели на стр. 167, единственное правило типизации, не управляемое синтаксисом

— T-Sub, так что именно с ним нам предстоит работать. Подобно S-Trans в предыдущем разделе, мы

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

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

более синтаксически управляемым способом.

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

дений между типами аргументов, ожидаемыми в функциях, и типами их реальных аргументов. Терм

вроде

(λr :{ x : Nat }. r . x) { x=0 ,y =1}

без правила включения не типизируется.

Возможно, это покажется странным, но указанная ситуация — единственная, где правило включе-

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

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

ние R-Sub «откладывается», будучи сдвинуто вниз по дереву к корню. Чтобы в этом убедиться, полезно

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

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

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

T-Sub.

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

его непосредственный подвывод заканчивается применением T-Sub:

Γ, x:S

: S

<: T

Γ, x:S

: T

T-Sub

Γ λx:S

: S

T-Abs

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

стракции, и получить то же заключение, что и раньше:

Γ, x:S

: S

Γ λx:S

: S

T-Abs

<: S

S-Refl

<: T

<: S

S-Arrow

Γ λx:S

: S

T-Sub

rev. 104