Индукция-индукция

В интуиционистской теории типов (ITT), некоторой дисциплине в рамках математической логики , индукция-индукция предназначена для одновременного объявления некоторого индуктивного типа и некоторого индуктивного предиката над этим типом.

Индуктивное определение дают правила порождения элементов некоторого типа. Затем можно определить некоторый предикат для этого типа, предоставив конструкторы для формирования элементов предиката, например, индуктивно в способе генерации элементов типа. Индукция-индукция обобщает эту ситуацию, поскольку можно одновременно определить тип и предикат, поскольку правила порождения элементов типа $A:{\mathsf {Type}}$ разрешено ссылаться на предикат $B:A\to {\mathsf {Type}}$ .

Индукцию-индукцию можно использовать для определения более крупных типов, включая различные конструкции вселенных в теории типов. ^[1] и предельные конструкции в теории категорий/топосов.

Пример 1 [ править ]

Представьте тип $A$ поскольку имеются следующие конструкторы, обратите внимание на раннюю ссылку на предикат $B$ :

$aa:A$
$\ell \ell :\sum _{x:A}B(x)\to A;$

и - одновременно представить сказуемое $B$ как имеющий следующие конструкторы:

${\mathsf {Tru}}:B(aa)$
${\mathsf {Fal}}:B(aa)$
если $x:A$ и $y:B(x)$ затем ${\mathsf {Zer}}:B(\ell \ell (x,y))$
если $x:A$ и $y:B(x)$ и $z:B(\ell \ell (x,y))$ затем ${\mathsf {Suc}}(z):B(\ell \ell (x,y))$ .

Пример 2 [ править ]

Простой общий пример — Вселенная типа Тарского. Это создает некоторый индуктивный тип $U:{\mathsf {Type}}$ и некоторый индуктивный предикат $T:U\to {\mathsf {Type}}$ . Для каждого типа в теории типов (кроме $U$ сам!), будет какой-то элемент $U$ который можно рассматривать как некоторый код для соответствующего типа; Предикат $T$ индуктивно кодирует каждый возможный тип в соответствующий элемент $U$ ; и создание новых кодов в $U$ потребует обращения к декодированию как типу более ранних кодов через предикат $T$ .

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

Индукция-рекурсия — для одновременного объявления некоторого индуктивного типа и некоторой рекурсивной функции над этим типом.

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

^ Дюбьер, Питер (июнь 2000 г.). «Общая формулировка одновременных индуктивно-рекурсивных определений в теории типов» (PDF) . Журнал символической логики . 65 (2): 525–549. CiteSeerX 10.1.1.6.4575 . дои : 10.2307/2586554 . JSTOR 2586554 . S2CID 18271311 .

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

Список публикаций Питера Дюбьера по индукции и индукционно-рекурсии.

[Dybjer-1] Дюбьер, Питер (июнь 2000 г.). «Общая формулировка одновременных индуктивно-рекурсивных определений в теории типов» (PDF) . Журнал символической логики . 65 (2): 525–549. CiteSeerX 10.1.1.6.4575 . дои : 10.2307/2586554 . JSTOR 2586554 . S2CID 18271311 .

[1]