Тип удостоверения
 | Эта статья нуждается в дополнительных цитатах для проверки . ( январь 2022 г. ) |
В теории типов тождественный тип представляет собой концепцию равенства . Оно также известно как пропозициональное равенство , чтобы отличить его от «оценочного равенства». Равенство в теории типов — сложная тема, которая была предметом исследований, например, в области теории гомотопических типов . [1]
с оценочным Сравнение равенством
Тождественный тип — это одно из двух различных понятий равенства в теории типов. [2] Более фундаментальное понятие — «равенство суждений», которое представляет собой суждение .
За пределами равенстве суждения о
Тип идентичности может сделать больше, чем то, что может сделать равенство в суждениях. Его можно использовать, чтобы показать «для всех ", что невозможно продемонстрировать с помощью оценочного равенства. Это достигается с помощью элиминатора (или "рекурсора") натуральных чисел, известного как "R".
Функция «R» позволяет нам определить новую функцию для натуральных чисел. Эта новая функция «P» определяется как «(λ x:nat . x+1 = 1+x)». Остальные аргументы действуют как части индукционного доказательства. Аргумент «PZ : P 0» становится базовым вариантом «0+1 = 1+0», что является термином «refl nat 1». Аргумент «PS : P n → P (S n)» становится индуктивным случаем. По сути, это означает, что когда «x+1 = 1+x» заменяется «x» каноническим значением, выражение будет таким же, как «refl nat (x+1)».
Версии типа удостоверения [ править ]
Тип идентичности сложен и является предметом исследования в теории типов. Хотя каждая версия согласовывает конструктор «refl». Их свойства и функции элиминатора существенно различаются.
Для «расширенных» версий любой тип идентичности может быть преобразован в оценочное равенство. Вычислительная версия известна как «Аксиома К» благодаря Томасу Штрайхеру. [3] В последнее время они не очень популярны.
Сложность типа личности [ править ]
Мартин Хоффман и Томас Штрайхер опровергли утверждение, что теория типов идей требует, чтобы все термины типа идентичности были одинаковыми. [4]
Популярным направлением исследования тождественного типа является теория гомотопических типов. [5] и его теория кубического типа .
Ссылки [ править ]
- ^ «Тип удостоверения» . нЛаб . Проверено 19 января 2022 г.
- ^ Мартин-Лёф, Пер (июнь 1980 г.). Интуиционистская теория типов (PDF) .
- ^ Штрайхер, Томас (1993). Исследования по интенсиональной теории типов (PDF) .
- ^ Хоффман, Мартин; Штрайхер, Томас (июль 1994 г.). «Группоидная модель опровергает единственность доказательств тождества» . Труды Девятого ежегодного симпозиума IEEE по логике в информатике . стр. 208–212. дои : 10.1109/LICS.1994.316071 . ISBN 0-8186-6310-3 . S2CID 19496198 .
- ^ Программа Uniвалентных фондов (12 марта 2013 г.). Гомотопическая теория типов . Институт перспективных исследований.
