Typeteori

Fra Wikipedia, den frie encyklopedi

I matematikk, informatikk og logikk er typeteori studien av visse formelle systemer som relaterer termer til typer. Typeteori ble opprinnelig utviklet for reparere Russels og Whiteheads logiske system Principia Mathematica, som Kurt Gödel i 1902 oppdaget var inkonsistent, men typeteori er i dag et studium i seg selv. Det forskes på bruk av typeteori som et alternativ til mengdelære som fundamentet for matematikk, og det er en nær sammenheng mellom datatyper, slik man finner dem i programmeringsspråk, og typene i typeteori. Videre er det en tett sammenheng med logikk, tydeliggjort av Curry-Howard-korrespondansen.

Lambdakalkylen med endelige typer[rediger | rediger kilde]

Lambdakalylen med endelig typer (eng: "simply typed lambda calculus"), , ble utviklet av Alonzo Church i 1940, i et forsøk på temme den utypete lambdakalkylen, som er logisk sett inkonsistent.

Syntaks[rediger | rediger kilde]

Den syntaktiske kategorien for typer defineres som følger, hvor er en mengde med "basistyper",

.

Et eksempel på basistyper som man kan finne i programmeringsspråk er

,

hvor nat står for naturlige tall, og bool for bolske verdier. Da vil f.eks. typen representere en funksjon som tar et naturlig tall og returnerer en boolsk verdi. En funksjon som tar flere argumenter, f.eks. pluss funksjonen, vil ha typen .

Termene i er definert som

.

Her represetnerer en funksjon som tar et argument av typen , og som returnerer . Jukstaposisjon av to termer, representerer funksjonskall (vanlig notasjon innen matematikk er ), og er referanse til en variable.

Typesjekking[rediger | rediger kilde]

Relasjonen definerer hvorvidt et uttykk har typen under antagelsene (hvor representerer antagelsen at variabelen har typen ). kalles en kontekst. Relasjonen defineres som følger:

(var) (lam) (app)

For å være formell, må det spesifiseres hva er og hva og skal bety. Det er flere måter å gjøre dette på. Det konseptuelt enkleset er å si at er en endelig, partiell funksjon fra mengden av variabler til typer, og å definere som funksjonen slik at , og ellers , gitt at .

Semantikk[rediger | rediger kilde]

Standardsemantikken for lambda kalkylen er -reduksjon, som kan defineres som , hvor er funksjonen som substituerer alle frie forekomster av i med , og samtidig passer på at ingen av de fri variablene i blir bundet av binderne i . Siden et uttrykk på formen kan -reduseres, kalles uttrykk på den formen en "redex" (eng "reducable expression", norsk: reduserbart uttrykk).

Denne relasjonen kan så løftes til en relasjon som gjør en enkel -reduksjon hvor som helst i en term. Relasjonen defineres som følger:

Gjentatt reduksjon representeres med relasjonen , som tilsvarer den refleksive og transitive tillukkningen av , og som defineres som :

 

Hvis en term ikke kan reduseres, altså, det finnes ingen slik at , så kalles en verdi. Det er bevist at for alle termer , kontekster og typer slik at , så vil slik at er en verdi. Dette er ikke tilfellet for utypet lambdakalkyle, hvor f.eks. termen ikke reduserer til noen verdi.

Lambdakalkyle à la Curry[rediger | rediger kilde]

Presentasjonen av i avsnittene over, er presentert à la Church, siden termene er annotert med typer. Et alternativ er å beholde de utypede termene fra den utypede lambdakalkylen. Dette kalles à la Curry, og definisjonen av termer er da:

og typerelasjonen er

  (var) (app)   (lam)

Hvorvidt et typesystem er presentert à la Curry eller Church vil få følger for hvilke egenskaper systemet får. F.eks. kan et uttrykk i à la Church kun ha en type, mens i à la Curry kan et term ha mange forskjellige typer. For mer uttrykksfulle typesystemer, så kan typesjekking bli uavgjørbart i Curry form, mens de oftere er avgjørbare i Church form. Noen typesystemer har kun mening i en av formuleringene.

Normalform[rediger | rediger kilde]

I motsetning til utypet lambdakalkyle, så har alle vell-typede termer i en unik normalform (opp til alpha-ekvivalens).

System F[rediger | rediger kilde]

System F generaliserer -kalkyle med endelige typer, ved å legge til kvantifisering over typer. Typesystemet går også under navnene Andreordens -kalkulus og polymorfisk -kalkulus. System F ble oppdaget av både logikeren Jean-Yves Girard og informatikeren John C. Reynolds uanvhengig av hverandre.

Motivasjon[rediger | rediger kilde]

Hvis man ser på den utypede funksjonen , altså identitetsfunksjone, så kan man se at den har typen for alle i à la Curry. Men hvis funksjonen forekommer som en del-term og den bindes til en variabel, så vil den variabelen kun ha èn type i den gitte derivasjonen. Det betyr at i må man gjenta definisjoner for forskjellige typer, selv om det er «unødvendig».

I System F løses dette ved å innføre variabler for typer og en kvantor som gjør det mulig å uttrykke for alle typer , så er en type, hvor kan forekomme fritt i . Konkret notasjon for kvantoren er . Her er noen eksempler på funksjonstyper hvor allkvantoren kommer til nytte:

  • . Identitetsfunksjonen.
  • . Funksjonen som legger til et element foran i en liste.
  • (Hvor er antatt en primitiv type for lister med elementer av en gitt type.)
  • . Typen for Church-enkodingen av naturlige tall.

Definisjon[rediger | rediger kilde]

Typene fra utvides med to nye former:

hvor kalles en type-variabel, og representerer polymorfi.

Termene utvides med to nye konstruktører:

hvor sier at termen skal fungere for alle typer satt inn i , og , som forventer at er av typen , betyr at uttrykket skal spesialiseres til typen .

Typereglene for System F er som for , men med to ekstra regler: og . Notasjonen betyr her mengden av frie type-variabler som forekommer i .

Eksempler[rediger | rediger kilde]

Vi kan observere at vi nå kan definere en genrell identitetsfunksjon, som har typen . Hvis vi kaller funksjonen ser vi at uttrykket har typen .

Det er også mulig å representere naturlige tall ved å benytte Churchs enkoding i System F. Ideen bak Churchs enkoding er at et tall representeres av en iterator som itererer ganger. I utypet -kalkyle kan man definere 0 som , altså funksjonen som tar et element og en funksjon , og sender gjennom funksjonen null ganger. Videre defineres 1 som , altså funksjonen som sender gjennom en gang, og 2 defineres som , funksjonen som sender gjennom to ganger. Generelt defineres tallet som funksjonen .

  • La være en forkortelse for typen .
  • La være definert som . Observer at .
  • La være definert som . Navnet er første bokstav i suksessor, og representerer pluss en funksjonen. Observer at .

Barendregts lambda-kube[rediger | rediger kilde]

Lambda cube

Matematikeren Henk Barendregt utviklet lambda-kuben, -kuben, for å utforske forskjellige utvidelser av typesystemer. Han tar utgangspunkt i , og ser på tre utvidelser, som vises som akser i kuben:

  1. Typeoperatorer — typer som er avhenger av typer, z-aksen
  2. Polymorphisme — termer som avhenger av typer, y-aksen
  3. Dependent typer — typer som avhenger av termer, x-aksen

Disse utvidelsene gir opphav til åtte forskjellige typesystemer, avhengig av hvilke utvidelser man tar med. Lambda-kuben gir et rammeverk som definerer alle åtte systemene samtidig, men det er også mulig å definere hvert system for seg selv. Hvis man ikke tar med noen av utvidelsene så får man som beskrevet over, og tar man med alle, får man noe som tilsvarer Calculus of Constructions.

Definisjon av lambda kuben[rediger | rediger kilde]

Det er ikke lenger praktisk å ha to seperate syntaktiske kategorier for termer og typer, og i -kuben definerer man derfor pseudo-termer som

hvor er en mengde konstanter, som minst inneholder (les: type) og (les: 'kind').

Felles regler[rediger | rediger kilde]

Alle systemene har noen regler til felles.

(ax) En type er en kind.
  (wk) Man kan legge til variabler.
  (var)
  (app)
  (abs)
(conv)

Parametriske regler[rediger | rediger kilde]

Følgende regel er parametrisk i .

Man kan bestemme hvilket typesystem man ønsker ved å bestemme hvilke instanser av man som er godtatt. Tabellen under lister opp alle mulighetene.

Dependent typer Polymorfi Typeoperatorer Forkortelse Navn
      Simply typed lambda calculus
     
      System F
      System F
      LF (Logical Framework)
     
     
     Coc, , Calculus of Construction


Egenskaper ved typesystemer[rediger | rediger kilde]

To klassiske egenskaper som typesystemer kan ha er:

  • Preservering (eng: subject reduction el. preservation): hvis og , så . Altså, reduksjon bevarer typen.
  • Progresjon (eng: progress): hvis , så er enten en verdi, eller så eksisterer en slik at . Altså, vel-typede termer henger ikke.

Litteratur[rediger | rediger kilde]