Lambdakalkyl

Från Wikipedia
Hoppa till: navigering, sök

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]

Idag är lambdakalkyl 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:

\lambda x.x
\lambda x.\lambda y.(y\ x)
(\lambda x.(y\ x) \lambda x.(u\ x))

[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 x,\ y,\ z. 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:

(x\ y)
(\lambda x.x^2)\ 5

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:

\lambda x.t\ 
\lambda x.(u\ x)

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 T_1 till λ-termen T_2 som T_1\ \xrightarrow[\alpha]{}\ T_2.

Rent formellt kan regeln beskrivas som: \lambda x.T_1 \to \lambda z.(\lambda x.T_1\ z)

Exempel på α-konvertering

(\lambda x.(u\ x)\ 4)\ \xrightarrow[\alpha]{}\ (\lambda z.(u\ z)\ 4)

Vidare säger man att två λ-termer, T_1 och T_2, är α-kongruenta om det finns en α-konvertering T_1\ \xrightarrow[\alpha]{}\ T_2 eller om T_1 = T_2. Detta betecknas T_1 \cong T_2

[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 (\lambda x.(u\ x)\ T_1)\ \xrightarrow[\beta]{}\ (u\ T_1). En term T_1 sägs vara β-konverterbar till T_2 om antingen T_1 kan β-reduceras till T_2 eller vice versa. Vi skriver detta som T_1\ \xrightarrow[\beta]{}\ T_2.

Exempel på β-reduktion

(\lambda x.(u\ x)\ 4)\ \xrightarrow[\beta]{}\ (u\ 4)

En λ-term som är på formen (\lambda x.T_1)\ T_2 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 (\lambda x.(x\ x)\ \lambda x.(x\ x))\ \xrightarrow[\beta]{}\ (\lambda x.(x\ x)\ \lambda x.(x\ x)), d.v.s. termen β-reduceras till sig själv.

Sats (Church-Rossers första sats): Om T\ \xrightarrow[\beta]{}\ U_1 och \ T\ \xrightarrow[\beta]{}\ U_2 så finns det en λ-term Z sådan att U_1\ \xrightarrow[\beta]{}\ Z och U_2\ \xrightarrow[\beta]{}\ Z

Följdsats: Om T\ \xrightarrow[\beta]{}\ U_1 och \ T\ \xrightarrow[\beta]{}\ U_2, där både U_1 och U_2 är på normalform så gäller att U_1 \cong U_2

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 \lambda x.f\ x 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 \left [ \mathbb{N} \times \mathbb{N} \to \mathbb{N} \right ]. Den kan vi då skriva om till en sekvens av funktioner med typen \left [ \mathbb{N} \to \left [\mathbb{N} \to \mathbb{N} \right ] \right ]. 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 \lambda x.\lambda y.((+\ x)\ y).

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

\text{true} \equiv \lambda t.\lambda f. t
\text{false} \equiv \lambda t.\lambda f. f

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

\text{and} \equiv \lambda a.\lambda b. a\ b\ false
\text{or} \equiv \lambda a. \lambda b. a\ true\ b
\text{not} \equiv \lambda a. a\ false\ true

Naturliga tal[redigera | redigera wikitext]

0 \equiv \lambda s.\lambda z. z
1 \equiv \lambda s.\lambda z. s\ z
2 \equiv \lambda s.\lambda z. s\ (s\ z)

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

\text{succ} \equiv \lambda m. \lambda s. \lambda z. s\ (m\ s\ z)
\text{plus} \equiv \lambda m. \lambda n. \lambda s. \lambda z. m\ s\ (n\ s\ z)
\text{times} \equiv \lambda m. \lambda n. m\ (plus\ n)\ 0

Källor[redigera | redigera wikitext]

  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