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

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

Парадокс Жирара [ править ]

Определения системы U и U ^- разрешить назначение полиморфных видов в общих конструкторами по аналогии с полиморфными типами терминов в классических полиморфных лямбда - исчислений, такие как System 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 }$

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

Ссылки [ править ]

Дальнейшее чтение [ править ]

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