Индуктивный тип

Эта статья требует дополнительных ссылок для проверки . Пожалуйста, помогите улучшить эту статью , добавив цитаты из надежных источников . Материал, не полученный от источника, может быть оспорен и удален.
Найти источники: «Индуктивный тип» - новости · газеты · книги · ученый · JSTOR ( январь 2018 г. ) ( Узнайте, как и когда удалить это сообщение-шаблон )

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

Стандартный пример - это кодирование натуральных чисел с использованием кодировки Пеано .

 Индуктивный  нат  :  Тип  : =  |  0  :  нац  |  С  :  нац  ->  нац .

Здесь натуральное число создается либо из константы «0», либо путем применения функции «S» к другому натуральному числу. «S» - это функция-преемник, которая представляет добавление 1 к числу. Таким образом, «0» равен нулю, «S 0» равен единице, «S (S 0)» равен двум, «S (S (S 0))» равен трем и так далее.

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

Устранение [ править ]

Индуктивные типы обычно имеют функцию, позволяющую доказать их свойства. Таким образом, «нат» может иметь:

 nat_elim  :  ( forall  P  :  nat  ->  Prop ,  ( P  0 )  ->  ( forall  n ,  P  n  ->  P  ( S  n ))  ->  ( forall  n ,  P  n )).

Это ожидаемая функция структурной рекурсии для типа nat.

Реализации [ править ]

W- и M-типы [ править ]

W-типы - это хорошо обоснованные типы в интуиционистской теории типов (ITT). ^[1] Они обобщают натуральные числа, списки, двоичные деревья и другие «древовидные» типы данных. Пусть U - вселенная типов . Учитывая тип A : U и зависимое семейство B : A → U , можно сформировать W-тип . Тип A можно рассматривать как «метки» для (потенциально бесконечного множества) конструкторов определяемого индуктивного типа, тогда как B указывает (потенциально бесконечную) арность ${\ displaystyle {\ mathsf {W}} _ {a: A} B (a)}$ каждого конструктора. W-типы (соответственно M-типы) также можно понимать как хорошо обоснованные (или необоснованные) деревья с узлами, помеченными элементами a : A, и где узел, помеченный a, имеет B ( a ) -многие поддеревья. ^[2] Каждый W-тип изоморфен исходной алгебре так называемого полиномиального функтора .

Пусть 0 , 1 , 2 и т. Д. Будут конечными типами с обитателями 1 ₁ : 1 , 1 ₂ , 2 ₂ : 2 и т. Д. Можно определить натуральные числа как W-тип.

{\ Displaystyle \ mathbb {N}: = {\ mathsf {W}} _ {x: \ mathbf {2}} f (x)}

с f : 2 → U определяется как f (1 ₂ ) = 0 (представляющий конструктор для нуля, который не принимает аргументов) и f (2 ₂ ) = 1 (представляющий функцию-последователь, которая принимает один аргумент).

Можно определить списки для типа A : U как где ${\ Displaystyle \ OperatorName {Список} (A): = {\ mathsf {W}} _ {(x: \ mathbf {1} + A)} f (x)}$

{\ displaystyle {\ begin {align} f (\ operatorname {inl} (1 _ {\ mathbf {1}})) & = \ mathbf {0} \\ f (\ operatorname {inr} (a)) & = \ mathbf {1} \ конец {выровнено}}}

и 1 ₁ является единственным обитателем 1 . Значение соответствует конструктору для пустого списка, в то время как значения соответствует конструктору , который присоединяет к началу другого списка. ${\ Displaystyle е (\ OperatorName {inl} (1 _ {\ mathbf {1}}))}$ ${\ Displaystyle е (\ OperatorName {inr} (а))}$

Конструктор элементов универсального W-типа имеет тип ${\mathsf {W}}_{x:A}B(x)$

{\mathsf {sup}}:\prod _{a:A}{\Big (}B(a)\to {\mathsf {W}}_{x:A}B(x){\Big )}\to {\mathsf {W}}_{x:A}B(x).

Мы также можем записать это правило в стиле доказательства естественного вывода :

{\frac {a:A\qquad f:B(a)\to {\mathsf {W}}_{x:A}B(x)}{{\mathsf {sup}}(a,f):{\mathsf {W}}_{x:A}B(x)}}.

Правило исключения для W-типов работает аналогично структурной индукции на деревьях. Если всякий раз, когда свойство (в интерпретации предложений как типов ) выполняется для всех поддеревьев данного дерева, оно также выполняется для этого дерева, то оно выполняется для всех деревьев. $C:{\mathsf {W}}_{x:A}B(x)\to U$

{\frac {w:{\mathsf {W}}_{a:A}B(a)\qquad a:A,\;f:B(a)\to {\mathsf {W}}_{x:A}B(x),\;c:\prod _{b:B(a)}C(f(b))\;\vdash \;h(a,f,c):C({\mathsf {sup}}(a,f))}{{\mathsf {elim}}(w,h):C(w)}}

В теориях экстенсионального типа W-типы (соответственно M-типы) могут быть определены с точностью до изоморфизма как начальные алгебры (соответственно финальные коалгебры) для полиномиальных функторов . В этом случае свойство начальности (окончательности) напрямую соответствует соответствующему принципу индукции. ^[3] В теориях интенсионального типа с аксиомой однолистности это соответствие сохраняется до гомотопии (пропозиционального равенства). ^[4]^[5]^[6]

M-типы двойственны W-типам, они представляют собой коиндуктивные (потенциально бесконечные) данные, такие как потоки . ^[7] M-типы могут быть производными от W-типов. ^[8]

Взаимоиндуктивные определения [ править ]

Этот метод позволяет некоторым определения нескольких типов , которые зависят друг от друга. Например, определение двух предикатов четности для натуральных чисел с использованием двух взаимно индуктивных типов в Coq :

Индуктивный  даже  :  физ  ->  Prop  : =  |  zero_is_even  :  даже  O  |  S_of_odd_is_even  :  (для всех  n : nat ,  нечетных  n  ->  четных  ( S  n )) с  odd  :  nat  ->  Prop  : =  |  S_of_even_is_odd  :  (для всех  n : nat ,  даже  n  ->  odd  ( S  n )).

Индукция-рекурсия [ править ]

Индукция-рекурсия началась как исследование возможностей ITT. Найденные ограничения были превращены в правила, позволяющие определять новые индуктивные типы. Эти типы могут зависеть от функции, а функция от типа, если оба они определены одновременно.

Типы юниверсов могут быть определены с помощью индукции-рекурсии.

Индукция-индукция [ править ]

Индукция-индукция позволяет одновременно определять тип и семейство типов. Итак, тип $А$ и семейство типов . $B:A\to Type$

Высшие индуктивные типы [ править ]

Это текущая область исследований теории гомотопических типов (HoTT). HoTT отличается от ITT своим типом идентичности (равенством). Высшие индуктивные типы не только определяют новый тип с константами и функциями, которые создают элементы типа, но также и новые экземпляры типа идентичности, которые их связывают.

Простым примером является тип $круга$ , который определяется двумя конструкторами: базовой точкой;

база : круг

и петля;

петля : основание = основание .

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

См. Также [ править ]

Коиндукция допускает (эффективно) бесконечные структуры в теории типов.

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

^ Мартин-Löf Пер (1984). Интуиционистская теория типов (PDF) . Самбин, Джованни. Неаполь: Библиополь. ISBN 8870881059. OCLC 12731401 .
^ Аренс, Бенедикт; Каприотти, Паоло; Спадотти, Режис (12 апреля 2015 г.). «Необоснованные деревья в теории гомотопических типов». arXiv : 1504.02949 . DOI : 10.4230 / LIPIcs.TLCA.2015.17 . Cite journal requires |journal= (help)
^ Dybjer, Питер (1997). «Представление индуктивно определенных множеств порядками в теории типов Мартина-Лёфа». Теоретическая информатика . 176 (1–2): 329–335. DOI : 10.1016 / s0304-3975 (96) 00145-4 .
^ Awodey, Стив; Гамбино, Никола; Соякова, Кристина (18.01.2012). «Индуктивные типы в теории гомотопических типов». arXiv : 1201.3898 [ math.LO ].
^ Аренс, Бенедикт; Каприотти, Паоло; Спадотти, Режис (12 апреля 2015 г.). «Необоснованные деревья в теории гомотопических типов». arXiv : 1504.02949 . DOI : 10.4230 / LIPIcs.TLCA.2015.17 . Cite journal requires |journal= (help)
^ Awodey, Стив; Гамбино, Никола; Соякова, Кристина (21.04.2015). «Гомотопически-начальные алгебры в теории типов». arXiv : 1504.05531 [ math.LO ].
^ ван ден Берг, Бенно; Марчи, Федерико Де (2007). «Необоснованные деревья по категориям». Летопись чистой и прикладной логики . 146 (1): 40–59. arXiv : math / 0409158 . DOI : 10.1016 / j.apal.2006.12.001 .
^ Эбботт, Майкл; Альтенкирх, Торстен; Гани, Нил (2005). «Контейнеры: конструирование строго положительных типов». Теоретическая информатика . 342 (1): 3–27. DOI : 10.1016 / j.tcs.2005.06.002 .

Программа Univalent Foundations (2013 г.). Теория гомотопического типа: однолистные основы математики . Институт перспективных исследований.

Внешние ссылки [ править ]

Индукционно-рекурсивные слайды
Индукционно-индукционные слайды
Высшие индуктивные типы: экскурсия по зверинцу

[1] Мартин-Löf Пер (1984). Интуиционистская теория типов (PDF) . Самбин, Джованни. Неаполь: Библиополь. ISBN 8870881059. OCLC 12731401 .

[2] Аренс, Бенедикт; Каприотти, Паоло; Спадотти, Режис (12 апреля 2015 г.). «Необоснованные деревья в теории гомотопических типов». arXiv : 1504.02949 . DOI : 10.4230 / LIPIcs.TLCA.2015.17 . Cite journal requires |journal= (help)

[3] Dybjer, Питер (1997). «Представление индуктивно определенных множеств порядками в теории типов Мартина-Лёфа». Теоретическая информатика . 176 (1–2): 329–335. DOI : 10.1016 / s0304-3975 (96) 00145-4 .

[4] Awodey, Стив; Гамбино, Никола; Соякова, Кристина (18.01.2012). «Индуктивные типы в теории гомотопических типов». arXiv : 1201.3898 [ math.LO ].

[5] Аренс, Бенедикт; Каприотти, Паоло; Спадотти, Режис (12 апреля 2015 г.). «Необоснованные деревья в теории гомотопических типов». arXiv : 1504.02949 . DOI : 10.4230 / LIPIcs.TLCA.2015.17 . Cite journal requires |journal= (help)

[6] Awodey, Стив; Гамбино, Никола; Соякова, Кристина (21.04.2015). «Гомотопически-начальные алгебры в теории типов». arXiv : 1504.05531 [ math.LO ].

[7] ван ден Берг, Бенно; Марчи, Федерико Де (2007). «Необоснованные деревья по категориям». Летопись чистой и прикладной логики . 146 (1): 40–59. arXiv : math / 0409158 . DOI : 10.1016 / j.apal.2006.12.001 .

[8] Эбботт, Майкл; Альтенкирх, Торстен; Гани, Нил (2005). «Контейнеры: конструирование строго положительных типов». Теоретическая информатика . 342 (1): 3–27. DOI : 10.1016 / j.tcs.2005.06.002 .

[1]