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 "formula_1" 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:
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:
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:
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:
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:
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 formula_2 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:
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 formula_3 tüüp2". Tüüp "tüüp1 formula_3 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:
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 formula_3 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:
Reduktsioon asendab parameetri "x" argumendiga "5". Niisiis saab seda termi arvutada kui:
mida saab omakorda arvutada kui:
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: 
On sama funktsioon, mis eelmine, kirjutatud teistmoodi. Seega termi
saab arvutada samamoodi tulemuseni
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"):
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:
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 formula_10 nii, et arv formula_10 on algarv" või "eksisteerib arv formula_10 nii, et omadus formula_13 on tõene." See tähendab, et omadus on tõestatud konkreetse "formula_10" 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 "formula_15" või "formula_16".
Seda kasutatakse näitamaks midagi, mida ei ole võimalik arvutada. Kui tüübi "A" puhul on võimalik luua funktsioon tüübiga "A formula_17", on teada, et tüübil "A" ei ole terme. Näide tüübist "A" võiks olla "eksisteerib arv formula_10, kus formula_10 on paarisarv ja formula_10 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 "formula_21" või "formula_22" 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 "formula_23 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", "formula_24" või "formula_25". 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:
Korrutistüüp.
Korrutistüübi termid on järjestatud paarid. Tüüpide "A" ja "B" puhul on korrutistüüp kirjutatud kui "A formula_28 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:
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 formula_3 C" ja "g : B formula_3 C" puhul:
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:
Tüübiteooria toetajad sageli viitavad selle seosele konstruktiivse matemaatikaga läbi Brouweri-Heytingi-Kolmogorovi tõlgenduse, selle seosele loogikaga läbi Curry-Howardi vastavuse ning selle seostele kategooriateooriaga.