Redigerer Lambdakalkyle (avsnitt)

== Omskrivningsregler ==
Termene vi definerte over har ikke blitt gitt noen formell mening. Historisk sett, så har det vært tre hovedregler som forteller hvordan man kan ''evaluere'' en term: 
alpha-konvertering (<math>\alpha</math>), beta-konvertering (<math>\beta</math>) og eta-ekspansjon (<math>\eta</math>).

Nedenfor vil forskjellige relasjoner bli definert, men disse vil kun gjelde for toppen av en term, og kan ikke brukes på deltermer. Anta derfor at vi har en relasjon <math>\rightarrow_R</math>
på termer, og vi kan så definere relasjonen <math>N \Rightarrow_R M</math> som følger:
* hvis <math>N \rightarrow_R M</math>, så <math>N \Rightarrow_R M</math>
* hvis <math>N \Rightarrow_R M</math>, så <math>\lambda x.\, N \Rightarrow_R \lambda x.\, M</math>
* hvis <math>M_1 \Rightarrow_R M_2</math>, så <math>N\,M_1 \Rightarrow_R N\, M_2</math>
* hvis <math>N_1 \Rightarrow_R N_2</math>, så <math>N_1\,M \Rightarrow_R N_2\, M</math>
Relasjonen <math>N \Rightarrow_R M</math> er dermed relasjonen som gjør ett <math>R</math>-steg på en del-term av <math>N</math>.

Fra en relasjon <math>M \Rightarrow_R</math> kan man definere relasjonen <math> M \Rightarrow^*_R N</math> som gjør null eller flere R-steg, som er den refleksive og transitive tillukningen av <math>\Rightarrow_R</math>.
Og videre kan man definere <math>M =_R N</math>, som er den refleksive, symmetriske, transitive tillukningen av <math>M \Rightarrow^*_R N</math>.

=== Alpha-konvertering ===
Intuisjonen vår rundt variabler er at ''navnet'' til en lokal variabel er irrelevant, funksjonene <math>x \mapsto x + 2</math> og <math>y \mapsto y + 2</math> representerer
''samme'' funksjon. Alpha-regelen gjør det at man kan bytte om lokale navn formelt.
:<math> \lambda x.\, M \to_\alpha \lambda y.\, M[y/x] </math>
gitt at <math>y</math> ikke forekommer fritt i <math>M</math>.

Med unntak av noen få, især de som jobber med implementasjoner av programmeringspråk, så er det vanlig å alltid jobbe med lambda-termer ''modulo'' alpha-ekvivalens,
altså på ekvivalensklasser av relasjonen <math>=_{\rightarrow\alpha} </math>.

=== Beta-reduksjon ===
Den viktigste regelen for lambdakalkylen er beta-reduksjon (<math>\beta</math>-redkusjon), som forteller hvordan en funksjon samhandler med et funksjonskall.
Å kalle på en funksjon <math>\lambda x.\, M</math> med et argument <math>N</math> betyr at man setter inn argumentet <math>N</math> for variabelen <math>x</math>
i kroppen, <math>M</math>, til funksjonen. Formelt skrives dette som:
:<math>(\lambda x. \, M) N \to_\beta M[N/x]</math>
hvor <math>M[N/x]</math> er substitusjon av <math>N</math> for <math>x</math> i <math>M</math>.

En term <math>M</math> er på beta normalform hvis det ikke finnes noen <math>N</math> slik at <math>M \Rightarrow_\beta N</math>, og
to termer <math>M</math> og <math>N</math> er beta-ekvivalente hvis <math>M =_\beta N</math>.

=== Eta-ekspansjon ===
Eta-ekspansjon handler om [[ekstensionalitet]], og sier at alle funksjoner beskrives ved hjelp av lambda-abstraksjon og applikasjon. Formelt er regelen
:<math> M \to_\eta \lambda x.\, M x</math>
hvor <math>x</math> ikke forekommer fritt i <math>M</math>.