Redigerer Lambdakalkyle (avsnitt)

== Formell definisjon av termer ==
Termene til lambdakalkylen, i sin rene form, veldig enkle. Det er tre former for uttrykk: (1) variabler, (2) funksjoner, og (3) funksjonskall.
Termene kan beskrives med en grammatikk som:
:<math> N, M ::= x \mid N\, M \mid \lambda x.\, M</math>.
Hvor variablene <math>x</math> hentes fra mengden <math>\mathbb{V} = \{ x_1, x_2, \ldots \}</math>, og mengden av alle termer kalles <math>\Lambda</math>.
Termen <math>N\, M</math> representerer funksjonskall, hvor <math>N</math> er funksjonen, og <math>M</math> er argumentet. Dette skrives gjerne som <math>N(M)</math> i konvensjonell matte.
Termen <math>\lambda x.\, M</math> representerer en funksjon som tar ett argument og binder det til <math>x</math>,
for så å regne ut verdien til kroppen <math>M</math>. I konvensjonell matte kan man skrive dette som <math>x \mapsto M</math>. 
Termen <math>\lambda x.\, M</math> kalles ofte ''abstraksjon'' eller ''lambda-abstraksjon''.


I utgangspunktet kan en term <math> M_1 \, M_2 \, M_3</math> tolkes på ''to'' måter, <math>(M_1 \, M_2) M_3 </math> og <math> M_1 \, (M_2 \, M_3)</math>. 
Men det er standard konvensjoner som sier:
* Applikasjon binder mot venstre, altså skal <math> M_1 \, M_2 \, M_3</math> tolkes som <math>(M_1 \, M_2) \, M_3</math>.
* [[Skopet]] for [[abstraksjon]] binder så langt til høyre som mulig. For eksempel skal <math>\lambda x.\, M \, N</math> tolkes som <math>\lambda x.\, (M \, N)</math>.
* Flere etterfølgende <math>\lambda</math>-abstraksjoner slås sammen: f.eks. er <math>\lambda x \, y. M</math> en forkortelse for <math>\lambda x. \lambda y.\; M</math>.

==== Eksempler ====
Noen eksempler vi nå kan definere i den rene lambdakalkylen er:
* <math> \mathrm{id} \equiv \lambda x. \, x</math>, identitesfunksjonen
* <math> \mathrm{K} \equiv \lambda x\,y.\; x</math> og <math>\mathrm{S} \equiv \lambda x\, y \, z.\; x z (y z)</math> fra [[kombinatorisk logikk]].
* <math> \mathrm{to-ganger} \equiv \lambda f\, x.\; f (f x)</math> som tar en funksjon og et argument, og sender argumentet to ganger gjennom funksjonen.

Hvis vi beveger oss bort fra den rene lambdakalkylen og godtar konstanter for tall og operasjoner som pluss, kan vi definere funksjoner slik som:
* <math>\mathrm{f} \equiv \lambda x.\; x * 2</math>, som er funksjonen som tar et tall og ganger med to.
* <math>\mathrm{kvadrer} \equiv \lambda x.\; x * x</math>, som kvadrere et tall.

Det er viktig å merke seg at <math>\equiv</math> ikke er en del av den rene lambdakalkylen, men er bare ment for gi navn til termer i [[metaspråk|metaspråket]].

=== Fri- og bundede variable ===
Lambda-abstraksjoner ''binder'' en variabel i skopet sitt. F.eks. i <math>(\lambda x.\, x + 1) (x + 4)</math>, så bindes variablen <math>x</math> i termen <math>x + 1</math>,
men den bindes ikke i deltermen <math>(x + 4)</math> .
En variabel kan også forekommer fritt i en term: variabelen <math>y</math> er ''fri'' i termen <math>\lambda x.\; x + y</math>. En variabel kan både forekomme som
bundet og fri i en term, men en gitt variabel på en gitt lokasjon i en gitt term er enten fri eller bundet, ikke begge deler.

Funksjonen <math>\textrm{FV} : \Lambda \to 2^\mathbb{V}</math> gir mengden av frie variabler som forekommer i en term, og er definert rekursivt over strukturen til termer, som:
* <math> \textrm{FV}(x) = \{x\} </math>
* <math> \textrm{FV}(N \, M) = \textrm{FV}(N) \cup \textrm{FV}(M)</math>
* <math> \textrm{FV}(\lambda x.\, M) = \textrm{FV}(M) \setminus \{x\}</math>

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