Lambdakalkyl

Från Wikipedia

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 | redigera wikitext]

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 | redigera wikitext]

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 | redigera wikitext]

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 | redigera wikitext]

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[redigera | redigera wikitext]

α-konvertering[redigera | redigera wikitext]

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 | redigera wikitext]

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 | redigera wikitext]

Termen konverteras till termen f

Currying[redigera | redigera wikitext]

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 | redigera wikitext]

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 | redigera wikitext]

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

Naturliga tal[redigera | redigera wikitext]

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

Källor/Litteraturförteckning[redigera | redigera wikitext]

  • 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