Tüübiteooria

Tüübiteooria on mõne üksiku tüübisüsteemi formaalne esitus ja tüübisüsteemide uurimise valdkond matemaatikas ja informaatikas.

Mõned tüübiteooriad pakuvad hulgateooria kõrval alternatiivset alust matemaatikale. Kaks tüübiteooriat, mida on pakutud matemaatika alusteooriateks on Alonzo Churchi tüübitud lambda-arvutus ning Per Martin-Löfi intuitsionistlik tüübiteooria. Enamik arvutipõhiseid tõestusassistente on rajatud mõnele tüübiteooriale.

Ajalugu

Tüübiteooria loodi 20. sajandi alguses, et vältida paradoksi matemaatilises tehtes, mis põhines naiivsel hulgateoorial ja formaalloogikal. Russelli paradoks (nimetatud Bertrand Russelli järgi) tulenes sellest, et hulk võis olla defineeritud "kõigist võimalikest hulkadest", sealhulgas iseendast. Aastail 1902–1908 pakkus Russell välja erinevaid "teooriaid tüüpidest", et probleem lahendada.

1908. aastaks oli Russell kirja pannud oma täiustatud "tüüpide teooria", mis ilmus ka Whiteheadi ja Russelli kolmeosalises teoses Principia Mathematica. Süsteem vältis neid teoreetilisi vastuolusid, kuna lõi tüüpide hierarhia ja määras igale konkreetsele matemaatilisele entiteedile spetsiifilise tüübi.

Antud tüüpi entiteete sai luua ainult selle tüübi alamtüüpidest, mis vältis entiteedi defineerimist entiteedi enda põhjal. Russelli tüüpide teooria tegi seega võimatuks hulga defineerimist hulga enda põhjal. Tüüpe ei kasutatud igal pool loogikas ning Russelli paradoksi suudeti vältida ka teiste moodustega. Tüüpide kasutamine oli populaarne seoses ühe konkreetse loogikaga, nimelt Alonzo Churchi lambda-arvutusega.

Üks märkimisväärne varajane näide tüübiteooriast oli Churchi lihtsalt tüübitud lambda-arvutus. Churchi tüübiteooria aitas sellel arvutussüsteemil vältida Kleene-Rosseri paradoksi, mis vaevas originaalset tüüpimata lambda-arvutust. Lihtsalt tüübitud lambda-arvutust loeti kõrgema järgu loogikaks.

Väljend "tüübiteooria" tähendab tänapäeval tüübitud süsteemi, mis on konstrueeritud lambda-arvutuse ümber. Üks märkimisväärne süsteem on Per Martin-Löfi intuitsionistlik tüübiteooria, mis pakuti välja kui alusteooria konstruktiivse matemaatika jaoks. Veel üks tüübiteooria on Thierry Coquandi konstruktsioonide arvutus, mille põhjal loodi Coq, Lean ja mitmed teised tõestusassistendid.

Tutvustus

Põhimõtted

Termid ja tüübid

Tüübiteoorias on term funktsioon või objekt ning iga term seostatakse tüübiga. Term ja selle tüüp kirjutatakse kui "term : tüüp". Üks näide tüübist, mida tüübiteooriad sageli sisaldavad, on naturaalarvud (mida sageli märgitakse kui "$\mathbb {N}$" või "nat"), või tõeväärtused (Boole'i väärtused "bool", tavaliselt väärtustega tõene ja väär, ingl. true ja false). Mõned näited lihtsatest termidest on:

• 1 : nat
• 42 : nat
• true : bool

Terme saab konstrueerida teistest termidest rakendades funktsioone. Tüübiteoorias kutsutakse seda "funktsiooni aplikatsiooniks". Funktsiooni aplikatsioon võtab antud tüüpi termi ning annab tulemuseks mõnda teist tüüpi termi. Funktsioone võib kirjutada kui "funktsioon argument argument ...", erinevalt programmeerimises levinud vormist "funktsioon(argument, argument, argument ...)". Naturaalarvude puhul on võimalik defineerida funktsioon nimega "liida", mis võtab kaks naturaalarvu. Mõned termid nende tüüpidega on:

• liida 0 0 : nat
• liida 2 3 : nat
• liida 1 (liida 1 (liida 1 0)) : nat

Viimase termi puhul on lisatud sulud, et näidata tehete järjekorda. Enamik tüübiteooriaid nõuavad sulgude kasutamist, aga praktikas jäetakse nad välja, ning autorid eeldavad, et lugejad suudavad tehete järjekorra põhjal tehet mõista. Sarnaselt sellele võib kirjutada "liida x y" asemel ka lihtsustatult "x + y". Seega võib ülemisi terme kirjutada ka kui:

• 0 + 0 : nat
• 2 + 3 : nat
• 1 + (1 + (1 + 0)) : nat

Termid võivad sisaldada ka muutujaid. Igal muutujal on tüüp. Seega, kui eeldame, et "x" ja "y" on muutujad tüübist "nat", on järgnevad termid samuti kehtivad:

• x : nat
• x + 2 : nat
• x + (x + y) : nat

Peale "nat" ja "bool" tüüpide on ka muid tüüpe. Term "liida" ei ole "nat", vaid funktsioon, mis, rakendades kahele "nat" väärtusele, arvutatakse "nat"-iks.

Arvutus

Tüübiteoorial on sisseehitatud arusaam arvutusest. Järgnevad termid on kõik erinevad:

• 1 + 4 : nat
• 3 + 2 : nat
• 0 + 5 : nat

Siiski on nende tulemuseks sama term "5 : nat". Tüübiteoorias mõisted "reduktsioonist" ja "redutseerumisest" viitavad arvutusele. Seega "0 + 5 : nat" redutseerub termiks "5 : nat". Seda võib kirjutada kui "0 + 5 : nat $\twoheadrightarrow$ 5 : nat". Selline arvutus on mehaaniline ning see saavutatakse läbi termi süntaksi ümberkirjutamise.

Terme, mis sisaldavad muutujaid, saab samuti redutseerida. Seega term "x + (1 + 4) : nat" redutseerub kui "x + 5 : nat". Tänu Church-Rosseri teoreemile on võimalik termis redutseerida mistahes alamtermi.

Muutujateta termi, mida pole võimalik enam redutseerida, kutsutakse "kanooniliseks termiks". Kõik ülemised termid redutseeruvad termiks "5 : nat", mis on kanooniline term. Naturaalarvude kanoonilised termid on:

• 0 : nat
• 1 : nat
• 2 : nat, jne.

Termid, mida saab arvutada samaks termiks, on võrdsed. Seega, kui eeldada, et "x : nat", siis termid "x + (1 + 4) : nat" ja "x + (4 + 1) : nat" on võrdsed, sest nad mõlemad redutseeruvad termiks "x + 5 : nat". Kui kaks termi on võrdsed, saab neid üksteisega asendada. Võrdsus on tüübiteoorias keeruline teema ning eksisteerivad paljud erinevat laadi võrdsused.

Funktsioonid

Tüübiteoorias on funktsioonid termid. Funktsioonid võivad olla kas lambda-termid (ehk λ-termid) või olla defineeritud "reeglipõhiselt".

Lambda-termid

Lambda-term on kirjapildis "(λ muutuja : tüüp1 . term)" ning selle tüüp on "tüüp1 $\to$ tüüp2". Tüüp "tüüp1 $\to$ tüüp2" näitab, et lambda-term on funktsioon, mis võtab parameetri tüübiga "tüüp1" ning seda arvutatakse termiks tüübiga "tüüp2". Term lambda-termi sees peab olema väärtus tüübiga "tüüp2" eeldades, et muutuja on tüübiga "tüüp1".

Näide lambda-termist on funktsioon, mis korrutab oma argumendi kahega:

• (λ x : nat . (liida x x)) : nat $\to$ nat

Muutuja nimi on "x" ja muutujal on tüüp "nat". Term "(liida x x)" omab tüüpi "nat", eeldusel et "x : nat". Seega on lambda-termil tüüp "nat $\to$ nat", mis tähendab, et andes sellele argumendi tüübiga "nat", arvutatakse väärtus tüübiga "nat". Reduktsioon (ehk arvutus) on lambda-termide jaoks defineeritud. Kui funktsioon läbib aplikatsiooni (ehk saab kutsutud), asendatakse parameeter argumendiga.

Funktsiooni aplikatsioon kirjutatakse pannes argumendi pärast funktsiooni termi, seega võime eelnevat funktsiooni kutsuda "nat"-tüüpi argumendiga "5" kirjutades:

• (λ x : nat . (liida x x)) 5 : nat

Reduktsioon asendab parameetri "x" argumendiga "5". Niisiis saab seda termi arvutada kui:

• (liida 5 5) : nat

mida saab omakorda arvutada kui:

• 10 : nat

Lambda-termi kutsutakse sageli "anonüümseks funktsiooniks", sest talle pole antud nime. Lihtsustamise mõttes antakse lambda-termile sageli ka nimi, ehkki sellisel nimel pole matemaatilist tähendust. Funktsiooni saab seostada nimega kasutades järgmist kirjapilti:

• topelt : nat $\to$ nat ::= (λ x : nat . (liida x x))

On sama funktsioon, mis eelmine, kirjutatud teistmoodi. Seega termi

• topelt 5 : nat

saab arvutada samamoodi tulemuseni

• 10 : nat

Sõltuv tüüp

Sõltuv tüüpimine on juhus, kus funktsiooni tagastatud tüüp sõltub funktsiooni argumendi väärtusest. Näiteks, kui tüübiteooria defineerib tõeväärtuse tüübi "bool", defineerib ta ka funktsiooni "if". Funktsioon "if" võtab kolm argumenti. "if true b c" tagastab "b" ja "if false b c" tagastab "c". Aga mis tüüpi on "if a b c"?

Kui "b" ja "c" on sama tüüpi, on termi "if a b c" tüüp sama, mis "b" ja "c". Seega, (kui "a" on "bool"):

• if a 2 4 : nat
• if a false true : bool

Kui "b" ja "c" tüübid erinevad, sõltub "if a b c" tüüp "a" väärtusest. Kasutame sümbolit "Π", et tähistada funktsiooni, mis võtab argumendi ja tagastab tüübi. Eeldades, et meil on tüübid "B" ja "C" ning "a : bool", "b: B" ja "c: C", siis sellisel juhul "if" tüüp oleks järgnev:

• if : (Π a : bool . B $\to$ C $\to$ if a B C)
• if a b c : if a B C

See tähendab, et "if" termi tüüp on kas teise või kolmanda argumendi tüüp, olenevalt esimese argumendi väärtusest. Tegelikkuses ei ole "if a B C" defineeritud kasutades "if" termi, vaid kasutades veidi keerulisemaid struktuure.

Kuna taoline tüüp võib ise sisaldada arvutust, on sõltuv tüüpimine äärmiselt võimas. Näiteks võib läbi sõltuva tüüpimise väljendada matemaatikas lauseid "eksisteerib arv $x$ nii, et arv $x$ on algarv" või "eksisteerib arv $x$ nii, et omadus $P(x)$ on tõene." See tähendab, et omadus on tõestatud konkreetse "$x$" puhul, ning see on nähtav tulemuse tüübis.

Sagedased "reeglipõhised" tüübid ja termid

Tüübiteooriad on defineeritud tuletusreeglite järgi. On olemas reeglid "funktsionaalse tuuma" jaoks, mis on ülal välja toodud, ning reeglid, mis loovad tüüpe ja terme. Allpool on osaline nimekiri sagedastest tüüpidest ja nende termidest.

Tühi tüüp

Tühjal tüübil ei ole ühtegi termi. Tüüp ilmub tavaliselt kirjapildis kui "$\bot$" või "$\mathbb {0}$".

Seda kasutatakse näitamaks midagi, mida ei ole võimalik arvutada. Kui tüübi "A" puhul on võimalik luua funktsioon tüübiga "A $\to \bot$", on teada, et tüübil "A" ei ole terme. Näide tüübist "A" võiks olla "eksisteerib arv $x$, kus $x$ on paarisarv ja $x$ on paaritu arv." Kui tüübil pole terme, öeldakse, et see on "asustamata".

Ühiktüüp

Ühiktüübil on täpselt üks kanooniline term. See kirjutatakse kui "$\top$" või "$\mathbb {1}$" ning selle ainus kanooniline term kirjutatakse kui "*".

Ühiktüüp näitab, et miski eksisteerib või on arvutatav. Kui tüübi "A" puhul on võimalik luua funktsioon tüübiga "$\top \to$ A", on teada, et tüübil "A" on vähemalt üks term. Kui tüübil on vähemalt üks term, öeldakse, et see on "asustatud".

Boole'i tüüp

Boole'i tüübil on täpselt kaks kanoonilist termi. Tüüp kirjutatakse tavaliselt kui "bool", "$\mathbb {B}$" või "$\mathbb {2}$". Kanoonilised termid on tavaliselt "tõene" ja "väär", ehk inglise keeles "true" ja "false".

Boole'i tüüp on defineeritud elimineeriva funktsiooniga "if", nii et:

• if true b c $\twoheadrightarrow$ b
• if false b c $\twoheadrightarrow$ c

Korrutistüüp

Korrutistüübi termid on järjestatud paarid. Tüüpide "A" ja "B" puhul on korrutistüüp kirjutatud kui "A $\times$ B". Kanoonilisi terme toodab konstruktorfunktsioon "pair". Term on "pair a b", kus "a" on term tüübist "A" ning "b" on term tüübist "B". Korrutistüüp on defineeritud elimineerivate funktsioonidega "first" ja "second" ("esimene" ja "teine"), nii et:

• first (pair a b) $\twoheadrightarrow$ a
• second (pair a b) $\twoheadrightarrow$ b

Peale järjestatud paaride kasutatakse seda tüüpi loogiliseks konjunktsiooniks (ehk "ning"), sest ta koosneb "A" ja "B" tüüpidest. Seda kasutatakse ka ühisosa jaoks, sest ta koosneb ühest kummastki tüübist.

Summatüüp

Summatüüp on "sildistatud ühend". See tähendab, et tüüpide "A" ja "B" puhul hoiab tüüp "A + B" kas "A" tüüpi termi või "B" tüüpi termi, ning ta teab ka, millist. Tüüp tuleneb konstruktoritest "injectionLeft" (vasak injektsioon) ja "injectionRight" (parem injektsioon). Aplikatsioon "injectionLeft a" võtab termi "a : A" ning tagastab kanoonilise termi tüübist "A + B". Sarnaselt, "injectionRight b" võtab "b : B" ja tagastab samuti kanoonilise termi tüübist "A + B". Tüüp on defineeritud elimineeriva funktsiooniga "match" (sobitama) nõnda, et tüübi "C" ja funktsioonide "f : A $\to$ C" ja "g : B $\to$ C" puhul:

• match (injectionLeft a) C f g $\twoheadrightarrow$ (f a)
• match (injectionRight b) C f g $\twoheadrightarrow$ (g b)

Summatüüpi kasutatakse loogilise disjunktsiooni ja ühendi jaoks.

Erinevused hulgateooriast

Matemaatika traditsiooniliseks aluseks on hulgateooria koos mingi loogikaga. Kõige levinum on Zermelo-Fraenkeli hulgateooria, lühendatult "ZF", ning valikuaksioomiga tuntud kui "ZFC". Tüübiteooriad erinevad sellest alusest mitmel moel:

• Hulgateoorial on reeglid ja aksioomid, aga tüübiteooriatel on vaid reeglid. Hulgateooriad on üles ehitatud loogikale. Seega on ZFC defineeritud nii esimese järgu loogika reeglite ja omaenda aksioomide järgi. Tüübiteooriatel üldjuhul pole aksioome ning neid defineerivad vaid nende tuletusreeglid.
• Klassikaline hulgateooria ja loogika järgivad välistatud kolmanda seadust, mille järgi on iga teoreem kas tõene või väär. Kui tüübiteooria defineerib "ning" ja "või" mõisted tüüpidena, on tulemuseks intuitsionistlik loogika, mis ei järgi välistatud kolmanda seadust. See-eest võib seadust teatud tüüpide puhul tõestada.
• Hulgateoorias ei ole element piiratud ilmuma vaid ühes hulgas. Element võib ilmuda alamhulkades või ühendites teiste hulkadega. Tüübiteoorias kuuluvad termid (üldjuhul) vaid ühe tüübi alla. Alamhulga asemel võib tüübiteooria kasutada predikaatfunktsiooni või sõltuvalt-tüübitud korrutistüüpi, kus iga element $x$ on paaris tõestusega, et alamhulga omadus on tõene $x$ puhul. Ühendi asemel kasutab tüübiteooria summatüüpi, mis sisaldab uusi kanoonilisi terme.
• Tüübiteoorial on sisseehitatud arusaam arvutusest. Seega on "1+1" ja "2" küll erinevad termid, aga arvutades jõuavad nad sama väärtuseni. Funktsioone defineeritakse arvutuslikult kui lambda-terme. See-eest hulgateoorias "1+1=2", seega on "1+1" lihtsalt erinev viis viidata väärtusele "2". Tüübiteooria arvutus nõuab keerulist arusaama võrdsusest.
• Hulgateooria kodeerib arvud tavaliselt hulkadena (hulgateooria definitsioonis naturaalarvudest on 0 tühi hulk; 1 on hulk, mis sisaldab tühja hulka, jne.). Tüübiteooria võib kodeerida arvusid kui Churchi numeraale või kui induktiivseid tüüpe. Induktiivse tüübi poolt loodud konstruktorid "0" ja "S" sarnanevad Peano aksioomidele.
• Tüübiteoorias on tõestused esmaklassilised väärtused.

Tüübiteooria toetajad sageli viitavad selle seosele konstruktiivse matemaatikaga läbi Brouwer-Heyting-Kolmogorovi tõlgenduse, selle seosele loogikaga läbi Curry-Howardi vastavuse ning selle seostele kategooriateooriaga.

Välislingid

• "Type Theory" veebilehel nLab, millel on artikleid paljudel teemadel (inglise keeles)
• Intuitsionistlik tüübiteooria artikkel, Stanford Encyclopedia of Philosophy (inglise keeles)
• Lambda Calculi with Types Henk Barendregti raamat (inglise keeles)
• Calculus of Constructions / Typed Lambda Calculus õpiku stiilis artikkel, Helmut Brandl (inglise keeles)
• Intuitsionistlik tüübiteooria Per Martin-Löfi märkmed (inglise keeles)
• Programming in Martin-Löf's Type Theory raamat (inglise keeles)
• Homotopy Type Theory raamat, mis pakkus välja homotüüpse tüübiteooria matemaatilise alusteooriana (inglise keeles)