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:

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

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

$(x\ y)$

$(\lambda x.x^{2})\ 5$

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:

$\lambda x.t\$

$\lambda x.(u\ x)$

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 $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}$

β-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 $(\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.

η-konvertering

Termen $\lambda x.f\ x$ 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 $\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)$.

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

${\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

$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/Litteraturförteckning

• Introduction to the Theory of Programming Languages av Bertrand Meyer