Typteori

Den aktuella versionen av sidan har ännu inte granskats av erfarna bidragsgivare och kan skilja sig väsentligt från versionen som granskades den 6 december 2021; kontroller kräver 2 redigeringar .

Typteori är vilket formellt system som helst , som är ett alternativ till naiv mängdteori , åtföljt av en klassificering av elementen i ett sådant system med hjälp av typer som bildar en viss hierarki. Typteori förstås också som studiet av sådana formalismer.

Typteori är en matematiskt formaliserad grund för att designa, analysera och studera datatypsystem i teorin om programmeringsspråk (sektionen för datavetenskap ). Många programmerare använder denna term för att referera till alla analytiska arbeten som studerar typsystem i programmeringsspråk. I vetenskapliga kretsar förstås typteori oftast som en smalare gren av diskret matematik , i synnerhet λ-kalkyl med typer.

Modern typteori utvecklades delvis i processen för att lösa Russells paradox och är till stor del baserad på Bertrand Russells och Alfred Whiteheads arbete " Principia mathematica " [1] .

Skriv Doktrin

Läran om typer går tillbaka till B. Russell, enligt vilken vilken typ som helst anses vara ett intervall av betydelse för en propositionell (propositionell) funktion. Dessutom tror man att varje funktion har en typ (dess domän, omfattning). I doktrinen om typer respekteras genomförbarheten av principen att ersätta en typ (proposition) med en definitionsmässigt ekvivalent typ (proposition) .

Skriv teori i logik

Denna teori bygger på principen om hierarki. Detta innebär att logiska begrepp - påståenden , individer, propositionella funktioner - är ordnade i en hierarki av typer. Det är väsentligt att en godtycklig funktion har som argument endast de begrepp som föregår den i hierarkin.

Någon typteori

En viss typteori förstås vanligtvis som tillämpad logik av högre ordning, där det finns en typ N av naturliga tal och där axiomen för Peano- aritmetiken är uppfyllda .

Branched type theory

Historiskt sett är den första föreslagna teorin om typer (perioden från 1902 till 1913) Ramified Theory of Types ( RTT ) , byggd av Whitehead och Russell, och slutligen formulerad i det grundläggande verket Principia Mathematica . Denna teori bygger på principen att begränsa antalet fall då objekt tillhör en enda typ. Åtta sådana fall deklareras uttryckligen, och två typhierarkier urskiljs: (helt enkelt) "typer" och "ordrar". Samtidigt är själva "typ"-notationen inte definierad, och det finns ett antal andra felaktigheter, eftersom huvudavsikten var att deklarera olika typer av funktioner från ett annat antal argument eller från argument av olika typer [2] . En integrerad del av teorin är reducerbarhetens axiom .

Enkel typteori

På 1920-talet föreslog Chwistek och Ramsey en oframifierad typteori, nu känd som "Simple Type Theory" eller Simple Type Theory , som kollapsar typhierarkin, vilket eliminerar behovet av reducerbarhetens axiom.

Intuitionistisk typteori

Intuitionistisk typteori ( ITT ) byggdes av Per Martin-Löf .

System av ren typ

Teorin om rentypssystem ( eng.  pure type systems , PTS ) generaliserar alla lambda- kubkalkyler och formulerar regler som gör att de kan beräknas som specialfall. Det byggdes oberoende av Berardi och Terlouw . System av ren typ fungerar endast med begreppet typ, med tanke på alla begrepp för andra kalkyler endast i form av typer - det är därför de kallas " rena ". Det finns ingen separation mellan termer och typer, mellan olika lager (dvs. släkten av typer kallas också typer, bara relaterade till ett annat universum), och även lagren i sig kallas inte varieteter , utan typer (mer exakt, universum av typer) . I allmänhet definieras ett system av ren typ av begreppet en specifikation, fem hårda regler och två flexibla (som varierar från system till system). Specifikationen för ett system av ren typ är en trippel (S, A, R), där ärS uppsättningen av sorter ( Sorts ), Aär uppsättningen av axiom ( Axiom ) över dessa sorter, och Rär uppsättningen av regler ( Regler ). [3] [4] [5]

Flerdimensionella typteorier

Teorier med högre dimensioner eller helt enkelt teorier om högre typ ( HTT ) generaliserar traditionella typteorier , vilket gör att icke-triviala ekvivalensförhållanden mellan typer kan etableras .  Till exempel, om man tar en uppsättning par ( kartesiska produkter ) av naturliga tal och en uppsättning funktioner som returnerar ett naturligt tal , så kan man inte säga att elementen i dessa mängder är parvis lika, men man kan säga att dessa mängder är likvärdig. Isomorfismer mellan typer och studeras i tvådimensionell, tredimensionell, etc. typteorier. Hela den nödvändiga grunden för formuleringen av dessa teorier lades av Girard-Reynolds , men själva teorierna formulerades långt senare. [6] [7]nat × natnat -> nat

Homotopi typteori

Homotopy type theory ( eng. Homotopy  type theory , HoTT ) generaliserar flerdimensionella teorier och etablerar likhet mellan typer på topologinivå . I flerdimensionella teorier anses begreppen "typekvivalens" och "typlikhet" vara olika. En radikal innovation inom homotopi-teorin är axiomet för univalens , som postulerar att om typerna är topologiskt likvärdiga, så är de topologiskt lika.

Ekonomisk typteori

Cost -Aware Type Theory ( CATT )  , formulerad 2020 , utökar funktionstyper med den enklaste informationen om algoritmisk komplexitet  - antalet beräkningssteg som krävs för att erhålla ett resultat - vilket gör att du kan verifiera program inte bara för semantisk korrekthet, utan också för påtvingade tidskomplexitetsbegränsningar. [8] Detta görs genom konstruktorn av beroende funktionstyper . Formaliseringen av teorin kräver bland annat att man tar hänsyn till stoppproblemet , för vilket skrivreglerna kräver att det rekursiva anropet är strikt mindre komplext än anropet med det aktuella värdet av argumentet. CATT tillåter att ett bevis kan skiljas mellan "abstrakt kostnad" som involverar matematiska steg (som ett rekursivt anrop) och "maskinkostnad" med hänsyn till effektiviteten hos fysiskt implementerade instruktioner (till exempel att summa- och produktaritmetiska operationer tar samma tid på de flesta processorer). ), och ta även hänsyn till parallellism . funtime

Se även

Anteckningar

  1. ↑ "Foundations of Mathematics" - en grundläggande trevolymsbok om matematisk logik (Whitehead, Alfred N. Foundations of Mathematics: I 3 volymer / A. N. Whitehead, B. Russell; redigerad av G. P. Yarovoy, Yu. N. Radaev. - Samara : Samara University Publishing House, 2005-2006 - ISBN 5-86465-359-4 )
  2. ↑ Modern Perspective on Type Theory, 2004 , 2b The Ramified Theory of Types RTT, p. 35.
  3. ↑ Barendregt, "Lambda Calculi with Types", 1992 , 5.2. Rent typsystem, sid. 96-114.
  4. ↑ Modern Perspective on Type Theory, 2004 , 4c Pure Type Systems, sid. 116.
  5. ↑ Pierce, 2002 , sid. 493.
  6. ↑ Harper, "Higher-Dimensional Type Theory", 2011 .
  7. ↑ Robert Harper Research Papers (länk inte tillgänglig) . Hämtad 20 oktober 2016. Arkiverad från originalet 30 oktober 2016. 
  8. ↑ Yue Niu, Robert Harper. Kostnadsmedveten typteori. - Carnegie Mellon University, 2020. - arXiv : 2011.03660v1 .

Litteratur

Länkar

  Gå till Wikidata-objektet  Ordböcker och uppslagsverk