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

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

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

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

Фон

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

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

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

Идея

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

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

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

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

Так что если ${ displaystyle D}$ это определяемый тип и ${ displaystyle f}$ является ли функция (одновременно) определенной, эти объявления параметров положительны:

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

Это наполовину положительно:

${ Displaystyle к: (е d) к D}$ (Зависит от параметра ${ displaystyle d}$ типа ${ displaystyle D}$ но только через звонок ${ displaystyle f}$ .)

Это нет положительный или полуположительный:

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

Пример Вселенной

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

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

${ Displaystyle конструктор _ { Pi} (u: U) (u ': T (u) to U): U}$

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

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

${ displaystyle T (конструктор _ { Pi} (u, u '))}$ становится ${ Displaystyle prod _ {х: Т (и)} Т (и '(х))}$ .

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

использование

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

Смотрите также

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

внешняя ссылка

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

[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 - функционального языка с зависимыми типами». Доказательство теорем в логиках высокого порядка. Конспект лекций по информатике. Берлин, Гейдельберг: Springer: 73–78. Дои:10.1007/978-3-642-03359-9_6. ISBN 978-3-642-03359-9.

[1]

[2]

[3]