Система У

В математической логике Система U и Система U ⁻ являются чистыми системами типов , т.е. специальными формами типизированного лямбда-исчисления с произвольным числом сортов , аксиом и правил (или зависимостей между сортами). Несовместимость системы U была доказана Жан-Ивом Жираром в 1972 году. ^[1] (и вопрос последовательности Система У ⁻ было сформулировано).Этот результат привел к осознанию того, что Мартина-Лёфа первоначальная теория типов 1971 года была непоследовательной, поскольку допускала то же поведение «Тип в типе», которое использует парадокс Жирара.

Формальное определение

Система U определена ^[2]^: 352 как система чистых типов с

три вида $\{\ast ,\square ,\triangle \}$ ;
две аксиомы $\{\ast :\square ,\square :\triangle \}$ ; и
пять правил $\{(\ast ,\ast ),(\square ,\ast ),(\square ,\square ),(\triangle ,\ast ),(\triangle ,\square )\}$ .

Система У ⁻ определяется так же, за исключением $(\triangle ,\ast )$ правило.

Сорта $\ast$ и $\square$ условно называются «Тип» и « Вид » соответственно; вид $\triangle$ не имеет конкретного названия. Две аксиомы описывают включение типов в виды ( $\ast :\square$ ) и виды в $\triangle$ ( $\square :\triangle$ ). Интуитивно понятно, что сорта описывают иерархию по природе терминов.

Все значения имеют тип , например базовый тип ( например, $b:\mathrm {Bool}$ читается как « $b$ — логическое значение») или (зависимый) тип функции ( например, $f:\mathrm {Nat} \to \mathrm {Bool}$ читается как « $f$ — функция преобразования натуральных чисел в логические значения»).
$\ast$ является сортом всех таких типов ( $t:\ast$ читается как « $t$ — тип»). От $\ast$ мы можем построить больше терминов, таких как $\ast \to \ast$ это своего рода унарные операторы уровня типа ( например , $\mathrm {List} :\ast \to \ast$ читается как « $Список$ — это функция от типов к типам», то есть полиморфный тип). Правила ограничивают то, как мы можем создавать новые виды.
$\square$ это сорт всех таких видов ( $k:\square$ читается как « $к$ — вид»). Точно так же мы можем создавать связанные термины в соответствии с тем, что позволяют правила.
$\triangle$ это разновидность всех таких терминов.

Правила регулируют зависимости между сортами: $(\ast ,\ast )$ говорит, что значения могут зависеть от значений ( функций ), $(\square ,\ast )$ позволяет значениям зависеть от типов ( полиморфизм ), $(\square ,\square )$ позволяет типам зависеть от типов ( операторов типов ) и так далее.

Парадокс Жирара

Определения системы U и U ⁻ позволяют присваивать полиморфные виды универсальным конструкторам по аналогии с полиморфными типами терминов в классических полиморфных лямбда-исчислениях, таких как System F . Примером такого универсального конструктора может быть ^[2]^: 353 (где k обозначает переменную типа)

\lambda k^{\square }\lambda \alpha ^{k\to k}\lambda \beta ^{k}\!.\alpha (\alpha \beta )\;:\;\Pi k:\square ((k\to k)\to k\to k)

.

Этого механизма достаточно для построения терма типа $(\forall p:\ast ,p)$ (эквивалент типа $\bot$ ), что означает, что каждый тип обитаем . Согласно соответствию Карри-Ховарда это эквивалентно доказуемости всех логических утверждений, что делает систему несовместимой.

Парадокс Жирара — это теоретико-типический аналог парадокса Рассела в теории множеств .

Ссылки

^ Жирар, Жан-Ив (1972). «Функциональная интерпретация и устранение сокращений арифметики высшего порядка» (PDF) .
^ Jump up to: ^а ^б Соренсен, Мортен Хейне; Уржичин, Павел (2006). «Системы чистых типов и лямбда-куб». Лекции по изоморфизму Карри–Говарда . Эльзевир. дои : 10.1016/S0049-237X(06)80015-7 . ISBN 0-444-52077-5 .

Дальнейшее чтение

Барендрегт, Хенк (1992). «Лямбда-исчисления с типами» . У С. Абрамского; Д. Габбай; Т. Майбаум (ред.). Справочник по логике в информатике . Оксфордские научные публикации . стр. 117–309.
Коканд, Тьерри (1986). «Анализ парадокса Жирара». Логика в информатике . Издательство Компьютерного общества IEEE . стр. 227–236.
Хуркенс, Антониус Дж. К. (1995). Дезани-Чианкаглини, Марианджола; Плоткин, Гордон (ред.). Упрощение парадокса Жирара . Вторая международная конференция по типизированным лямбда-исчислениям и их приложениям (TLCA '95) . Эдинбург. стр. 266–278. дои : 10.1007/BFb0014058 .

[Girard1972-1] Жирар, Жан-Ив (1972). «Функциональная интерпретация и устранение сокращений арифметики высшего порядка» (PDF) .

[SoerensenUrzyczyn2006-2] Jump up to: ^а ^б Соренсен, Мортен Хейне; Уржичин, Павел (2006). «Системы чистых типов и лямбда-куб». Лекции по изоморфизму Карри–Говарда . Эльзевир. дои : 10.1016/S0049-237X(06)80015-7 . ISBN 0-444-52077-5 .

[1]

[2]