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 1969Dana 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.[1]

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

Definition

redigera

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:

 
 
 

[2]

Variabler och konstanter

redigera

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

redigera

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

redigera

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:

 
 

α-konvertering

redigera

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  

[3]

β-reduktion

redigera

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.

[4]

η-konvertering

redigera

Termen   konverteras till termen f

Currying

redigera

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  .

[5]

Churchkodning

redigera

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

redigera
 
 

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

 
 
 

Naturliga tal

redigera
 
 
 

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

 
 
 

Källor/Litteraturförteckning

redigera
  • Introduction to the Theory of Programming Languages av Bertrand Meyer
  1. ^ Revesz, G: Lambda-Calculus, Combinators, and Functional Programming, sidan vii. Cambridge University Press, 1988
  2. ^ Revesz, G: Lambda-Calculus, Combinators, and Functional Programming, sidan 16. Cambridge University Press, 1988
  3. ^ Revesz, G: Lambda-Calculus, Combinators, and Functional Programming, sidan 20. Cambridge University Press, 1988
  4. ^ Revesz, G: Lambda-Calculus, Combinators, and Functional Programming, sidan 23. Cambridge University Press, 1988
  5. ^ Revesz, G: Lambda-Calculus, Combinators, and Functional Programming, sidan 13. Cambridge University Press, 1988