Typeteori

Fra Wikipedia, den frie encyklopedi
Gå til: navigasjon, søk

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 studie 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"), \lambda^\to, 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 B er en mengde med "basistyper",

\tau ::= \tau \to \tau \mid T \quad \mathrm{hvor} \quad T \in B.

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

B = \{ \mathrm{nat},\; \mathrm{bool} \},

hvor nat står for naturlige tall, og bool for bolske verdier. Da vil f.eks. typen  \mathrm{nat} \to \mathrm{bool} 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  \mathrm{nat} \to \mathrm{nat} \to \mathrm{nat}.

Termene i \lambda^\to er definert som

e ::= x \mid e\,e \mid \lambda x : \tau. e.

Her represetnerer \lambda x : \tau . e en funksjon som tar et argument x av typen \tau, og som returnerer e. Jukstaposisjon av to termer, e_1 \, e_2 representerer funksjonskall (vanlig notasjon innen matematikk er e_1(e_2)), og x er referanse til en variable.

Typesjekking[rediger | rediger kilde]

Relasjonen \Gamma \vdash e\,:\,\tau definerer hvorvidt et uttykk e har typen \tau under antagelsene \Gamma = x_1 : \tau_1, \ldots, x_n : \tau_n (hvor x_i : \tau_i representerer antagelsen at variabelen x har typen \tau). \Gamma kalles en kontekst. Relasjonen defineres som følger:

{x\mathbin{:}\sigma \in \Gamma\over\Gamma \vdash x\mathbin{:}\sigma } (var) {\Gamma,x\mathbin{:}\sigma\vdash e\mathbin{:}\tau\over\Gamma\vdash (\lambda x\mathbin{:}\sigma.~e)\mathbin{:}(\sigma \to \tau)} (lam) {\Gamma\vdash e_1\mathbin{:}\sigma\to\tau\quad\Gamma\vdash e_2\mathbin{:}\sigma\over\Gamma\vdash e_1~e_2\mathbin{:}\tau} (app)

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

Semantikk[rediger | rediger kilde]

Standardsemantikken for lambda kalkylen er \beta-reduksjon, som kan defineres som  (\lambda x : \tau . e_1)\, e_2 \to_\beta e_1[e_2 / x], hvor e_1[e_2 / x] er funksjonen som substituerer alle frie forekomster av x i e_1 med e_2, og samtidig passer på at ingen av de fri variablene i e_2 blir bundet av binderne i e_1. Siden et uttrykk på formen (\lambda x : \tau . e_1) e_2 kan \beta-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 \beta-reduksjon hvor som helst i en term. Relasjonen defineres som følger:

{ e \to_\beta e'  \over e \to e'} { e \to e' \over \lambda x : \tau . e \to \lambda x : \tau . e' } { e \to e' \over e \, e_2 \to e' \, e_2} { e \to e' \over e_1 \, e \to e_1 \, e'}

Gjentatt reduksjon representeres med relasjonen e \to^* e', som tilsvarer den refleksive og transitive tillukkningen av e \to e', og som defineres som :

{ \mathrm{} \over e \to^* e}  { e_1 \to e_2 \quad e_2 \to^* e_3 \over e_1 \to^* e_3}

Hvis en term e ikke kan reduseres, altså, det finnes ingen e' slik at  e \to e', så kalles e en verdi. Det er bevist at for alle termer e, kontekster \Gamma og typer \tau slik at  \Gamma \vdash e : \tau, så vil e \to e' slik at e' er en verdi. Dette er ikke tilfellet for utypet lambdakalkyle, hvor f.eks. termen (\lambda x. x \, x) (\lambda x. x \, x) ikke reduserer til noen verdi.

Lambdakalkyle à la Curry[rediger | rediger kilde]

Presentasjonen av \lambda^\to 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:

 e ::= x \mid \lambda x . e \mid e \, e

og typerelasjonen er

  { \Gamma(x) = \tau \over \Gamma \vdash x : \tau } (var)  { \Gamma \vdash e_1 : \tau_2 \to \tau_2 \quad \Gamma \vdash e_2 : \tau_2 \over \Gamma \vdash e_1 \, e_2 : \tau_2} (app)   { \Gamma, x : \tau_2 \vdash e : \tau_2 \over \Gamma \vdash \lambda x . e : \tau_1 \to \tau_2 } (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 e i \lambda^\to à 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 \lambda^\to en unik normalform (opp til alpha-ekvivalens).

System F[rediger | rediger kilde]

System F generaliserer \lambda-kalkyle med endelige typer, ved å legge til kvantifisering over typer. Typesystemet går også under navnene Andreordens \lambda-kalkulus og polymorfisk \lambda-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 \lambda x . x, altså identitetsfunksjone, så kan man se at den har typen \tau \to \tau for alle \tau i \lambda^\to à 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 \lambda^\to 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 \alpha, så er \tau en type, hvor \alpha kan forekomme fritt i \tau. Konkret notasjon for kvantoren er \forall \alpha . \tau. Her er noen eksempler på funksjonstyper hvor allkvantoren kommer til nytte:

  •  identity : \forall \alpha. \; \alpha \to \alpha . Identitetsfunksjonen.
  •  cons : \forall \alpha. \; \alpha \to \mathrm{List}\;\alpha \to \mathrm{List}\;\alpha. Funksjonen som legger til et element forran på en liste.
  •  map : \forall \alpha. \forall \beta. \; \mathrm{List}\,\alpha \to (\alpha \to \beta) \to \mathrm{List}\,\beta (Hvor List er antatt en primitiv type for lister med elementer av en gitt type.)
  •  \forall \alpha . \alpha \to (\alpha \to \alpha) \to \alpha. Typen for Church-enkodingen av naturlige tall.

Definisjon[rediger | rediger kilde]

Typene fra \lambda^2 utvides med to nye former:

 \tau ::= T \mid \alpha \mid \tau \to \tau \mid \forall \alpha . \tau

hvor \alpha kalles en type-variabel, og \forall \alpha . \tau representerer polymorfi.

Termene utvides med to nye konstruktører:

 e ::= x \mid e\,e \mid \lambda x : \tau . e \mid \Lambda \alpha . e \mid e\,\tau

hvor \Lambda \alpha. e sier at termen e skal fungere for alle typer satt inn i e, og e\,\tau, som forventer at e er av typen \forall \alpha . \tau', betyr at uttrykket e skal spesialiseres til typen \tau.

Typereglene for System F er som for \lambda^\to, men med to ekstra regler:  \Gamma \vdash e : \tau \quad \alpha \not\in \mathrm{FV}(\Gamma) \over \Gamma \vdash \Lambda \alpha . e : \forall \alpha. \tau og  \Gamma \vdash e : \forall \alpha . \tau_1 \over \Gamma \vdash e\,\tau_2 : \tau_1[\tau_2 / \alpha] . Notasjonen \mathrm{FV(\Gamma)} betyr her mengden av frie type-variabler som forekommer i \Gamma.

Eksempler[rediger | rediger kilde]

Vi kan observere at vi nå kan definere en genrell identitetsfunksjon,  \Lambda \alpha.\, \lambda x : \alpha . x som har typen  \forall \alpha . \alpha \to \alpha. Hvis vi kaller funksjonen id ser vi at uttrykket id\, \mathrm{nat} har typen \mathrm{nat} \to \mathrm{nat}.

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

  • La nat være en forkortelse for typen \forall \alpha . \alpha \to (\alpha \to \alpha) \to \alpha.
  • La 0 være definert som \forall \alpha. \lambda x : \alpha . \lambda f : \alpha \to \alpha . x. Observer at \vdash 0 : nat.
  • La S være definert som \lambda n : nat. \forall \alpha . \lambda x : \alpha. \lambda f : \alpha \to \alpha. n \alpha\, x\, (f\, x). Navnet S er første bokstav i suksessor, og representerer pluss en funksjonen. Observer at \vdash S : nat \to nat.

Barendregts lambda-kube[rediger | rediger kilde]

Lambda cube

Matematikeren Henk Barendregt utviklet lambda-kuben, \lambda-kuben, for å utforske forskjellige utvidelser av typesystemer. Han tar utgangspunkt i \lambda^\to, 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 \lambda^\to 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 \lambda-kuben definerer man derfor pseudo-termer som

 \mathcal{T} ::= x \mid C \mid \mathcal{T}_1\, \mathcal{T}_2 \mid \lambda x : \mathcal{T}_1 . \mathcal{T}_2 \mid \Pi x : \mathcal{T}_1 . \mathcal{T}_2

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

Felles regler[rediger | rediger kilde]

Alle systemene har noen regler til felles.

{ \mathrm{} \over \cdot \vdash * : \Box } (ax) En type er en kind.
 { \Gamma \vdash N : A \over \Gamma, x : B \vdash N : A } (wk) Man kan legge til variabler.
 { \mathrm{} \over \Gamma, x : A \vdash x : A } (var)
 { \Gamma \vdash N : \Pi x : A . B \quad \Gamma \vdash M : A \over \Gamma \vdash N \, M : B[M/x] } (app)
 { \Gamma, x : A \vdash N : B \over \Gamma \vdash \lambda x : A . N : \Pi x : A . B } (abs)
{ \Gamma \vdash N : A \quad A =_\beta A' \over \Gamma \vdash N : A' } (conv)

Parametriske regler[rediger | rediger kilde]

Følgende regel er parametrisk i  s_1, s_2 \in \{ *, \Box \}.

\Gamma \vdash A : s_1 \quad \Gamma, x : A \vdash B : s_2 \over \Gamma \vdash \Pi x:A.B : s_2

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

Dependent typer Polymorfi Typeoperatorer Forkortelse Navn
(*, *)      \lambda^\to Simply typed lambda calculus
(*, *)     (\Box, \Box)  \lambda\underline\omega
(*, *)    (\Box, *)  \lambda 2 System F
(*, *)    (\Box, *) (\Box, \Box)  \lambda\omega System F\omega
(*, *)  (*, \Box)    \lambda P LF (Logical Framework)
(*, *)  (*, \Box)   (\Box, \Box)  \lambda P \underline\omega
(*, *)  (*, \Box)  (\Box, *)  \lambda P 2
(*, *)  (*, \Box)  (\Box, *) (\Box, \Box)  Coc, \lambda C, \lambda P\omega Calculus of Construction


Egenskaper ved typesystemer[rediger | rediger kilde]

To klassiske egenskaper som typesystemer kan ha er:

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

Litteratur[rediger | rediger kilde]