Redigerer Lambdakalkyle (avsnitt)

=== Substitusjon ===
Substitusjon (eng: ''capture-avoiding substitution'') er et viktig begrep i lambdakalkylen. Formålet med substitusjon er å bytte ut en variabel i en term med en annen term.
For eksempel ønsker vi at det å bytte ut <math>x</math> med <math>10</math> i uttrykket <math>x + y</math> skal gi uttrykket <math>10 + y</math>.
I lambdakalkylen ønsker vi derfor å definere en funksjon <math>M[N/x]</math>,
som leses som ''bytt ut alle forekomster av <math>x</math> i <math>M</math> med <math>N</math>''.

En naiv, tekstelig substitusjon vil bli feil, fordi variabler som forekommer fritt i <math>N</math> kan bli bundet hvis <math>N</math> settes rett inn i <math>M</math>.
F.eks. vil <math>(\lambda x. y)[f x / y] \equiv \lambda x. f \, x</math> være ''feil'', siden den tidligere frie variabelen <math>x</math> i <math>f \, x</math> er blitt bundet 
i <math>\lambda x. \, f \, x</math>.

I litteraturen beskrives flere måter å håndtere dette på. Den letteste måten er å definere substitusjon som en [[partiell funksjon]] som ikke gir noe svar dersom det blir navnekræsj, på følgende måte:
* <math>x [ N / x] \equiv N </math>
* <math>y [ N / x] \equiv x</math> når <math>x</math> og <math>y</math> er forskjellige
* <math>(M_1 \, M_2) [N / x] \equiv M_1[N / x] \; M_2[N / x]</math>
* <math> (\lambda x.\, M) [N / x] = \lambda x.\, M </math>
* <math> (\lambda y.\, M) [N / x] = \lambda y. M [N / x] </math> gitt at <math> y \not\in \textrm{FV}(N)</math>

En korrekt, total funksjon, endrer den siste regelen til:
* <math> (\lambda y. \, M) [N / x] = \lambda y'. M[y' / y][N / x] </math> hvor <math>x</math>, <math>y</math> og <math>y'</math> er forskjellige, og <math>y' \not\in \mathrm{FV}(M) \cup \mathrm{FV}(N)</math>.