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

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

Стандартный пример — кодирование натуральных чисел с использованием кодировки Пеано . Его можно определить в Coq следующим образом:

 Inductive nat : Type :=
   | 0 : nat
   | S : nat -> nat.

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

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

Ликвидация [ править ]

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

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

Другими словами: для любого предложения «P» над натуральными числами, учитывая доказательство «P 0» и доказательство «Pn -> P (n+1)», мы получаем обратно доказательство «для всех n, P n ". Это знакомый принцип индукции для натуральных чисел.

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

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

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

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

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

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

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

{\begin{aligned}f(\operatorname {inl} (1_{\mathbf {1} }))&=\mathbf {0} \\f(\operatorname {inr} (a))&=\mathbf {1} \end{aligned}}

и 1 ₁ является единственным обитателем 1 . Стоимость

f(\operatorname {inl} (1_{\mathbf {1} }))

соответствует конструктору пустого списка, тогда как значение

f(\operatorname {inr} (a))

соответствует конструктору, который добавляет a в начало другого списка.

Конструктор для элементов универсального 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-типы) могут быть определены с точностью до изоморфизма как исходные алгебры (соответственно конечные коалгебры) для полиномиальных функторов . В этом случае свойство инициалности (res.finality) непосредственно соответствует соответствующему принципу индукции. ^[3] В теориях интенсионального типа с аксиомой однолистности это соответствие сохраняется с точностью до гомотопии (пропозиционального равенства). ^[4]^[5]^[6]

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

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

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

Inductive even : nat -> Prop :=
  | zero_is_even : even O
  | S_of_odd_is_even : (forall n:nat, odd n -> even (S n))
with odd : nat -> Prop :=
  | S_of_even_is_odd : (forall n:nat, even n -> odd (S n)).

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

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

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

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

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

Типы с более высокой индуктивностью [ править ]

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

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

основа : круг

и петля;

цикл : база = база .

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

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

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

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

^ Мартин-Лёф, Пер (1984). Интуиционистская теория типов (PDF) . Самбин, Джон. Неаполь: Библиополис. ISBN 8870881059 . ОСЛК 12731401 .
^ Аренс, Бенедикт; Каприотти, Паоло; Спадотти, Режис (12 апреля 2015 г.). Необоснованные деревья в гомотопической теории типов . Международные труды Лейбница по информатике (LIPIcs). Том. 38. стр. 17–30. arXiv : 1504.02949 . doi : 10.4230/LIPIcs.TLCA.2015.17 . ISBN 9783939897873 . S2CID 15020752 .
^ Дюбьер, Питер (1997). «Представление индуктивно определенных множеств с помощью хорошего порядка в теории типов Мартина-Лёфа». Теоретическая информатика . 176 (1–2): 329–335. дои : 10.1016/s0304-3975(96)00145-4 .
^ Аводи, Стив; Гамбино, Никола; Соякова, Кристина (18 января 2012 г.). «Индуктивные типы в теории гомотопических типов». arXiv : 1201.3898 [ math.LO ].
^ Аренс, Бенедикт; Каприотти, Паоло; Спадотти, Режис (12 апреля 2015 г.). Необоснованные деревья в гомотопической теории типов . Международные труды Лейбница по информатике (LIPIcs). Том. 38. стр. 17–30. arXiv : 1504.02949 . doi : 10.4230/LIPIcs.TLCA.2015.17 . ISBN 9783939897873 . S2CID 15020752 .
^ Аводи, Стив; Гамбино, Никола; Соякова, Кристина (21 апреля 2015 г.). «Гомотопически-начальные алгебры в теории типов». arXiv : 1504.05531 [ math.LO ].
^ ван ден Берг, Бенно; Марки, Федерико Де (2007). «Необоснованные деревья в категориях». Анналы чистой и прикладной логики . 146 (1): 40–59. arXiv : math/0409158 . дои : 10.1016/j.apal.2006.12.001 . S2CID 360990 .
^ Эбботт, Майкл; Альтенкирх, Торстен; Гани, Нил (2005). «Контейнеры: построение строго положительных типов» . Теоретическая информатика . 342 (1): 3–27. CiteSeerX 10.1.1.166.34 . дои : 10.1016/j.tcs.2005.06.002 .

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

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

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

[2] Аренс, Бенедикт; Каприотти, Паоло; Спадотти, Режис (12 апреля 2015 г.). Необоснованные деревья в гомотопической теории типов . Международные труды Лейбница по информатике (LIPIcs). Том. 38. стр. 17–30. arXiv : 1504.02949 . doi : 10.4230/LIPIcs.TLCA.2015.17 . ISBN 9783939897873 . S2CID 15020752 .

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

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

[5] Аренс, Бенедикт; Каприотти, Паоло; Спадотти, Режис (12 апреля 2015 г.). Необоснованные деревья в гомотопической теории типов . Международные труды Лейбница по информатике (LIPIcs). Том. 38. стр. 17–30. arXiv : 1504.02949 . doi : 10.4230/LIPIcs.TLCA.2015.17 . ISBN 9783939897873 . S2CID 15020752 .

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

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

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

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]