Lambdakalkyl

Lambdakalkyl (λ-kalkyl) är ett formellt system som skapades för att undersöka funktioner och rekursion. Lambdakalkyl utvecklades på 1930-talet av Alonzo Church, men fick sitt genombrott först efter 1969 då Dana Scott tagit fram den första konsistenta matematiska modellen för lambdakalkyl. Formella teorier för semantik i programspråk som baserades på lambdakalkyl hade innan dess ansetts som defekta då inga konsistenta matematiska modeller fanns.

Lambdakalkylen är den matematiska grunden för många funktionella programspråk, exempelvis Lisp.

Definition 
Lambdakalkyl består av så kallade λ-termer. En λ-term kan rekursivt beskrivas med följande grammatik (Backus-Naur-form):

 <λ-term>       ::=  <variabel>|<konstant>|<applikation>|<abstraktion>
 <applikation>  ::=  (<λ-term> <λ-term>)
 <abstraktion>  ::=  λ<variabel>.<λ-term>

Exempel på λ-termer enligt denna grammatik:

Variabler och konstanter  
Variabler och konstanter är de minsta beståndsdelarna i lambdakalkyl, även kallade atomer. Variabler identifieras oftast med bokstäver som till exempel . En konstant kan vara till exempel siffran 3.

Applikationer 
En applikation applicerar en λ-term på en annan λ-term. Den första av dessa två kallas för operator och den andra för operand. Detta kan likställas med ett funktionsanrop i ett vanligt programmeringsspråk. I lambdakalkylen kan alla λ-termer användas som både operatorer och operander. 
För att uttrycka en applikation skriver man två λ-termer separerade med ett mellanrum. Vill man vara tydlig kan man omge dem med parenteser.
 
Exempel på applikation:

Abstraktioner 
En abstraktion binder en variabel i en λ-term i syfte att skapa en funktion från λ-termen. Den genererade funktionen tar endast ett argument. Vill man ha fler argument får man använda sig av s.k. currying. Man kan jämföra en abstraktion med en funktionsdefinition i ett vanligt programmeringsspråk. 
Själva uttrycket för en abstraktion är tecknet λ direkt följt av ett variabelnamn och sedan en punkt som mellan variabelnamnet och en λ-term. λ-tecknet säger att variabeln kommer att vara bundet till ett värde i den följande λ-termen.

Exempel på abstraktion:

Regler

α-konvertering 
Denna konvertering innebär att vi kan byta namn på en bunden variabel i en λ-term förutsatt att det nya namnet inte redan används i λ-termen. Vi uttrycker detta namnbyte (α-konvertering) från λ-termen  till λ-termen  som .
    
Rent formellt kan regeln beskrivas som: 

Exempel på α-konvertering
 

Vidare säger man att två λ-termer,  och , är α-kongruenta om det finns en α-konvertering  eller om . Detta betecknas

β-reduktion 
En β-reduktion innebär att vi substituerar en bunden variabel i en λ-term med den λ-term som applicerats på den första. Till exempel .
En term  sägs vara β-konverterbar till  om antingen  kan β-reduceras till  eller vice versa. Vi skriver detta som .

Exempel på β-reduktion
 

En λ-term som är på formen  kallas för en β-redex, från engelskans β-reducible expression. Vidare sägs en λ-term vara på normalform om inga β-redex finns i termen. Notera dock att inte alla λ-termer kan skrivas på detta sätt. Till exempel , d.v.s. termen β-reduceras till sig själv.

Sats (Church-Rossers första sats): Om  och  så finns det en λ-term  sådan att  och 

Följdsats: Om  och , där både  och  är på normalform så gäller att 

Det vill säga varje λ-term har en unik normalform (under α-kongruens), förutsatt att den har en normalform överhuvudtaget.

η-konvertering 
Termen  konverteras till termen f

Currying 
Currying är ett sätt att beskriva en funktion som tar flera argument som en sekvens av funktioner som tar ett argument. Rent matematiskt kan man se det som att om vi har funktionen addition av heltal, så har den typen . Den kan vi då skriva om till en sekvens av funktioner med typen . D.v.s. den första funktionen tar ett argument och returnerar en ny funktion som också tar ett argument. Den här metoden användes flitigt av Haskell B. Curry, som också har givit den dess namn.

Så exempelvis addition skulle representeras i lambdakalkyl som .

Churchkodning 
För att använda lambdakalkyl för programspråk behöves bland annat tal och booleska värden. De finns inte i lambdakalkyl men de kan kodas med så kallad Churchkodning.

Booleska värden 

Givet dessa definitioner kan man sedan definiera elementära funktioner som arbetar med booleska värden.

Naturliga tal 

Givet ovanstående induktiva definition kan man definiera elementära aritmetiska operationer.

Källor/Litteraturförteckning 
Introduction to the Theory of Programming Languages  av  Bertrand Meyer 

Teoretisk datalogi