Redigerer Typeteori (avsnitt)

== 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]]).