Redigerer Lambdakalkyle

'''Lambdakalkulus''' eller '''lambdakalkylen'''{{trenger referanse}} (også kjent som <math>\lambda</math>-kalkylen) er et formelt system innenfor [[informatikk]], [[logikk]] og [[matematikk]] utviklet av [[Alonzo Church]] i 1930-årene.
Formålet var å undersøke fundamentet for matematikk, men [[Stephen Kleene]] og [[J.B. Rosser]] viste i 1935 at systemet er, logisk sett, inkonsistent.
I 1940 presenterte Alonzo Church et typesystem for lambdakalkylen som gir opphav til et konsistent system, men som begrenser beregnbarhetsstryket betraktelig.

Senere ble systemet forsket med som et fundament for beregninger, og [[Alan Turing]] viste i 1937 at lambdakalkylen er [[turingkomplett]]. I dag er det
i denne forbindelse den utypete lambdakalkylen er mest kjent. Se [[typeteori]] for typede varianter av lambdakalkylen.

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

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

== Egenskaper ved lambdakalkylen ==
Lambdakalkylen er [[konfluent]] under beta-reduksjon. Mer presist: for alle <math>M</math>, <math>M_1</math> og <math>M_2</math>, 
hvis <math>M \Rightarrow^*_\beta M_1</math> og <math>M \Rightarrow^*_\beta M_2</math>, så eksisterer en <math>N</math> slik
at <math>M_1 \Rightarrow^*_\beta N</math> og <math>M_2 \Rightarrow^*_\beta N</math>

Lambdakalkylen er hverken svakt eller sterkt normaliserende (eng: ''weakly'' og ''strongly normalizing''), ettersom 
f.eks. termen <math>(\lambda x. \, x\, x) (\lambda x.\, x \, x)</math> ikke har noen beta normalform.

== Koding av data ==
I den rene lambdakalkylen er det ingen data bortsett fra funksjoner. Det er likevel mulig å kode forskjellige datatyper som lambdatermer. 

=== Sannhetsverdier ===
De bolske verdiene ''sann'' og ''usann'' kan kodes som følger:
* <math>\mathrm{SANN} \equiv \lambda x\, y. \; x</math>
* <math>\mathrm{USANN} \equiv \lambda x\, y.\; y</math>
* <math>\mathrm{IF} \equiv \lambda b\, c\, a.\; b\; c\; a</math>
Vi kan se at dette fungerer ved å se på hvordan <math>\textrm{IF}\; \textrm{SANN}\; x\; y</math> 
reduserer til <math>x</math>:
:<math>\textrm{IF}\; \textrm{SANN}\; x\; y \Rightarrow^3_\beta \textrm{SANN}\; x\; y \Rightarrow^2_\beta x</math>.

=== Ordnede par ===
Et par <math>\langle M, N \rangle</math> sammen med to projeksjoner <math>\pi_1</math> og <math>\pi_2</math>
kan defineres slik at <math>\pi_1 \langle M, N \rangle =_\beta M</math> og <math>\pi_2 \langle M, N \rangle =_\beta N</math>.
* <math>\mathrm{PAIR} \equiv \lambda\,x\,y\,f.\; f \; x\; y</math>, hvor <math>\langle M, N \rangle </math> er en forkortelse for <math>\mathrm{PAIR}\; M \; N</math>.
* <math>\mathrm{\pi_1} \equiv \lambda p. \; (\lambda\; x \; y.\; x) \; p</math>
* <math>\mathrm{\pi_2} \equiv \lambda p. \; (\lambda\; x \; y.\; y) \; p</math>

=== Naturlige tall ===
I Churchs koding av [[Naturlig tall|naturlige tall]], så representeres et tall <math>n</math> som termen <math>\lambda\;f\;x.\; f^n x</math>, hvor
<math>f^n</math> er definert som <math>f^0 x  = x</math> og <math>f^{n+1} x = f (f^n x)</math>.
Intuisjonen er at tall <math>n</math> representeres ved en iterator som gitt en funksjon og et startverdi vil kalle på
funksjonen <math>n</math> ganger med startverdien.

Det er mulig å definere funksjoner slik som pluss, minus, gange, og relasjoner som sammenligner tall.

== Litteratur ==
* H. P. Barendregt. ''Lambda Calculus, Its Syntax and Semantics''.  North Holland, 1985. ISBN 0444875085.
{{Autoritetsdata}}

[[Kategori:Logikk]]
[[Kategori:Programmering]]