Система U - System U

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

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

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

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

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

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

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

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

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

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

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

Этого механизма достаточно, чтобы построить терм с типом ${\displaystyle (\forall p:\ast ,p)=\bot }$, откуда следует, что каждый тип обитаемый. Посредством Переписка Карри – Ховарда, это эквивалентно доказуемости всех логических предложений, что делает систему непоследовательной.

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

Рекомендации

1. Жирар, Жан-Ив (1972). "Interprétation fonctionnelle et Élimination des coupures de l'arithmétique d'ordre supérieur" (PDF).
2. Соренсен, Мортен Гейне; Уржичин, Павел (2006). «Системы чистых типов и лямбда-куб». Лекции об изоморфизме Карри – Ховарда. Эльзевир. ISBN  0-444-52077-5.

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

• Барендрегт, Хенк (1992). «Лямбда-исчисления с типами». У С. Абрамского; Д. Габбай; Т. Майбаум (ред.). Справочник по логике в компьютерных науках. Oxford Science Publications. С. 117–309.
• Кокванд, Тьерри (1986). «Анализ парадокса Жирара». Логика в информатике. IEEE Computer Society Нажмите. С. 227–236.