Индукция-рекурсия

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

Индуктивное определение дается правилами порождения элементов типа. Затем можно определить функции этого типа путем индукции по способу генерации элементов этого типа. Индукция-рекурсия обобщает эту ситуацию, поскольку можно одновременно определить тип и функцию, поскольку правилам генерации элементов типа разрешено ссылаться на функцию. ^[1]

Индукцию-рекурсию можно использовать для определения больших типов, включая различные конструкции юниверсов. Это существенно увеличивает теоретико-доказательную силу теории типов. Тем не менее, индуктивно-рекурсивные рекурсивные определения по-прежнему считаются предикативными .

Предыстория [ править ]

Индукция-рекурсия возникла в результате исследований правил интуиционистской теории типов Мартина-Лёфа . Теория типов имеет ряд «формирователей типов» и четыре вида правил для каждого из них. Мартин-Лёф намекнул, что правила для каждого формирователя типа следуют шаблону, который сохраняет свойства теории типов (например, сильная нормализация , предикативность ). Исследователи начали искать наиболее общее описание шаблона, поскольку оно могло бы указать, какие типы формирователей типов можно добавить (или не добавлять!) для расширения теории типов.

Формирователь типа «вселенная» был наиболее интересным, потому что, когда правила были написаны «а-ля Тарский», они одновременно определяли «тип вселенной» и функцию, которая с ней работала. В конечном итоге это привело Дюбьера к индукции-рекурсии.

В первых статьях Дюбьера индукция-рекурсия называлась «схемой» правил. В нем говорилось, какие формирователи типов можно добавить в теорию типов. Позже он и Сетцер напишут новый формирователь типов с правилами, которые позволят создавать новые определения индукции-рекурсии внутри теории типов. ^[2] Это было добавлено в помощник Halfproof (вариант Alf ).

Идея [ править ]

Прежде чем рассматривать индуктивно-рекурсивные типы, рассмотрим более простой случай — индуктивные типы. Конструкторы для индуктивных типов могут быть самоссылающимися, но ограниченным образом. Параметры конструктора должны быть «положительными»:

не ссылаться на определяемый тип
быть точно определяемым типом, или
быть функцией, которая возвращает определяемый тип.

При использовании индуктивных типов тип параметра может зависеть от более ранних параметров, но они не могут ссылаться на параметры определяемого типа. Индуктивно-рекурсивные типы идут дальше, и типы параметров могут ссылаться на более ранние параметры, которые используют определяемый тип. Они должны быть «полуположительными»:

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

Итак, если $D$ определяется тип и $f$ определяется ли функция (одновременно), эти объявления параметров являются положительными:

$a:A$
$d:D$
$g:A\to Type$
$h:A\to D$
$i:A\to B\to D$
$j:g\ a$ (Зависит от предыдущих параметров, ни один из которых не является типом. $D$ .)

Это полупозитивно:

$k:(f\ d)\to D$ (Зависит от параметра $d$ типа $D$ но только через звонок $f$ .)

Они не являются ни положительными, ни полуположительными:

$k:D\to A$ ( $D$ является параметром функции.)
$l:(A\to D)\to A$ (Параметр принимает функцию, которая возвращает $D$ , но возвращает $A$ себя.)
$m:z\ d$ (Зависит от $d$ типа $D$ , но не через функцию $f$ .)

Пример вселенной [ править ]

Простой общий пример — Вселенная типа Тарского. Он создает тип $U$ и функция $T$ . Есть элемент $U$ для каждого типа в теории типов (кроме $U$ сам!). Функция $T$ отображает элементы $U$ к связанному типу.

Тип $U$ имеет конструктор (или правило введения) для каждого формирователя типа в теории типов. Для зависимых функций будет:

$constructor_{\Pi }(u:U)(u':T(u)\to U):U$

То есть он принимает элемент $u$ типа $U$ который будет соответствовать типу параметра и функции $u'$ такой, что для всех значений $x:T(u)$ , $u'(x)$ сопоставляется с типом возвращаемого значения функции (который зависит от значения параметра, $x$ ). (Финальный $:U$ говорит, что результатом конструктора является элемент типа $U$ .)

Правило редукции (или правила вычислений) гласит, что

$T(constructor_{\Pi }(u,u'))$ становится $\prod _{x:T(u)}T(u'(x))$ .

После сокращения функция $T$ работает с меньшей частью входа. Если это так, когда $T$ применяется к любому конструктору, то $T$ всегда будет прекращено. Не вдаваясь в подробности, Индукция-Рекурсия утверждает, какие определения (или правила) можно добавить в теорию, чтобы вызовы функций всегда завершались.

Использование [ править ]

Индукция-рекурсия реализована в Agda и Idris . ^[3]

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

Индукция-индукция – дальнейшая работа, определяющая тип и семейство типов одновременно.

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

^ Дюбьер, Питер (июнь 2000 г.). «Общая формулировка одновременных индуктивно-рекурсивных определений в теории типов» (PDF) . Журнал символической логики . 65 (2): 525–549. CiteSeerX 10.1.1.6.4575 . дои : 10.2307/2586554 . JSTOR 2586554 . S2CID 18271311 .
^ Дюбьер, Питер (1999). «Конечная аксиоматизация индуктивно-рекурсивных определений». Типизированные лямбда-исчисления и приложения . Конспекты лекций по информатике. Том. 1581. стр. 129–146. CiteSeerX 10.1.1.219.2442 . дои : 10.1007/3-540-48959-2_11 . ISBN 978-3-540-65763-7 .
^ Бове, Ана; Дюбьер, Питер; Норелл, Ульф (2009). «Краткий обзор Agda — функционального языка с зависимыми типами» . В Бергхофере, Стефан; Нипков, Тобиас; Городской, христианский; Венцель, Макариус (ред.). Доказательство теорем в логике высшего порядка . Конспекты лекций по информатике. Том. 5674. Берлин, Гейдельберг: Springer. стр. 73–78. дои : 10.1007/978-3-642-03359-9_6 . ISBN 978-3-642-03359-9 .

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

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

[DybjerSetzer-2] Дюбьер, Питер (1999). «Конечная аксиоматизация индуктивно-рекурсивных определений». Типизированные лямбда-исчисления и приложения . Конспекты лекций по информатике. Том. 1581. стр. 129–146. CiteSeerX 10.1.1.219.2442 . дои : 10.1007/3-540-48959-2_11 . ISBN 978-3-540-65763-7 .

[3] Бове, Ана; Дюбьер, Питер; Норелл, Ульф (2009). «Краткий обзор Agda — функционального языка с зависимыми типами» . В Бергхофере, Стефан; Нипков, Тобиас; Городской, христианский; Венцель, Макариус (ред.). Доказательство теорем в логике высшего порядка . Конспекты лекций по информатике. Том. 5674. Берлин, Гейдельберг: Springer. стр. 73–78. дои : 10.1007/978-3-642-03359-9_6 . ISBN 978-3-642-03359-9 .

[1]

[2]

[3]