Интуиционистична теория на типа

2023 Автор: Noah Black | [email protected]. Последно модифициран: 2023-08-25 04:38

Навигация за влизане

• Съдържание за участие
• библиография
• Академични инструменти
• Friends PDF Preview
• Информация за автора и цитирането
• Върнете се в началото

Интуиционистична теория на типа

Публикувана за първи път пет февруари 2016 г.; съществена ревизия пн 8 юни 2020 г.

Интуиционистичната теория на типа (също теория на конструктивния тип или теорията на типа Мартин-Льоф) е формална логическа система и философска основа за конструктивна математика. Това е пълномащабна система, която има за цел да изиграе подобна роля за конструктивната математика, както теорията на множествата на Зермело-Френкел за класическата математика. Той се основава на принципа на предложенията като видове и изяснява интерпретацията на интуиционистичната логика на Брууер-Хейтинг-Колмогоров. Той разширява тази интерпретация до по-общата настройка на теорията на интуиционистичния тип и по този начин дава обща представа не само за това какво е конструктивно доказателство, но и какво е конструктивен математически обект. Основната идея е математическите понятия като елементи, набори и функции да се обясняват по отношение на понятия от програмиране като структури от данни, т.е.типове данни и програми. Тази статия описва формалната система на теорията на интуиционистичния тип и нейните семантични основи.

В този запис първо даваме преглед на най-важните аспекти на теорията на интуиционистичния тип - един вид „разширено абстрактно“. Той е предназначен за читател, който вече донякъде е запознат с теорията. Раздел 2, от друга страна, е предназначен за читател, който е нов за теорията на интуиционистичния тип, но запознат с традиционната логика, включително логиката на предложенията и предиката, аритметиката и теорията на множествата. Тук неформално представяме няколко аспекта, което отличава интуиционистичната теория на типа от тези традиционни теории. В раздел 3 представяме основна версия на теорията, близка до първата публикувана версия на Мартин-Льоф от 1972 г. Читателят, който бе заинтригуван от неформалността на раздел 2, сега ще види подробно как е изградена теорията. Тогава раздел 4 представя редица важни разширения на основната теория. По-специално,тя подчертава централната роля на индуктивните (и индуктивно-рекурсивните) определения. Раздел 5 представя основните философски идеи, включително теорията на смисъла, разработена от Мартин-Льоф. Докато раздел 5 е за философията и основите, раздел 6 дава преглед на математическите модели на теорията. Накрая в раздел 7 описваме няколко важни вариации на основната „интензивна“теория на Мартин-Льоф, описани в раздели 3 и 4.описваме няколко важни вариации на основната „интензивна“теория на Мартин-Льоф, описани в раздели 3 и 4.описваме няколко важни вариации на основната „интензивна“теория на Мартин-Льоф, описани в раздели 3 и 4.

• 1. Преглед

• 2. Предложения като видове

  • 2.1 Интуиционистична теория на типа: нов начин на поглед към логиката?
  • 2.2 Кореспонденцията на Къри-Хауърд
  • 2.3 Комплекти от доказателства
  • 2.4 Зависими типове
  • 2.5 Предложения като типове в интуиционистичната теория на типа

• 3. Основна интуиционистка теория на типа

  • 3.1 Решения
  • 3.2 Форми на съдебно решение
  • 3.3 Правила за заключение
  • 3.4 Интуиционистична предикатна логика
  • 3.5 Естествени числа
  • 3.6 Вселената на малките типове
  • 3.7 Предлагаща идентичност
  • 3.8 Аксиомата на избора е теорема

• 4. Разширения

  • 4.1 Логическата рамка
  • 4.2 Общ тип идентичност
  • 4.3 Добре установени дървета
  • 4.4 Итеративни комплекти и CZF
  • 4.5 Индуктивни дефиниции
  • 4.6 Индуктивно-рекурсивни определения

• 5. Значение Обяснения

  • 5.1 Изчисляване на канонична форма
  • 5.2 Значението на категоричните решения
  • 5.3 Значението на хипотетичните преценки

• 6. Математически модели

  • 6.1 Категорични модели
  • 6.2 Зададен теоретичен модел
  • 6.3 Модели на реализация
  • 6.4 Модел на нормални форми и проверка на типа

• 7. Варианти на теорията

  • 7.1 Теория на разширения тип
  • 7.2 Уникални основи и теория на типа на хомотопията
  • 7.3 Частична и нестандартна теория на типа
  • 7.4 Непредпазлива теория на типа
  • 7.5 Асистенти за доказване
• библиография
• Академични инструменти
• Други интернет ресурси
• Свързани записи

1. Преглед

Започваме с гледка от птичи поглед към някои важни аспекти на теорията на интуиционистичния тип. Читателите, които не са запознати с теорията, може да предпочетат да я пропуснат на първо четене.

Произходът на теорията на интуиционистичния тип са интуиционизмът на Броувър и теорията на Ръсел. Подобно на класическата проста теория на типовете на Църквата, тя се основава на изчислението на ламбда с типове, но се различава от това по това, че се основава на принципа на предложенията като видове, открит от Curry (1958) за логика на предложенията и разширен до логиката на предиката Хауърд (1980) и де Бруйн (1970). Това разширение стана възможно чрез въвеждането на индексирани семейства от типове (зависими типове) за представяне на предикатите на предикатната логика. По този начин всички логически съединители и количествени средства могат да бъдат интерпретирани от формати за тип. В интуиционистичната теория на типа се добавят и други типове като вид естествени числа, тип малки типове (вселена) и тип добре обосновани дървета. Получената теория съдържа интуиционистична теория на числата (Хейтинг аритметика) и много други.

Теорията е формулирана в естествена дедукция, където правилата за всеки тип бивши са класифицирани като правила за формиране, въвеждане, премахване и равенство. Тези правила показват определени прилики между правилата за въвеждане и елиминиране след третирането на естествената дедукция на Гентцен и Правиц, както е обяснено във вписването за доказателствено-теоретичната семантика.

Елементите на предложенията, когато се интерпретират като видове, се наричат доказателствени обекти. Когато доказателствените обекти се прибавят към изчислението на естествената дедукция, тя се превръща в типично изчисляване на ламбда с зависими типове, което разширява оригиналното набрано от църквата лямбда. Правилата за равенство са правила за изчисление за условията на това смятане. Всяка функция, определена в теорията, е тотална и изчислима. Следователно интуиционистичната теория на типовете е типизиран функционален език за програмиране с необичайното свойство, което всички програми прекратяват.

Интуиционистичната теория на типа е не само формална логическа система, но също така осигурява цялостна философска рамка за интуиционизма. Това е тълкуван език, където разликата между демонстрацията на решение и доказателството за предложение играе основна роля (Sundholm 2012). Рамката изяснява интерпретацията на интуиционистичната логика на Брууер-Хейтинг-Колмогоров и я разширява до по-общата настройка на теорията на интуиционистичния тип. По този начин тя предлага обща представа не само за това какво е конструктивно доказателство, но и за това какво е конструктивен математически обект. Значението на преценките на теорията на интуиционистичния тип се обяснява по отношение на изчисленията на каноничните форми на типове и термини. Тези неформални,обясненията с интуитивно значение са „пред-математически“и трябва да се противопоставят на формалните математически модели, разработени в стандартна математическа рамка, като теорията на множествата.

Тази теория на смисъла също така оправдава различни индуктивни, рекурсивни и индуктивно-рекурсивни определения. Въпреки че теоретично силните теории могат да бъдат оправдани, например аналози на някои големи кардинали, системата се счита за предикативна. Безсмислените дефиниции от рода, открити в логиката от по-висок ред, интуиционистичната теория на множествата и теорията на топоса, не са част от теорията. Нито е принципът на Марков и по този начин теорията се отличава от руския конструктивизъм.

Алтернативна формална логическа система за предиктивна конструктивна математика е конструктивната теория на множествата Zermelo-Fraenkel (CZF) на Myhill and Aczel. Тази теория, която се основава на интуиционистичната логика на предикат от първи ред и отслабва някои от аксиомите на класическата теория на множеството на Зермело-Френкел, има естествена интерпретация в интуиционистичната теория на типа. Следователно обясненията на Мартин-Льоф за значението също косвено формират основа за CZF.

Вариантите на теорията на интуиционистичния тип са в основата на няколко широко използвани асистенти за доказателство, включително NuPRL, Coq и Agda. Тези асистенти за доказателство са компютърни системи, които са били използвани за формализиране на големи и сложни доказателства за математически теореми, като теорията на четирите цвята в теорията на графите и теорията на Фейт-Томпсън в теорията на крайните групи. Те също са били използвани за доказване на правилността на реалистичен компилатор C (Leroy 2009) и друг компютърен софтуер.

Философски и практически теорията на интуиционистичния тип е основополагаща рамка, в която конструктивната математика и компютърното програмиране са в дълбок смисъл еднакви. Тази точка е подчертана от (Gonthier 2008) в документа, в който той описва доказателствата си за теорията на четирите цвята:

Подходът, който се оказа успешен за това доказателство, беше да превърне почти всяка математическа концепция в структура от данни или програма в системата Coq, като по този начин превърне цялото предприятие в такова за проверка на програмата.

2. Предложения като видове

2.1 Интуиционистична теория на типа: нов начин на поглед към логиката?

Интуиционистичната теория на типа предлага нов начин за анализ на логиката, главно чрез въвеждането на явни доказателства. Това осигурява директна изчислителна интерпретация на логиката, тъй като за доказателствата има правила за изчисление. По отношение на експресивната сила теорията на интуиционистичния тип може да се разглежда като разширение на логиката от първи ред, много по-скоро като логика от по-висок ред, но предикативна.

2.1.1 Теория на типа

Ръсел разработи теорията на типа в отговор на откритието си за парадокс в теорията на наивните множества. В неговата теория за разклонен тип математическите обекти се класифицират според техните типове: тип предложения, тип предмети, вид свойства на предмети и др. Когато Чърч разработва своята проста теория за типовете въз основа на типизирана версия на неговия ламбда смятане той добави правилото, че има тип функции между всеки два типа теория. Интуиционистичната теория на типа допълнително разширява просто набраното ламбда смятане с зависими типове, тоест индексирани семейства от типове. Пример е семейството от типове (n) - кортежи, индексирани с (n).

Видовете са широко използвани в програмирането от дълго време. Ранните езици за програмиране на високо ниво въведоха видове цели числа и числа с плаваща запетая. Съвременните езици за програмиране често имат системи с богат тип с много конструкции за формиране на нови типове. Интуиционистичната теория на типовете е функционален език за програмиране, където системата от типа е толкова богата, че практически всяко мислимо свойство на програмата може да бъде изразено като тип. Така типовете могат да се използват като спецификации на задачата на дадена програма.

2.1.2 Интуитивна логика с обекти с доказателство

Анализът на Брауър на логиката го доведе до интуиционистична логика, която отхвърля закона на изключената средна и закона на двойното отрицание. Тези закони не са валидни в теорията на интуиционистичния тип. По този начин тя не съдържа класическа (пеано) аритметика, а само интуиционистична (хейтинг) аритметика. (Друг е въпросът, че аритметиката на Peano може да бъде интерпретирана в аритмията Heyting чрез интерпретация на двойното отрицание, вижте вписването на интуиционистичната логика.)

Помислете за теорема за интуиционистична аритметика, каквато е теоремата за разделянето

) forall m, n. m> 0 / supset / съществува q, r. mq + r = n / клин m> r)

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

Когато теоремата за разделянето се докаже в теорията на интуиционистичния тип, ние не изграждаме само формално доказателство в обичайния смисъл, но и конструкция (или доказателствен обект) „(divi)“, която свидетелства за истинността на теоремата. Ние пишем

) divi: / forall m, n {:} N. \, m> 0 / supset / съществува q, r {:} N. \, mq + r = n / klin m> r)

да изразим, че (divi) е доказателствен обект за теоремата за разделянето, тоест елемент от типа, представляващ теоремата за разделянето. Когато предложенията са представени като видове, кванторът (forall) - идентификаторът се идентифицира с бившия зависим от функционалното пространство (или общо декартово изделие) (Pi), (съществува) - количественото число със зависимите двойки напишете бивша (или обща несъответстваща сума) (Sigma), връзка (клин) с декартово изделие (пъти), отношението на идентичност = с типа бивш (I) на доказателствени обекти на идентичности и по-голямото от отношение (>) с типа бивш (GT) на доказателствени обекти с по-големи от изразите. Използвайки „type-notation“по този начин пишем

) divi: / Pi m, n {:} N. \, / GT (m, 0) rightarrow / Sigma q, r {:} N. \, / I (N, mq + r, n) пъти / GT (m, r))

да се изрази, че доказателният обект „(divi)“е функция, която картографира две числа (m) и (n) и доказателствен обект (p), свидетелстващи за това, че (m> 0) до четворка ((q, (r, (s, t)))), където (q) е коефициентът и (r) е останалата част, получена при разделяне (n) на (т). Третият компонент (s) е доказателствен обект, свидетел на факта, че (mq + r = n), а четвъртият компонент (t) е доказателствен обект, свидетел (m> r).

От съществено значение, (divi) не е само функция в класическия смисъл; тя също е функция в интуиционистичния смисъл, тоест програма, която изчислява изхода ((q, (r, (s, t)))), когато е дадена (m), (n), (p) като входни данни. Тази програма е термин в ламбда смятане със специални константи, тоест програма на функционален език за програмиране.

2.1.3 Разширение на логиката на предикат от първи ред

Интуиционистичната теория на типовете може да се разглежда като разширение на логиката от първи ред, доколкото логиката от по-висок ред е разширение на логиката от първи ред. В по-висок ред логика намираме някои отделни домейни, които могат да бъдат интерпретирани като всеки набор, който ни харесва. Ако в подписа има релационни константи, те могат да бъдат интерпретирани като всякакви отношения между множествата, интерпретиращи отделните домейни. На всичкото отгоре можем да определим количествено отношенията и връзките на отношенията и т.н. Можем да мислим за логиката от по-висок ред като логика от първи ред, оборудвана с начин за въвеждане на нови области на количествено определяне: ако (S_1, / ldots, S_n) са домейни за количествено определяне, тогава ((S_1, / ldots, S_n)) е нов домейн за количествено определяне, състоящ се от всички n-арни отношения между домейните (S_1, / ldots, S_n). Логиката от по-висок ред има пряка теоретично зададена теоретична интерпретация, където ((S_1, / ldots, S_n)) се интерпретира като набор от мощност (P (A_1 / times / cdots / пъти A_n)), където (A_i) е интерпретацията на (S_i), за (i = 1, / ldots, n). Това е вид логика от по-висок ред или проста теория за типовете, които Рамзи, Църква и други въведоха.

Интуиционистичната теория на типа може да се разглежда по подобен начин, само че тук възможностите за въвеждане на домейни за количествено определяне са по-богати, човек може да използва (Sigma, / Pi, +, / I), за да конструира нови от стари. (Раздел 3.1; Martin-Löf 1998 [1972]). Интуиционистичната теория на типовете също има пряка теоретично множествена теоретична интерпретация, където (Sigma), (Pi) и т. Н. Се интерпретират като съответните конструктивни теоретични множества; виж отдолу. Към интуиционистичния тип теория можем да добавим неуточнени отделни домейни, точно както в HOL. Те се интерпретират като множества, както за HOL. Сега показваме разлика от HOL: в теорията за интуиционистичен тип можем да въведем неуточнени семейни символи. Можем да представим (T) като група от типове над отделния домейн (S):

[T (х); { rm type}; (x {:} S).)

Ако (S) се интерпретира като (A), (T) може да се интерпретира като всяко семейство от множества, индексирани с (A). Като не-математически пример, можем да представим бинарната връзка любов между членове на отделен домейн от хора, както следва. Представете двоичното семейство Loves над домейна People

[{ rm обича} (x, y); { rm type}; (x {:} { rm Хора}, y {:} { rm Хора}).)

Интерпретацията може да бъде всяко семейство от множества (B_ {x, y}) ((x {:} A), (y {:} A)). Как това обхваща стандартното понятие за отношение? Да предположим, че имаме двоично отношение (R) на (A) в познатия теоретично зададен набор. Можем да направим двоично семейство, съответстващо на това, както следва

[B_ {x, y} = / начало {случаи} {0 } & / текст {ако} R (x, y) текст {има} / \ varnothing & / text {if} R (x, y) текст {е невярно.} край {случаи})

Сега ясно (B_ {x, y}) не е празно, ако и само ако (R (x, y)) е валидно. (Бихме могли да изберем друг елемент от нашата теоретична вселена, различен от 0, за да посочим истината.) Следователно от всяко отношение можем да изградим семейство, чиято истина на (x, y) е еквивалентна на (B_ {x, y}) да бъде непразна. Обърнете внимание, че това тълкуване не се интересува какво е доказателството за (R (x, y)), а само това, че има. Спомнете си, че теорията на интуиционистичния тип интерпретира предложенията като типове, така че (p {:} { rm обича} ({ rm John}, { rm Mary})) означава, че ({ rm обича} ({ rm Джон}, { rm Мери})) е вярно.

Тълкуването на отношенията като семейства позволява да се проследяват доказателства или доказателства, които има (R (x, y)), но може също да изберем да го игнорираме.

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

За разлика от това как би се справила математическата връзка (>) между естествените числа в интуиционистичната теория на типа? На първо място се нуждаем от тип числа (N). По принцип бихме могли да въведем неопределен индивидуален домейн (N) и след това да добавим аксиоми, точно както правим в логиката от първи ред, когато настроихме аксиомната система за аритметика на Peano. Това обаче не би ни дало желаната изчислителна интерпретация. Така както е обяснено по-долу, ние определяме правила за въвеждане за изграждане на нови естествени числа в (N) и правила за елиминиране и изчисляване за дефиниране на функции на (N) (чрез рекурсия). Стандартното отношение на поръчката (>) трябва да отговаря

) mbox {(x> y) ако съществува (z {:} N) такъв, че (y + z + 1 = x)}.)

Дясната ръка е представена като (Sigma z {:} N. \, / I (N, y + z + 1, x)) в теорията на интуиционистичния тип и приемаме това като определение на отношение (>). ((+) се определя от рекурсивни уравнения, (I) е конструкцията на типа на идентичност). Сега всички свойства на (>) се определят от споменатите правила за въвеждане и премахване и изчисление за (N).

2.1.4 Логика с няколко форми на преценка

Типовата система на интуиционистичната теория на типа е много изразителна. В резултат на това добре оформеността на даден тип вече не е просто въпрос на разбор, а е нещо, което трябва да бъде доказано. Добре оформеността на типа е една форма на преценка на интуиционистичната теория на типа. Добро типизирането на термин по отношение на тип е друго. Освен това има решения за равенство за типове и термини. Това е още един начин, по който интуиционистичната теория на типа се различава от обикновената логика от първи ред с фокуса си върху единствената преценка, изразяваща истинността на едно предложение.

2.1.5 Семантика

Докато стандартното представяне на логиката от първи ред би следвало Тарски при дефинирането на понятието модел, интуиционистичната теория на типа следва традицията на теорията на смисъла на Брууер, както е разработена още от Хейтинг и Колмогоров, така наречената BHK-интерпретация на логиката. Ключовият момент е, че доказателството за импликация (A / supset B) е метод, който преобразува доказателство за (A) в доказателство за (B). В теорията на интуиционистичния тип този метод официално е представен от програмата (f {:} A / supset B) или (f {:} A / rightarrow B): типът доказателства за импликация (A / supset B) е типът функции, който преобразува доказателствата на (A) в доказателства на (B).

Освен това, докато семантиката на Тарски обикновено се представя мета-математически и предполага теория на множествата, теорията на смисъла на Мартин-Льоф на теорията на интуиционистичния тип трябва да се разбира директно и „пред-математически“, тоест, без да се предполага мета-език като теорията на множествата,

2.1.6 Функционален език за програмиране

Читателите с предистория в смятането на ламбда и функционалното програмиране могат да получат алтернативно първо сближаване на теорията на интуиционистичния тип, като мислят за него като за типизиран функционален език за програмиране в стила на Haskell или за един от диалектите на ML. Въпреки това, тя се различава от тях в два основни аспекта: (i) има зависими типове (виж по-долу) и (ii) всички програми за типизиране се прекратяват. (Обърнете внимание, че теорията на интуиционистичния тип повлия на последните разширения на Haskell с обобщени алгебрични типове данни, които понякога могат да играят подобна роля като индуктивно дефинираните зависими типове.)

2.2 Кореспонденцията на Къри-Хауърд

Както вече споменахме, принципът, че

предложение е видът на неговите доказателства.

е основен за интуиционистичната теория на типа. Този принцип е известен още като кореспонденцията на Къри-Хауърд или дори изоморфизма на Къри-Хауърд. Къри откри съответствие между импликативния фрагмент от интуиционистичната логика и просто набраното ламбда-смятане. Хауърд разшири тази кореспонденция до предикатната логика от първи ред. В интуиционистичната теория на типа тази кореспонденция се превръща в идентификация на предложение и типове, което е разширено и включва количествено определяне на по-високи типове и други.

2.3 Комплекти от доказателства

И така, какви са тези доказателствени обекти? Те не трябва да се смятат за логически изводи, а по-скоро като някакви (структурирани) символични доказателства, че нещо е истина. Друг термин за такива доказателства е „създател на истината“.

Поучително е като малко грубо първо приближение да замените типовете с обикновени множества в тази кореспонденция. Определете набор (E_ {m, n}), в зависимост от (m, n / в {{ mathbb N}}), чрез:

) E_ {m, n} = / наляво { начало {масив} {ll} {0 } & / mbox {ако (m = n)} / \ varnothing & / mbox {ако (m / ne n).} край {масив} вдясно.)

Тогава (E_ {m, n}) не е празен точно когато (m = n). Множеството (E_ {m, n}) съответства на предложението (m = n), а числото (0) е обект на доказателство (създател на истината), обитаващ множествата (E_ {т, т}).

Помислете, че (m) е четно число, изразено като формулата (съществува n / в {{ mathbb N}}. M = 2n). Можем да изградим набор от обекти за доказване, съответстващи на тази формула, като използваме общата операция за сумирано теоретично задаване. Да предположим, че (A_n) ((n / в {{ mathbb N}})) е семейство от множества. Тогава несъответстващата му сума се дава от множеството двойки

[(Сигма n / в {{ mathbb N}}) A_n = {(n, a): n / в {{ mathbb N}}, a / в A_n }.)

Ако приложим тази конструкция към семейството (A_n = / E_ {m, 2n}), виждаме, че ((Sigma n / в {{ mathbb N}}) E_ {m, 2n}) е непусто точно когато има (n / в {{ mathbb N}}) с (m = 2n). Използвайки общата операция с теоретично задаване на продукти ((Pi n / в {{ mathbb N}}) A_n) можем по подобен начин да получим набор, съответстващ на универсално количествено определение.

2.4 Зависими типове

В теорията на интуиционистичния тип съществуват примитивни формообразуващи типове (Sigma) и (Pi) за общи суми и продукти и (I) за типове идентичност, аналогични на описаните по-горе теоретично зададени конструкции. Типът идентичност (I (N, m, n)), съответстващ на множеството (E_ {m, n}), е пример за зависим тип, тъй като зависи от (m) и (н). Нарича се също индексирано семейство от типове, тъй като е семейство от типове, индексирани с (m) и (n). По подобен начин можем да формираме общата несъвместима сума (Sigma x {:} A. \, B) и общата декартова продукция (Pi x {:} A. \, B) на такова семейство от типове (B) индексиран с (x {:} A), съответстващ на зададената теоретична сума и операции с продукти по-горе.

Зависимите типове също могат да бъдат определени чрез примитивна рекурсия. Пример е типът (n) - кортежи (A ^ n) на елементи от тип (A) и индексирани с (n {:} N), дефинирани от уравненията

) начало {подравняване *} A ^ 0 & = 1 \\ A ^ {n + 1} & = A / пъти A ^ n / край {подравняване *})

където (1) е един елемент, а (пъти) означава декартово произведение от два типа. Забелязваме, че зависимите типове въвеждат изчисления във типове: дефиниращите правила по-горе са изчислителни правила. Например резултатът от изчисляването (A ^ 3) е (A / пъти (A / пъти (A / пъти 1))).

2.5 Предложения като типове в интуиционистичната теория на типа

С предложенията като типове предикатите стават зависими типове. Например предикатът (mathrm {Prime} (x)) се превръща в типа доказателства, които (x) са първични. Този тип зависи от (x). По същия начин (x <y) е типът доказателства, че (x) е по-малък от (y).

Според интерпретацията на Curry-Howard на предложенията като типове, логическите константи се интерпретират като формообразуватели на типове:

) начало {подравняване *} бот & = / варно нещо \\ / топ & = 1 \\ A / vee B & = A + B \\ A / клин B & = A / пъти B \\ A / supset B & = A / rightarrow B \\ / съществува x {:} A. \, B & = / Sigma x {:} A. \, B \\ / forall x {:} A. \, B & = / Pi x {:} A. \, B / end {align *})

където (Sigma x {:} A. \, B) е разсеяната сума на семейството (A) - индексирано от типове (B) и (Pi x {:} A. \, B) е декартовият му продукт. Каноничните елементи на (Sigma x {:} A. \, B) са двойки ((a, b)) такива, че (a {:} A) и (b {:} B [x: = a]) (типът, получен чрез заместване на всички свободни събития на (x) в (B) с (a)). Елементите на (Pi x {:} A. \, B) са (изчислими) функции (f) такива, че (f \, a {:} B [x: = a]), всеки път (a {:} A).

Например, помислете за предложението

) започнем {уравнение} forall m {:} N. \, / съществува n {:} N. \, m / lt n / wedge / mathrm {Prime} (n) tag {1} етикет {prop1} край {уравнение})

изразявайки, че има произволно големи прайми. При интерпретацията на Curry-Howard това става тип (Pi m {:} N. \, / Sigma n {:} N. \, m / lt n / times / mathrm {Prime} (n)) на функции, които преобразуват число (m) в тройка ((n, (p, q))), където (n) е число, (p) е доказателство, че (m / lt n) и (q) е доказателство, че (n) е първостепенно. Това е принципът на доказателствата като програмен: конструктивното доказателство, че има произволно големи прайсове се превръща в програма, която при всяко число произвежда по-голям премиум заедно с доказателства, че той наистина е по-голям и наистина е първичен.

Обърнете внимание, че доказателството, което произтича противоречие от предположението, че има най-голям премиум, не е конструктивно, тъй като не дава изрично начин да се изчисли още по-голям премиум. За да превърнем това доказателство в конструктивно, трябва да покажем изрично как да изградим по-големия прайс. (Тъй като предложението (ref {prop1}) по-горе е формула (Pi ^ 0_2), можем например да използваме A-превод на Фридман, за да превърнем такова доказателство в класическата аритметика в доказателство в интуиционистична аритметика и по този начин в а доказателство в теорията на интуиционистичния тип.)

3. Основна интуиционистка теория на типа

Сега представяме основна версия на теорията на интуиционистичния тип, тясно свързана с първата версия на теорията, представена от Мартин-Льоф през 1972 г. (Martin-Löf 1998 [1972]). В допълнение към формообразувателите на типове, необходими за интерпретацията на Curry-Howard на въведената интуиционистка логика на предикати, изброени по-горе, имаме два типа: тип (N) на естествени числа и тип (U) на малки типове.

Може да се покаже, че получената теория съдържа интуиционистична теория на числата (HA) (айетична аритметика), система на Гьодел (T) на примитивни рекурсивни функции от по-висок тип и теорията (HA ^ / omega) на аритмията от Хейтинг от по-висок тип.

Тази основна интуиционистка теория на типа е не само оригиналната, но може би и минималната версия, която показва основните характеристики на теорията. По-късните разширения с примитивни типове идентичност, добре обосновани типове дървета, вселенски йерархии и общи понятия за индуктивни и индуктивно-рекурсивни дефиниции увеличиха доказателствената сила на теорията и също така я направиха по-удобна за програмиране и формализиране на математиката. Например, с добавянето на добре обосновани дървета можем да интерпретираме конструктивната теория за набор на Zermelo-Fraenkel (CZF) на Aczel (1978 [1977]). Ще изчакаме до следващия раздел, за да опишем тези разширения.

3.1 Решения

В Martin-Löf (1996) е представена обща философия на логиката, където традиционната представа за преценка се разширява и получава централно положение. Преценката вече не е само утвърждаване или отричане на предложение, а общ акт на знание. Когато математически разсъждаваме, правим преценки за математически обекти. Една форма на преценка е да се твърди, че някакво математическо твърдение е вярно. Друга форма на преценка е да се твърди, че нещо е математически обект, например набор. Логичните правила дават методи за създаване на правилни преценки от предишни преценки. Решенията, получени по такива правила, могат да бъдат представени под формата на дърво

) infer [r_4] {J_8} { infer [r_1] {J_3} {J_1 & J_2} & / infer [r_3] {J_7} { infer [r_5] {J_5} {J_4} & J_6}}]

или в последователна форма

• (1) (J_1 / quad / текст {аксиома})
• (2) (J_2 / quad / текст {аксиома})
• (3) (J_3 / quad / текст {по правило (r_1) от (1) и (2)})
• (4) (J_4 / quad / текст {аксиома})
• (5) (J_5 / quad / текст {по правило (r_2) от (4)})
• (6) (J_6 / quad / текст {аксиома})
• (7) (J_7 / quad / текст {по правило (r_3) от (5) и (6)})
• (8) (J_8 / quad / текст {по правило (r_4) от (3) и (7)})

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

Мотивите от първи ред могат да бъдат представени с помощта на един вид преценка:

твърдението (B) е вярно при хипотезата, че предложенията (A_1, / ldots, A_n) са верни.

Пишем тази хипотетична преценка като така наречената последователност на Гентцен

[A_1, / ldots, A_n { vdash} Б.)

Обърнете внимание, че това е единично решение, което не трябва да се бърка с извличането на решението ({ vdash} B) от решенията ({ vdash} A_1, / ldots, { vdash} A_n). Когато (n = 0), тогава категоричното решение ({ vdash} B) заявява, че (B) е вярно без никакви предположения. С последователна нотация става познатото правило за съвместно въвеждане

) infer [(земя I)] {A_1, / ldots, A_n { vdash} B / land C} {A_1, / ldots, A_n { vdash} B & A_1, / ldots, A_n { vdash} ° С}.)

3.2 Форми на съдебно решение

Теорията на типа Мартин-Льоф има четири основни форми на преценки и е значително по-сложна система от логиката от първи ред. Една от причините е, че в дериватите се носи повече информация поради идентифицирането на предложения и видове. Друга причина е, че синтаксисът е по-ангажиран. Например, добре оформените формули (типове) трябва да се генерират едновременно с доказано верните формули (обитавани типове).

Четирите форми на категорична преценка са

• (vdash A \; { rm type}), което означава, че (A) е добре оформен тип,
• (vdash a {:} A), което означава, че (a) има тип (A),
• (vdash A = A '), което означава, че (A) и (A') са равни типове,
• (vdash a = a '{:} A), което означава, че (a) и (a') са равни елементи от тип (A).

Като цяло преценката е хипотетична, тоест тя се прави в контекст (Gamma), тоест списък (x_1 {:} A_1, / ldots, x_n {:} A_n) на променливи, които може да възникне безплатно в преценката, заедно със съответните им видове. Обърнете внимание, че типовете в даден контекст могат да зависят от променливи от по-ранни типове. Например, (A_n) може да зависи от (x_1 {:} A_1, / ldots, x_ {n-1} {:} A_ {n-1}). Четирите форми на хипотетични преценки са

• (Gamma / vdash A \; { rm type}), което означава, че (A) е добре оформен тип в контекста (Gamma),
• (Gamma / vdash a {:} A), което означава, че (a) има тип (A) в контекст (Gamma),
• (Gamma / vdash A = A '), което означава, че (A) и (A') са равни типове в контекста (Gamma),
• (Gamma / vdash a = a '{:} A), което означава, че (a) и (a') са равни елементи от тип (A) в контекста (Gamma),

Под предложението като тълкуване на типове

) маркер {2} етикет {analytic} vdash a {:} A)

може да се разбира като преценката, че (a) е доказателствен обект за предложението (A). Когато потискаме този обект, получаваме преценка, съответстваща на тази в обикновената логика от първи ред (виж по-горе):

) маркер {3} етикет {синтетичен} vdash A \; { rm true}.)

Забележка 3.1. Мартин-Льоф (1994) твърди, че аналитичната преценка на Кант априори и синтетичната преценка априори могат да бъдат пример в областта на логиката съответно от ([аналитичен]) и ([синтетичен]). В аналитичната преценка ([аналитична]) всичко, което е необходимо, за да стане очевидното, е категорично. За неговата синтетична версия ([синтетична]) е необходимо да се предвиди евентуално сложна доказателна конструкция (a), за да стане очевидна. Това разбиране за аналитичност и синтетичност има изненадващото последствие, че „логическите закони в обичайната им формулировка са всички синтетични“. Мартин-Льоф (1994: 95). Неговият анализ допълнително дава:

„[…] Логиката на аналитичните преценки, тоест логиката за извличане на преценки на двете аналитични форми, е пълна и решаваща, докато логиката на синтетичните преценки е непълна и неразрешима, както показа Гьодел.“Мартин-Льоф (1994: 97).

Решимостта на двете аналитични преценки ((vdash a {:} A) и (vdash a = b {:} A)) зависи от метаматематическите свойства на теорията на типовете: силна нормализация и проверка на решителен тип.

Понякога следните форми изрично се считат за преценки на теорията:

• (Gamma \; { rm контекст}), което означава, че (Gamma) е добре оформен контекст.
• (Gamma = / Gamma '), което означава, че (Gamma) и (Gamma') са равни контексти.

По-долу ще съкратим преценката (Gamma / vdash A \; { rm type}) като (Gamma / vdash A) и (Gamma \; { rm контекст}) като (Гама / vdash.)

3.3 Правила за заключение

Когато заявяваме правилата, ще използваме буквата (Gamma) като мета променлива, варираща в контекста, (A, B, / ldots) като мета-променливи, вариращи в зависимост от типове, и (a, b, c, d, e, f, / ldots) като мета-променливи, вариращи в термини.

Първата група правила за изводи са общи правила, включително правила за предположение, заместване и формиране на контекста. Има и правила, които изразяват, че равенствата са отношения на еквивалентност. Има много такива правила и ние показваме само особено важното правило за равенство на типа, което е от решаващо значение за изчисляването на типовете:

) frac { Gamma / vdash a {:} A / hspace {2em} Gamma / vdash A = B} { Gamma / vdash a {:} B})

Останалите правила са специфични за създателите на типове. Те се класифицират като правила за формиране, въвеждане, премахване и равенство.

3.4 Интуиционистична предикатна логика

Ние даваме само правилата за (Pi). Съществуват аналогични правила за останалите типови формати, съответстващи на логическите константи на въведената предикатна логика.

В следното (B [x: = a]) означава терминът, получен чрез заместване на термина (a) за всяко свободно възникване на променливата (x) в (B) (избягване на улавяне на променлива), (Pi) - формация.) frac { Gamma / vdash A / hspace {2em} Gamma, x {:} A / vdash B} { Gamma / vdash / Pi x {:} A. B}) (Pi) -Въведение.) frac { Gamma, x {:} A / vdash b {:} B} { Gamma / vdash / lambda x. b {:} Pi x {:} A. B}) (Pi) - премахване.) frac { Gamma / vdash f {:} Pi x {:} AB / hspace {2em} Gamma / vdash a {:} A} { Gamma / vdash f \, a {:} B [x: = a]}) (Pi) - равенство.) frac { Gamma, x {:} A / vdash b {:} B / hspace {2em} Gamma / vdash a {:} A} { Gamma / vdash (lambda xb), a = b [x: = a] {:} B [x: = a]}) Това е правилото на (beta) - преобразуване. Можем също да добавим правилото на (eta) - преобразуване:) frac { Gamma / vdash f {:} Pi x {:} A. B} { Gamma / vdash / lambda x. f \, x = f {:} Pi x {:} A. B}.)

Освен това съществуват правила за конгруентност, които изричат, че операциите, въведени от правилата за формиране, въвеждане и премахване, запазват равенството. Например, правилото за конгруенция за (Pi) е

) frac { Gamma / vdash A = A '\ hspace {2em} Gamma, x {:} A / vdash B = B'} { Gamma / vdash / Pi x {:} A. B = / Pi x {:} A '. B '}.)

3.5 Естествени числа

Както в аритметиката на Peano, естествените числа се генерират от 0 и операцията на наследника (s). Правилото за премахване гласи, че това са единствените възможни начини за генериране на естествено число.

Пишем (f (c) = / R (c, d, xy.e)) за функцията, която се определя от примитивната рекурсия на естественото число (c) с базов случай (d) и стъпка функция (xy.e) (или алтернативно (lambda xy.e)), която преобразува стойността (y) за предишното число (x {:} N) към стойността за (S (х)). Обърнете внимание, че (R) е нов оператор, обвързващ променливите: променливите (x) и (y) стават свързани в (e).

(N) - формация.) Gamma / vdash / N) (N) - въведение.) Gamma / vdash 0 {:} N / hspace {2em} frac { Gamma / vdash a {:} N} { Gamma / vdash s (a) {:} N}) (N) - елиминиране.) frac { Gamma, x {:} N / vdash C / hspace {1em} Gamma / vdash c {:} N / hspace {1em} Gamma / vdash d {:} C [x: = 0] hspace {1em} Gamma, y {:} N, z {:} C [x: = y] vdash e {:} C [x: = s (y)]} { Gamma / vdash / R (c, d, yz.e) {:} C [x: = c]}) (N) - равенство (при подходящи помещения).) начало {подравняване *} R (0, d, yz.e) & = d {:} C [x: = 0] / \ R (s (a), d, yz.e) & = e [y: = a, z: = / R (a, d, yz.e)] {:} C [x: = s (a)] end {align *})

Правилото на (N) - елиминиране едновременно изразява типа функция, дефинирана от примитивната рекурсия и под интерпретацията на Curry-Howard правилото на математическата индукция: доказваме свойството (C) на естествено число (x) чрез индукция на (x).

Системата на Гьодел (T) е по същество интуиционистична теория на типовете само с формовете на типовете (N) и (A / правна B) (вида функции от (A) до (B), което е специалният случай на ((Pi x {:} A) B), където (B) не зависи от (x {:} A)). Тъй като няма никакви зависими типове в System (T), правилата могат да бъдат опростени.

3.6 Вселената на малките типове

Първата версия на теорията на типовете Мартин-Льоф (Martin-Löf 1971a) има аксиома, в която се посочва, че има тип от всички видове. Това се оказа непоследователно от Жирар, който откри, че парадоксът Бурали-Форти може да бъде кодиран в тази теория.

За да преодолее тази патологична непредсказуемост, но все пак запазва част от своята експресивност, Мартин-Льоф въвежда през 1972 г. вселена (U) от малки типове, затворена под всички типови форми на теорията, с изключение на това, че тя не съдържа себе си (Мартин- Löf 1998 [1972]). Правилата са:

(U) - формация.) Gamma / vdash / U) (U) - въведение.) Gamma / vdash / varnothing {:} U / hspace {3em} Gamma / vdash 1 {:} U)) frac { Gamma / vdash A {:} U / hspace {2em} Gamma / vdash B {:} U} { Gamma / vdash A + B {:} U} hspace {3em} frac { Gamma / vdash A {:} U / hspace {2em} Gamma / vdash B {:} U} { Gamma / vdash A / пъти B {:} U})) frac { Gamma / vdash A {:} U / hspace {2em} Gamma / vdash B {:} U} { Gamma / vdash A / rightarrow B {:} U})) frac { Gamma / vdash A {:} U / hspace {2em} Gamma, x {:} A / vdash B {:} U} { Gamma / vdash / Sigma x {:} A. \, B {:} U} hspace {3em} frac { Gamma / vdash A {:} U / hspace {2em} Gamma, x {:} A / vdash B {:} U} { Gamma / vdash / Pi x {:} A. \, B {:} U})) Gamma / vdash / N {:} U) (U) - премахване.) frac { Gamma / vdash A {:} U} { Gamma / vdash A})

Тъй като (U) е тип, можем да използваме (N) - премахване, за да определим малки типове чрез примитивна рекурсия. Например, ако (A: / U), можем да определим вида на (n) - кортежи на елементи в (A), както следва:

[A ^ n = / R (n, 1, xy. A / пъти y) {:} U)

Тази теоретична вселена тип (U) е аналог на Вселената на Гротендик в теорията на множествата, която е набор от затворени множества по всички начини, на които множествата могат да бъдат конструирани в теорията на множествата на Цермер-Френкел. Съществуването на вселената на Гротендик не може да бъде доказано от обичайните аксиоми на теорията на множествата на Цермер-Френкел, но се нуждае от нова аксиома.

В Мартин-Льоф (1975 г.) Вселената е разширена до преброена йерархия на вселените

) U_0: / U_1: / U_2: / cdots.)

По този начин всеки тип има тип, не само всеки малък тип.

3.7 Предлагаща идентичност

По-горе въведохме преценката за равенството

) етикет {4} етикет {defeq} Gamma / vdash a = a '{:} A.)

Това обикновено се нарича „определено равенство“, защото може да се реши чрез нормализиране на термините (a) и (a ') и проверка дали нормалните форми са идентични. Това равенство обаче е преценка, а не предложение (тип) и по този начин не можем да докажем такива равенства на осъждането чрез индукция. Поради тази причина трябва да въведем предложения за типове идентичност. Например, типът идентичност за естествени числа (I (N, m, n)) може да бъде определен чрез (U) - примитивна рекурсия с стойност \. Тогава можем да изразим и докажем аксиомите на Пеано. Освен това, равенството на разширяването на разширенията може да бъде определено от

) I (N / rightarrow / N, f, f ') = / Pi x {:} N. / I (N, F \, X, е '\, х).)

3.8 Аксиомата на избора е теорема

Следващата форма на аксиома на избор е непосредствено следствие от BHK-интерпретацията на интуиционистичните количествени характеристики и лесно се доказва в теорията на интуиционистичния тип:

[(Pi x {:} A. / Sigma y {:} B. C) rightarrow / Sigma f {:} (Pi x {:} A. B). C [y: = f \, x])

Причината е, че (Pi x {:} A. / Sigma y {:} B. C) е типът функции, които картографират елементи (x {:} A) към двойки ((y, z)) с (y {:} B) и (z {:} C). Функцията за избор (f) се получава чрез връщане на първия компонент (y {:} B) на тази двойка.

Може би е изненадващо, че теорията на интуиционистичния тип директно потвърждава аксиома на избор, тъй като тази аксиома често се смята за проблемна от конструктивна гледна точка. Възможно обяснение на това състояние на нещата е, че горното е аксиома за избор на типове и че типовете не са като цяло подходящи конструктивни приближения на множествата в класическия смисъл. Например, можем да представим реално число като последователност на Коши в теорията на интуиционистичния тип, но наборът от реални числа не е типът на последователностите на Коши, а типът на последователностите на Коши до еквиконвергенция. По-общо, набор в конструктивната математика на Бишоп е представен от тип (обикновено наричан „предварително зададен“), заедно със съотношение на еквивалентност.

Ако (A) и (B) са оборудвани с отношения на еквивалентност, разбира се, няма гаранция, че функцията за избор (f) по-горе е разширена в смисъл, че тя преобразува еквивалентен елемент в еквивалентни елементи. Това е неуспехът на аксиомата за разширение на избора, виж за анализ Martin-Löf (2009).

4. Разширения

4.1 Логическата рамка

Горното завършва описанието на основна версия на теорията на интуиционистичния тип, близка до тази на (Martin-Löf 1998 [1972]).

През 1986 г. Мартин-Льоф предлага преформулиране на теорията на интуиционистичния тип; вижте Nordström, Peterson и Smith (1990) за експозиция. Целта беше да се даде по-компактна формулировка, където (lambda) и (Pi) са единствените операции за свързване на променливи. В днешно време се счита за основна версия на теорията. Той също е основа за асистента за доказателство на Agda. Теорията от 1986 г. има две части:

• теорията на видовете (логическата рамка);
• теорията на множествата (малки типове).

Забележка 4.1. Обърнете внимание, че думата „набор“в логическата рамка не съвпада с начина, по който се използва в конструктивната математика на Бишоп. За да се избегне това объркване, типовете заедно с отношенията на еквивалентност обикновено се наричат „сетоиди“или „екстензионални множества“в интуиционистичната теория на типа.

Логическата рамка има само два форматора на формат: (Pi x {:} A. B) (обикновено се пише ((x {:} A) B) или ((x {:} A) rightarrow B) във формулировката на логическата рамка) и (U) (обикновено наричани (Set)). Правилата за (Pi x {:} A. B) (((x {:} A) rightarrow B)) са същите като дадените по-горе (включително (eta) - преобразуване). Правилата за (U) ((Set)) също са едни и същи, само че логическата рамка предвижда затваряне само при формиране на тип (Pi).

Другите малки форматори (“set formers”) са въведени в теорията на множествата. При формулирането на логическата рамка всяко правило за образуване, въвеждане и премахване може да бъде изразено като въвеждане на нова константа. Например стават правилата за естествените числа

) започнете {подравняване *} N &: / Задайте, \\ 0 &: / N, \\ / s &: / N / rightarrow / N, \\ / R &: (C {:} N / rightarrow / Set) rightarrow C \, 0 / rightarrow ((x {:} N) rightarrow C \, x / rightarrow C \, (s \, x)) rightarrow (c {:} N) rightarrow C \, c. / Край {подравняване *})

където сме пропуснали общия контекст (Gamma), тъй като видовете на тези константи са затворени. Обърнете внимание, че рекурсивният оператор (R) има първи аргумент (C {:} N / rightarrow / Set) за разлика от оригиналната формулировка.

Освен това правилата за равенство могат да бъдат изразени като уравнения

) начало {подравняване *} R \, C \, d \, e \, 0 & = d {:} C \, 0 \\ / R \, C \, d \, e \, (s \, a) & = e \, a \, (R \, C \, d \, e \, a) {:} C \, (s \, a) end {align *})

при подходящи предположения.

В продължението ще представим няколко разширения на теорията на типа. За да запазим представянето равномерно, обаче няма да използваме логическото рамково представяне на теорията на типовете, но ще използваме същите обозначения като в раздел 2.

4.2 Общ тип идентичност

Както споменахме по-горе, идентичността на естествените числа може да бъде определена чрез примитивна рекурсия. Отношенията на идентичността на други видове също могат да бъдат определени в основната версия на теорията на интуиционистичния тип, представена в раздел 2.

Въпреки това, Мартин-Льоф (1975 г.) разшири теорията за интуиционистичния тип с еднакъв примитивен тип бивша идентичност бивш (I) за всички видове. Правилата за (I) изразяват, че връзката на идентичност се генерира индуктивно от доказателството за рефлексивност, канонична константа, наречена (r). (Обърнете внимание, че (r) е кодирано от числото 0 във въвеждащото представяне на обекти с доказателство в 2.3. Правилото за елиминиране за типа идентичност е обобщение на елиминирането на идентичност в логиката на предиката и въвежда константа на елиминиране (Тук показваме формулировката поради Paulin-Mohring (1993), а не оригиналната формулировка на Martin-Löf (1975). Правилата на извода са следните.

(I) - формация.) frac { Gamma / vdash A / hspace {1em} Gamma / vdash a {:} A / hspace {1em} Gamma / vdash a '{:} A} { Gamma / vdash / I (A, а, а ')})

(Въведение.) frac { Gamma / vdash A / hspace {1em} Gamma / vdash a {:} A} { Gamma / vdash / r {:} I (A, a, a)})

(I) - елиминиране.

) frac { Gamma, x {:} A, y {:} I (A, a, x) vdash C / hspace {1em} Gamma / vdash b {:} A / hspace {1em} Gamma / vdash c {:} I (A, a, b) hspace {1em} Gamma / vdash d {:} C [x: = a, y: = r]} { Gamma / vdash / J (c, d) {:} C [x: = b, y: = c]})

(I) - равенство (при подходящи предположения).

) начало {подравняване *} J (r, d) & = d / край {подравняване *})

Обърнете внимание, че ако (C) зависи само от (x: A), а не от доказателството (y: / I (A, a, x)) (и също така потискаме доказателствените обекти) в правилото на (I) - елиминиране възстановяваме правилото за премахване на идентичност в предикатната логика.

Чрез изграждането на модел на теорията на типовете, при който типовете се интерпретират като групови (категории, при които всички стрели са изоморфизми) Хофман и Стрейхер (1998) показаха, че не може да се докаже в интуиционистичната теория на типовете, че всички доказателства на (I (A, a, b))) са идентични. Това може да изглежда като непълнота на теорията и Стрейхер предложи нова аксиома (K), от която следва, че всички доказателства за (I (A, a, b)) са идентични на (r).

Типът (I) често се нарича тип интензивна идентичност, тъй като не удовлетворява принципа на разширяването на функциите. Интуиционистичната теория на типа с интензионен тип идентичност също често се нарича интензивна теория на интуиционистичния тип, за да се разграничи от разширената интуиционистка теория на типа, която ще бъде представена в раздел 7.1.

4.3 Добре установени дървета

Тип добре обосновани дървета от формата (W x {:} A. B) е въведен през Martin-Löf 1982 (и в по-ограничен вид от Скот 1970). Елементите на (W x {:} A. B) са дървета с различно и произволно разклонение: вариращи, тъй като типът на разклоняване (B) се индексира с (x {:} A) и произволен, защото (B) може да бъде произволен. Типът се дава чрез обобщена индуктивна дефиниция, тъй като добре обоснованите дървета могат да бъдат безкрайно разклонени. Можем да мислим за (W x {:} A. B) като алгебра на свободния термин, където всеки (a {:} A) представлява терминов конструктор (sup \, a) с (вероятно безкрайна) arity (B [x: = a]).

(W) - формация.) frac { Gamma / vdash A / hspace {2em} Gamma, x {:} A / vdash B} { Gamma / vdash / W x {:} A. B}) (W) -Въведение.) frac { Gamma / vdash a {:} A / hspace {2em} Gamma, y {:} B [x: = a] vdash b: Wx {:} A. B} { Gamma / vdash / sup (a, yb): / W x {:} A. B})

Пропускаме правилата на (W) - премахване и (W) - равенство.

Добавянето на добре обосновани дървета към теорията на интуиционистичния тип увеличава значително неговата доказателствено-теоретична сила (Setzer (1998)).

4.4 Итеративни комплекти и CZF

Важно приложение на добре обосновани дървета е конструкцията на Aczel (1978) на типово-теоретичен модел на конструктивната теория за набор на Zermelo Fraenkel. За тази цел той определя вида на итеративните набори като

) V = / W x {:} U. х.)

Нека (A {:} U) е малък тип, а (x {:} A / vdash M) е индексирано семейство от итеративни набори. Тогава (sup (A, xM)), или с по-внушаваща нотация ({M / mid x {:} A }), е итеративен набор. Ако перифразирам: итеративният набор е семейство итеративни множества, индексирани от малък тип.

Обърнете внимание, че итеративният набор е alt = "sep man icon" /> Как да цитирам този запис.

Вижте PDF версията на този запис в Дружеството на приятелите на SEP.

Разгледайте тази тема за вписване в интернет философския онтологичен проект (InPhO).

Подобрена библиография за този запис в PhilPapers, с връзки към неговата база данни.

Други интернет ресурси

• Интернет енциклопедия на философията: конструктивна математика
• Scholarpedia: Теория на изчислителния тип
• nLab: Теория на типа