Redigerer Typeteori (avsnitt)

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