Redigerer Typeteori


I [[matematikk]], [[informatikk]] og [[logikk]] er '''typeteori''' studien av visse formelle systemer som relaterer termer til typer.
Typeteori ble opprinnelig utviklet for reparere [[Bertrand Russell|Russel]]s og [[Alfred North Whitehead|Whitehead]]s logiske system ''Principia Mathematica'', som
[[Kurt Gødel|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 [[Datatype|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 ==
[[Lambdakalkyle|Lambdakalylen]] med endelig typer (eng: "simply typed lambda calculus"), <math>\lambda^\to</math>, ble utviklet
av [[Alonzo Church]] i 1940, i et forsøk på temme den utypete lambdakalkylen, som er logisk sett inkonsistent.

=== Syntaks ===
Den syntaktiske kategorien for typer defineres som følger, hvor <math>B</math> er en mengde med "basistyper",
:<math>\tau ::= \tau \to \tau \mid T \quad \mathrm{hvor} \quad T \in B</math>.
Et eksempel på basistyper som man kan finne i programmeringsspråk er
:<math>B = \{ \mathrm{nat},\; \mathrm{bool} \}</math>,
hvor nat står for naturlige tall, og
bool for bolske verdier. 
Da vil f.eks. typen <math> \mathrm{nat} \to \mathrm{bool}</math> 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 <math> \mathrm{nat} \to \mathrm{nat} \to \mathrm{nat}</math>.

Termene i <math>\lambda^\to</math> er definert som 
:<math>e ::= x \mid e\,e \mid \lambda x : \tau. e</math>.
Her represetnerer <math>\lambda x : \tau . e</math> en funksjon
som tar et argument <math>x</math> av typen <math>\tau</math>,
og som returnerer <math>e</math>. Jukstaposisjon av to termer, <math>e_1 \, e_2</math>
representerer funksjonskall (vanlig notasjon innen matematikk er <math>e_1(e_2)</math>), og <math>x</math> er referanse til en variable.

=== Typesjekking ===
Relasjonen <math>\Gamma \vdash e\,:\,\tau</math> definerer hvorvidt et uttykk <math>e</math> har typen <math>\tau</math> under
antagelsene <math>\Gamma = x_1 : \tau_1, \ldots, x_n : \tau_n</math> (hvor <math>x_i : \tau_i</math> representerer antagelsen at variabelen <math>x</math> har typen <math>\tau</math>).
<math>\Gamma</math> kalles en ''kontekst''.
Relasjonen defineres som følger:
{| align="center" cellpadding="9"
| align="center" | <math>{x\mathbin{:}\sigma \in \Gamma\over\Gamma \vdash x\mathbin{:}\sigma }</math> (var)
| align="center" | <math>{\Gamma,x\mathbin{:}\sigma\vdash e\mathbin{:}\tau\over\Gamma\vdash (\lambda x\mathbin{:}\sigma.~e)\mathbin{:}(\sigma \to \tau)}</math> (lam)
| align="center" | <math>{\Gamma\vdash e_1\mathbin{:}\sigma\to\tau\quad\Gamma\vdash e_2\mathbin{:}\sigma\over\Gamma\vdash e_1~e_2\mathbin{:}\tau}</math> (app)
|}
For å være formell, må det spesifiseres hva <math>\Gamma</math> er og hva <math>\Gamma, x:\tau</math> og <math>\Gamma(x) = \tau</math> skal bety.
Det er flere måter å gjøre dette på. Det konseptuelt enkleset er å si at <math>\Gamma</math> er en endelig, partiell funksjon fra mengden av variabler til typer,
og å definere <math>\Gamma, x : \tau</math> som funksjonen slik at <math>(\Gamma, x : \tau)(x) = \tau</math>, og ellers <math>(\Gamma, x : \tau)(y) = \Gamma(y)</math>,
gitt at <math> x \not= y</math>.

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

Gjentatt reduksjon representeres med relasjonen <math>e \to^* e'</math>, som tilsvarer den refleksive og transitive tillukkningen av <math>e \to e'</math>, og som defineres som :
{| align="center" cellpadding="9"
| align="center" | <math>{ \mathrm{} \over e \to^* e}</math>
| align="center" | <math>{ e_1 \to e_2 \quad e_2 \to^* e_3 \over e_1 \to^* e_3}</math>
|}

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

=== Lambdakalkyle à la Curry ===
Presentasjonen av <math>\lambda^\to</math> 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:
:<math> e ::= x \mid \lambda x . e \mid e \, e </math> 
og typerelasjonen er
{| align="center" cellpadding="9"
| align="center" | <math> { \Gamma(x) = \tau \over \Gamma \vdash x : \tau } </math> (var)
| align="center" | <math> { \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} </math> (app)
| align="center" | <math> { \Gamma, x : \tau_2 \vdash e : \tau_2 \over \Gamma \vdash \lambda x . e : \tau_1 \to \tau_2 } </math> (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 <math>e</math> i <math>\lambda^\to</math> à 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 ===
I motsetning til utypet lambdakalkyle, så har alle vell-typede termer i <math>\lambda^\to</math> en unik normalform (opp til [[Lambdakalkyle#Alpha-konvertering|alpha-ekvivalens]]).

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

=== Motivasjon ===
Hvis man ser på den utypede funksjonen <math>\lambda x . x</math>, altså identitetsfunksjone, så kan man se at den har typen <math>\tau \to \tau</math> for 
alle <math>\tau</math> i <math>\lambda^\to</math> à 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 <math>\lambda^\to</math> 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 <math>\alpha</math>, så er <math>\tau</math> en type'', hvor
<math>\alpha</math> kan forekomme fritt i <math>\tau</math>. Konkret notasjon for kvantoren er <math>\forall \alpha . \tau</math>. Her er noen eksempler på 
funksjonstyper hvor allkvantoren kommer til nytte:

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

=== Definisjon ===
Typene fra <math>\lambda^2</math> utvides med to nye former:
:<math> \tau ::= T \mid \alpha \mid \tau \to \tau \mid \forall \alpha . \tau </math>
hvor <math>\alpha</math> kalles en type-variabel, og <math>\forall \alpha . \tau</math> representerer polymorfi.

Termene utvides med to nye konstruktører:
:<math> e ::= x \mid e\,e \mid \lambda x : \tau . e \mid \Lambda \alpha . e \mid e\,\tau</math>
hvor <math>\Lambda \alpha. e</math> sier at termen <math>e</math> skal fungere for alle typer satt inn i <math>e</math>,
og <math>e\,\tau</math>, som forventer at <math>e</math> er av typen <math>\forall \alpha . \tau'</math>, betyr at uttrykket
<math>e</math> skal spesialiseres til typen <math>\tau</math>.

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

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

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

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

== Barendregts lambda-kube ==
[[File:Lambda cube.png|thumb|Lambda cube]]
Matematikeren [[Henk Barendregt]] utviklet lambda-kuben, <math>\lambda</math>-kuben, for å utforske forskjellige utvidelser av typesystemer.
Han tar utgangspunkt i <math>\lambda^\to</math>, og ser på tre utvidelser, som vises som akser i kuben:

# Typeoperatorer — typer som er avhenger av typer, z-aksen
# Polymorphisme — termer som avhenger av typer, y-aksen
# ''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 <math>\lambda^\to</math> som beskrevet over, 
og tar man med alle, får man noe som tilsvarer [[Calculus of Constructions]].

=== Definisjon av lambda kuben ===
Det er ikke lenger praktisk å ha to seperate syntaktiske kategorier for termer og typer, og i <math>\lambda</math>-kuben definerer man derfor pseudo-termer som
:<math> \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</math>
hvor <math>C</math> er en mengde konstanter, som minst inneholder <math>*</math> (les: type) og <math>\Box</math> (les: 'kind').

==== Felles regler ====
Alle systemene har noen regler til felles.
{| align="center" cellpadding="9"
| align="left" | <math>{ \mathrm{} \over \cdot \vdash * : \Box }</math> (ax) En type er en kind.
|-
| align="left" | <math>{ \Gamma \vdash N : A \over \Gamma, x : B \vdash N : A }</math> (wk) Man kan legge til variabler.
|-
| align="left" | <math>{ \mathrm{} \over \Gamma, x : A \vdash x : A }</math> (var) 
|- 
| align="left" | <math>{ \Gamma \vdash N : \Pi x : A . B \quad \Gamma \vdash M : A \over \Gamma \vdash N \, M : B[M/x] }</math> (app) 
|- 
| align="left" | <math>{ \Gamma, x : A \vdash N : B \over \Gamma \vdash \lambda x : A . N : \Pi x : A . B }</math> (abs)
|-
| align="left" | <math>{ \Gamma \vdash N : A \quad A =_\beta A' \over \Gamma \vdash N : A' }</math> (conv)
|}

==== Parametriske regler ====
Følgende regel er parametrisk i <math> s_1, s_2 \in \{ *, \Box \}</math>. 

:<math>\Gamma \vdash A : s_1 \quad \Gamma, x : A \vdash B : s_2 \over \Gamma \vdash \Pi x:A.B : s_2 </math>

Man kan bestemme hvilket typesystem man ønsker ved å bestemme hvilke instanser av <math>(s_1, s_2)</math> man som er godtatt. Tabellen under lister opp alle mulighetene.
{| class="wikitable"
|-
!  !! ''Dependent'' typer !! Polymorfi !! Typeoperatorer !! Forkortelse !! Navn
|-
| <math>(*, *)</math> ||  ||  ||  || <math>\lambda^\to</math> || ''Simply typed lambda calculus''
|-
| <math>(*, *)</math> ||  ||  || <math>(\Box, \Box)</math> || <math>\lambda\underline\omega</math> || 
|-
| <math>(*, *)</math> ||  || <math>(\Box, *)</math> ||  || <math>\lambda 2</math> || ''System F''
|-
| <math>(*, *)</math> ||  || <math>(\Box, *)</math> || <math>(\Box, \Box)</math> || <math>\lambda\omega</math> || ''System F<math>\omega</math>''
|-
| <math>(*, *)</math> || <math>(*, \Box)</math> ||  ||  || <math>\lambda P</math> || LF (''Logical Framework'')
|-
| <math>(*, *)</math> || <math>(*, \Box)</math> ||  || <math>(\Box, \Box)</math> || <math>\lambda P \underline\omega</math> ||
|-
| <math>(*, *)</math> || <math>(*, \Box)</math> || <math>(\Box, *)</math> || || <math>\lambda P 2</math> || 
|-
| <math>(*, *)</math> || <math>(*, \Box)</math> || <math>(\Box, *)</math> || <math>(\Box, \Box)</math> || Coc, <math>\lambda C</math>, <math>\lambda P\omega</math> || ''Calculus of Construction''
|}


== Egenskaper ved typesystemer ==

To klassiske egenskaper som typesystemer kan ha er:
* Preservering (eng: ''subject reduction'' el. ''preservation''): hvis <math>\vdash e : \tau</math> og <math>e \to e'</math>, så <math>\vdash e' : \tau</math>. Altså, reduksjon bevarer typen.
* Progresjon (eng: ''progress''): hvis <math>\vdash e : \tau</math>, så er enten <math>e</math> en verdi, eller så eksisterer en <math>e'</math> slik at <math>e \to e'</math>. Altså, vel-typede termer henger ikke.

== Litteratur ==
* S. Abramsky / D. M. Gabbay / T. S. E. Maibaum / H. P. Barendregt (1993). "Handbook of Logic in Computer Science, volume II, chapter Lambda Calculi with Types"
* Jean-Yves Girard (1989). ''Proofs and Types'', Cambridge University Press. ISBN 0 521 37181 3. Tilgjengelig online: http://www.paultaylor.eu/stable/Proofs+Types.html
{{Autoritetsdata}}

[[Kategori:Logikk]]