Кіріспе
Математиканың баламалы негізі Интуициялық типтік теория (сонымен қатар конструктивті типтік теория немесе Мартин Лёфтың типтік теориясы деп те аталады, соңғысы MLTT деп қысқартылады) – типтік теория және математиканың баламалы негізі. Интуициялық типтік теорияны швед математигі және философы Пер Мартин Лёф 1972 жылы жариялаған. Типтік теорияның бірнеше нұсқасы бар: Мартин Лёф теорияның интенционалды және экстенсионалды түрлерін ұсынды, ал Жирардтың парадоксына байланысты сәйкессіздігі дәлелденген ертедегі импредикативтік түрлері предикативтік түрлеріне жол берді. Дегенмен, барлық нұсқалар тәуелді типтерді қолдана отырып, конструктивті логиканың негізгі қағидаларын сақтайды.
Intuitionistic type theory (also known as constructive type theory, or Martin Löf type theory, the latter abbreviated as MLTT) is a type theory and an alternative foundation of mathematics. Intuitionistic type theory was created by Per Martin Löf, a Swedish mathematician and philosopher, who first published it in 1972. There are multiple versions of the type theory: Martin Löf proposed both intensional and extensional variants of the theory and early impredicative versions, shown to be inconsistent by Girard's paradox, gave way to predicative versions. However, all versions keep the core design of constructive logic using dependent types.
Дизайн
Мартин Лёф типтік теорияны математикалық конструктивизм принциптеріне негіздеп жасады. Конструктивизм кез келген барлық нәрсе дәлелінің "куәгерді" қамтуын талап етеді. Демек, "1000-нан үлкен жай сан бар" деген кез келген дәлел 1000-нан үлкен және жай сан болатын нақты санды көрсетуі керек. Интуициялық типтік теория бұл жобалық мақсатына BHK интерпретациясын ішкі түсіндіру арқылы қол жеткізді. Қызықтысы, дәлелдер математикалық объектілерге айналады, оларды қарастыруға, салыстыруға және манипуляциялауға болады. Интуициялық типтік теорияның типтік конструкторлары логикалық байланыстармен бір-бірге сәйкестік принципін сақтау үшін құрылды. Мысалы, импликация деп аталатын логикалық байланыс функцияның типіне сәйкес келеді. Бұл сәйкестік Карри-Говард изоморфизмі деп аталады. Бұрынғы типтік теориялар да осы изоморфизмді ұстанған, бірақ Мартин Лёфтың теориясы тәуелді типтерді енгізу арқылы оны алғаш рет предикаттық логикаға дейін кеңейтті.
Тип теориясы
Интуициялық типтік теорияда үш шекті тип бар, олар бес түрлі типтік конструкторларды қолдана отырып құрастырылады. Жинақтар теориясынан айырмашылығы, типтік теория Фреге сияқты логикаға негізделмеген. Сондықтан, типтік теорияның әрбір мүмкіндігі математика мен логиканың ерекшелігі ретінде қызмет етеді. Егер сіз типтік теориямен таныс емес болсаңыз, бірақ жинақтар теориясын білсеңіз, мынадай қысқаша түсінік беріледі: Типтер жинақтар сияқты терминдерді қамтиды, жинақтар элементтерді қамтиды. Терминдер бір ғана типке жатады. Мысалы, және басқа терминдер 4 сияқты канондық түрлерге дейін есептеледі ("қайтадан жайластырылады"). Толығырақ ақпарат алу үшін типтік теория туралы мақаланы қараңыз.
0 түрі, 1 түрі және 2 түрі
Үш шекті тип бар: 0 типі 0 терминді қамтиды. 1 типі 1 каноникалық терминді қамтиды. Ал 2-ші типте 2 каноникалық термин бар. 0 типі 0 терминді қамтитындықтан, ол бос тип деп те аталады. Ол болуы мүмкін емес нәрсені көрсетеді. Сондай-ақ, ол дәлелдеуге келмейтін нәрсені білдіреді. (Яғни, оның дәлелі болуы мүмкін емес.) Осының салдарынан, жоққа шығару оған функция ретінде анықталады: Сол сияқты, 1 типі 1 каноникалық терминді қамтиды және ол болуды көрсетеді. Оны бірлік типі деп те атайды. Ол көбінесе дәлелденетін мәлімдемелерді көрсетеді, сондықтан кейде жазылады. Соңында, 2 типі 2 каноникалық терминді қамтиды. Бұл екі мәннің арасындағы нақты таңдауды білдіреді. Ол бульдік мәндер үшін қолданылады, бірақ мәлімдемелер үшін емес. Мәлімдемелердің орнына, нақты типтермен бейнеленеді. Мысалы, дұрыс мәлімдеме 1 типімен, ал жалған мәлімдеме 0 типімен көрсетілуі мүмкін. Бірақ бұл мәлімдемелердің жалғыз түрлері деп айта алмаймыз, яғни, интуиционистік типтер теориясындағы ортасы жоқ заңы мәлімдемелерге қатысты қолданылмайды.
Likewise, the 1 type contains 1 canonical term and represents existence. It also is called the unit type. It often represents propositions that can be proven and is, therefore, sometimes written
Finally, the 2 type contains 2 canonical terms. It represents a definite choice between two values. It is used for Boolean values but not propositions. Propositions are instead represented by particular types. For instance, a true proposition can be represented by the 1 type, while a false proposition can be represented by the 0 type. But we cannot assert that these are the only propositions, i. e. the law of excluded middle does not hold for propositions in intuitionistic type theory.
Σ типті конструктор
Σ типтерінде реттелген жұптар болады. Типтік реттелген жұп (немесе 2-топтама) түрінде, Σ түрі басқа екі түрдің Картезиан көбейтіндісін сипаттай алады, және логикалық тұрғыдан, мұндай реттелген жұп дәлелдемесін және дәлелдемесін ұстайтын болады, сондықтан мұндай типті Σ түрі ретінде жазылған түрде көруге болады. Тәуелді типтеудің арқасында Σ типтері типтік реттелген жұп түрлерінен күштірек. Реттелген жұпта екінші мүшенің түрі бірінші мүшенің мәніне байланысты болуы мүмкін. Мысалы, жұптың бірінші мүшесі натурал сан болуы мүмкін, ал екінші мүшенің түрі бірінші мүшесіне тең ұзындықтағы нақты сандар тізбегі болуы мүмкін. Мұндай тип былай жазылады:
Σ types are more powerful than typical ordered pair types because of dependent typing. In the ordered pair, the type of the second term can depend on the value of the first term. For example, the first term of the pair might be a natural number and the second term's type might be a sequence of reals of length equal to the first term. Such a type would be written:
Жинақтар теориясы терминологиясын қолданғанда, бұл жинақтардың индекстелген ажыратылған біріктірілісіне ұқсас. Әдеттегі реттелген жұптарда екінші мүшенің түрі бірінші мүшенің мәніне байланысты емес. Сондықтан картезиан көбейтіндісін сипаттайтын тип былай жазылады:
Мұнда бірінші мүшенің мәні , екінші мүшенің түріне тәуелді емес екенін атап өту маңызды. Σ типтерін математикада қолданылатын және көптеген бағдарламалау тілдеріндегі жазбалар немесе құрылымдар құру үшін пайдалануға болады. Тәуелді типтегі 3-топтаманың мысалы – екі бүтін сан және бірінші бүтін санның екіншісінен кіші екендігінің дәлелі, ол мынадай типпен сипатталады:
Σ types can be used to build up longer dependently typed tuples used in mathematics and the records or structs used in most programming languages. An example of a dependently typed 3 tuple is two integers and a proof that the first integer is smaller than the second integer, described by the type:
Тәуелді типтеу Σ типтеріне экзистенциалдық квантор рөлін атқаруға мүмкіндік береді. « түріндегі бар, сонда дәлелденеді» деген мәлімдеме реттелген жұптардың түріне айналады, онда бірінші элемент – түріндегі мәні, ал екінші элемент – дәлелдемесі. Есімізде болсын, екінші элементтің түрі (дәлелдемелер) реттелген жұптың бірінші бөлігіндегі мәнге байланысты. Оның түрі былай болады:
= типтік құрастырғыш
= типтері екі терминнен жасалады. Егер екі термин берілген болса, мысалы, және , жаңа типін жасауға болады. Осы жаңа типтің терминдері осы жұптың бірдей каноникалық терминге келуін көрсетеді. Осылайша, егер екеуі де және каноникалық терминге есептелсе , онда типінде термин болады. Интуиционистік типтер теориясында = типтерін енгізудің жалғыз жолы – рефлексивтілік:
Мүмкін, мысалы, сияқты = типтерін жасауға болады, онда терминдер бірдей каноникалық терминге дейін келе бермейді, бірақ сіз осы жаңа типтегі терминдерді жасай алмайсыз. Шындығында, егер сіз терминін жасасаңыз, онда терминін де жасай аласыз. Оны функцияға қоссаңыз, типіндегі функция пайда болады. Интуиционистік типтер теориясы терісті осылай анықтайды, сондықтан сіз немесе, соңында, болады. Дәлелдемелердің теңдігі – дәлелдеме теориясындағы белсенді зерттеу саласы және гомотопиялық типтер теориясы және басқа типтер теорияларының дамуына әкелді.
Equality of proofs is an area of active research in proof theory and has led to the development of homotopy type theory and other type theories.
Индуктивті типтер
Индуктивті типтер күрделі, өзіне сілтеме жасайтын типтерді құруға мүмкіндік береді. Мысалы, табиғи сандардың тізбегі бос тізбек немесе табиғи сан мен басқа тізбектің жұбынан тұрады. Индуктивті типтер ағаштар, графтар сияқты шексіз математикалық құрылымдарды анықтау үшін қолданылуы мүмкін. Шындығында, табиғи сандар типін де индуктивті тип ретінде анықтауға болады, ол өзінің ізі немесе басқа табиғи санның ізі болуы мүмкін. Индуктивті типтер нөл және ізін табу функциясы сияқты жаңа тұрақтыларды анықтайды. Оның анықтамасы болмайтындықтан және алмастыру арқылы есептелмейтіндіктен, және сияқты шарттар табиғи сандардың канондық шарттарына айналады. Индуктивті типтердегі дәлелдемелер индукция арқылы жүзеге асырылады. Әрбір жаңа индуктивті типтің өзіне тән индукциялық ережесі болады. Барлық табиғи сан үшін предикатты дәлелдеу үшін келесі ережені қолданасыз:
and become the canonical terms of the natural numbers. Proofs on inductive types are made possible by induction. Each new inductive type comes with its own inductive rule. To prove a predicate for every natural number, you use the following rule:
Интуиционистік типтер теориясындағы индуктивті типтер W типтері, яғни жақсы негізделген ағаштар типінің негізінде анықталады. Типтер теориясы бойынша кейінгі жұмыстар коиндуктивті типтерді, индукциялық рекурсияны және өзін-өзі анықтамалық түрлерінің күрделірек түрлерімен жұмыс істеу үшін индукциялық индукцияны жасады. Жоғары индуктивті типтер шарттар арасындағы теңдікті анықтауға мүмкіндік береді.
Ғалам түрлері
Ғалам типтері басқа типтік конструкторлармен жасалған барлық типтер туралы дәлелдер жазуға мүмкіндік береді. Ғалам типіндегі әрбір термин, кез келген комбинацияда және индуктивті типтік конструктормен жасалған типке бейімделуі мүмкін. Дегенмен, парадокс болдырмау үшін, ғалам типінде кез келген үшін бейімделетін термин жоқ.
To write proofs about all "the small types" and , you must use , which does contain a term for , but not for itself Similarly, for There is a predicative hierarchy of universes, so to quantify a proof over any fixed constant universes, you can use
Universe types are a tricky feature of type theories. Martin Löf's original type theory had to be changed to account for Girard's paradox. Later research covered topics such as "super universes", "Mahlo universes", and impredicative universes.
Барлық "кішкентай типтер" және туралы дәлелдер жазу үшін, сізді қамтитын ғаламды пайдалану қажет, ол үшін термин бар, бірақ өзі үшін емес. Сол сияқты, үшін де. Ғаламдардың предикативтік иерархиясы бар, сондықтан кез келген белгілі тұрақты ғаламдар бойынша дәлелді сандық өлшемдеу үшін сізді пайдалана аласыз.
To write proofs about all "the small types" and , you must use , which does contain a term for , but not for itself Similarly, for There is a predicative hierarchy of universes, so to quantify a proof over any fixed constant universes, you can use
Universe types are a tricky feature of type theories. Martin Löf's original type theory had to be changed to account for Girard's paradox. Later research covered topics such as "super universes", "Mahlo universes", and impredicative universes.
Ғалам типтері – типтік теориялардың қиын ерекшелігі. Мартин Лёфтың бастапқы типтік теориясы Жирардтың парадоксын ескеру үшін өзгертілуі керек болды. Кейінгі зерттеулер "супер ғаламдар", "Мало ғаламдары" және импредикативті ғаламдар сияқты тақырыптарды қамтыды.
To write proofs about all "the small types" and , you must use , which does contain a term for , but not for itself Similarly, for There is a predicative hierarchy of universes, so to quantify a proof over any fixed constant universes, you can use
Universe types are a tricky feature of type theories. Martin Löf's original type theory had to be changed to account for Girard's paradox. Later research covered topics such as "super universes", "Mahlo universes", and impredicative universes.
Экстенсионды және интенсионды
Негізгі айырмашылық – экстенсионалдық және интенсионалдық типтер теориясы. Экстенсионалдық типтер теориясында анықтамалық (яғни, есептеулік) теңдік, дәлелдеуді қажет ететін ұйғарымдық теңдіктен ажыратылмайды. Соның салдарынан, экстенсионалдық типтер теориясында типті тексеру шешілмейтін болады, себебі теориядағы бағдарламалар тоқтамауы мүмкін. Мысалы, мұндай теория Y комбинаторына тип беруге мүмкіндік береді; мұның толық мысалын Nordström және Petersson еңбегіндегі «Programming in Martin Löf's Type Theory» кітабынан табуға болады. Дегенмен, бұл экстенсионалдық типтер теориясының практикалық құралдың негізі болуына кедергі келтірмейді; мысалы, Nuprl экстенсионалдық типтер теориясына негізделген. Керісінше, интенсионалдық типтер теориясында типті тексеру шешіледі, бірақ стандартты математикалық ұғымдарды бейнелеу біршама қиын, себебі интенсионалдық ойлау сетоидтар немесе осыған ұқсас құрылымдарды пайдалануды талап етеді. Бұл құрылымдарсыз жұмыс істеу қиын немесе бейнелеу мүмкін емес көптеген математикалық объектілер бар, мысалы, бүтін сандар, рационалдық сандар және нақты сандар. Бүтін және рационалдық сандарды сетоидтарсыз бейнелеуге болады, бірақ мұндай бейнелеумен жұмыс істеу қиын. Коши нақты сандарын осылай бейнелеуге болмайды. Гомотопиялық типтер теориясы осы мәселені шешуге бағытталған. Ол жоғары индуктивті типтерді анықтауға мүмкіндік береді, олар тек бірінші реттік конструкторларды (мәндерді немесе нүктелерді) ғана емес, сонымен қатар жоғары реттік конструкторларды, яғни элементтер арасындағы теңдіктерді (жолдарды), теңдіктер арасындағы теңдіктерді (гомотопияларды) және т.б. шексіз анықтауға мүмкіндік береді.
Тип теориясын іске асыру
Түр теориясының әр түрлі нысандары көптеген дәлелдеуге көмектесетін жүйелердің негізіндегі ресми жүйелер ретінде іске асырылды. Көптеген түрлері Пер Мартин Лёфтің идеяларына негіделгенімен, олардың көпшілігі қосымша мүмкіндіктерге, көбірек аксиомаларға немесе өзгеше философиялық негізге ие. Мысалы, Nuprl жүйесі есептеулік түр теориясына негізделген, ал Coq – (қосымша) индуктивті құрылымдардың есебіне негізделген. Тәуелді типтер ATS, Cayenne, Epigram, Agda және Idris сияқты бағдарламалау тілдерінің дизайнында да қолданылады.
Мартин-Лёф типтік теориясы
Пер Мартин Лёф әр түрлі уақытта жарияланған бірнеше типтік теорияларды құрастырды, олардың кейбіреулері олардың сипаттамалары бар препринттер мамандарға қол жетімді болғаннан кейін (соның ішінде Жан Ив Жирар және Джованни Самбин). Төмендегі тізімде басылып шыққан барлық теориялар тізімі және оларды бір-бірінен ерекшелейтін негізгі ерекшеліктер келтірілген. Бұл теориялардың барлығында тәуелді өнімдер, тәуелді сомалар, ажыратылған одақтар, шекті типтер және табиғи сандар болды. Барлық теорияларда тәуелді өнімдер немесе тәуелді сомалар үшін η-қайтаруды қамтымайтын бірдей қайтару ережелері болды, MLTT79-дан басқа, онда тәуелді өнімдер үшін η-қайтару қосылған. MLTT71 Пер Мартин Лёф жасаған алғашқы типтік теория болды. Ол 1971 жылы препринт түрінде жарық көрді. Онда бір ғалам болды, бірақ бұл ғаламның өзінде аты болды, яғни ол қазіргі терминологиямен айтқанда, «типте тип» типтік теориясы еді. Жан Ив Жирар бұл жүйенің дұрыс еместігін көрсетті және препринт жарияланбады. MLTT72 1972 жылғы препринтте ұсынылды, ол кейін жарияланды. Бұл теорияда бір ғалам V және сәйкестік типтері (= типтер) болған жоқ. Ғалам «предикативті» болды, яғни V-ге жатпайтын нысанға (мысалы, V-нің өзіне) байланысты V-ден алынған отбасының тәуелді өнімі V-ге жатады деп есептелмеді. Ғалам Расселдің Principia Mathematica-сы сияқты болды, яғни «T∈V» және «t∈T» (Мартин Лёф қазіргі заманғы «:» символын орнына «∈» символын қолданады) тікелей жазылатын, «El» сияқты қосымша конструкторларсыз. MLTT73 Пер Мартин Лёф жариялаған типтік теорияның алғашқы анықтамасы болды (ол 1973 жылғы Логикалық коллоквиумда ұсынылды және 1975 жылы жарияланды). Онда «ұсыныстар» деп сипатталатын сәйкестік типтері бар, бірақ ұғымдар мен қалған типтер арасында нақты айырмашылық енгізілмегендіктен, оның мағынасы белгісіз. Кейіннен J-элиминатор деп аталатын нәрсе бар, бірақ әлі атаусыз (94-95 беттерді қараңыз). Бұл теорияда V0, ..., Vn ғаламдарының шексіз тізбегі бар. Ғаламдар предикативті, Рассел сияқты және жинақталмайды. Шын мәнінде, 115-беттегі 3.10-қорытындысында егер A∈Vm және B∈Vn және A мен B өзара айналысатын болса, онда m=n делінеді. Бұл, мысалы, осы теорияда бірлік аксиомасын қалыптастыру қиын болатынын білдіреді – Vi-дің әрқайсысында жиырылатын типтер бар, бірақ оларды i ≠ j үшін Vi және Vj-ді байланыстыратын сәйкестік типтері болмағандықтан, тең деп жариялау қалай болатыны белгісіз. MLTT79 1979 жылы ұсынылды және 1982 жылы жарияланды. Бұл мақалада Мартин Лёф тәуелді типтік теория үшін төрт негізгі үкім түрін енгізді, ол осы жүйелердің метатеориясын зерттеуде маңызды рөл атқарады. Ол сонымен қатар контексттерді жеке ұғым ретінде енгізді (161-бетті қараңыз). J-элиминаторымен сәйкестік типтері бар (ол MLTT73-те пайда болған, бірақ онда бұл атау болмаған), сонымен қатар теорияны «экстенсионалды» ететін ережемен (169-бет). W типтері бар. Жинақталатын предикативті ғаламдардың шексіз тізбегі бар. Bibliopolis: 1984 жылғы Bibliopolis кітабында типтік теория туралы талқылау бар, бірақ ол біршама ашық және нақты таңдаулар жиынтығын көрсетпейді, сондықтан оған байланысты нақты типтік теория жоқ.
MLTT79 was presented in 1979 and published in 1982. In this paper, Martin Löf introduced the four basic types of judgement for the dependent type theory that has since become fundamental in the study of the meta theory of such systems. He also introduced contexts as a separate concept in it (see p. 161). There are identity types with the J eliminator (which already appeared in MLTT73 but did not have this name there) but also with the rule that makes the theory "extensional" (p. 169). There are W types. There is an infinite sequence of predicative universes that are cumulative. Bibliopolis: there is a discussion of a type theory in the Bibliopolis book from 1984, but it is somewhat open ended and does not seem to represent a particular set of choices and so there is no specific type theory associated with it.