Lambda-kalkule

Lambda-kalkule er navnet på en række formalismer, der blev konstrueret af den amerikanske logiker Alonzo Church omkring 1940. Churchs oprindelige ærinde var at formulere en universel beregningsmodel (se Turings tese), men notationen er samtidig et bekvemt generelt redskab til håndtering af funktioner og benyttes i forskellige varianter i en række funktionsprogrammeringssprog.

Indeholder et udtryk en variabel, giver det anledning til en funktion, idet man for konkrete argumenter kan erstatte den variable med argumentet. For at markere dette indføres i traditionelle fremstillinger et navn for funktionen. Af udtrykket xa+b* markeres for eksempel ved f(a) = xa+b*, at det er a, som opfattes som variabel (og ikke x eller b), men samtidig har man indført navnet f for funktionen. Anvendes funktionen for eksempel på argumentet 3, får man f(3) = x3+b*.

Med lambda-notation skrives funktionen λ a.xa+b*, og man slipper derved for at give den navn. De to centrale operationer bliver "abstraktion": af et udtryk e at danne λ x.e, hvor x er bundet som funktionsvariabel, og dens modsætning "applikation": at anvende abstraktionen på et argument. I lambda-kalkule beregnes for eksempel applikationen (λ a.xa+b)(3)* til x3+b*.

Brugen af netop symbolet λ har en pudsig forklaring, idet der ikke refereres til noget sprogligt (selv om λ jo er et græsk l): I det store værk Principia Mathematica om matematikkens grundlag, som Alfred North Whitehead og Bertrand Russell udgav i årene 1910-13, brugte de en accent circonflexe for at markere abstraktion, som i â.xa+b*. Kunne man af typografiske grunde ikke sætte accenten ovenover, blev den placeret foran: Λ a.xa+b*, hvorved den kom til at ligne et stort græsk lambda Lambda, og Church brugte saa i stedet et lille lambda i sin afhandling.

I eksemplerne ovenfor har lambda-notation været blandet med talkonstanter (3) og aritmetiske operationer (+ og ), men både disse og alle andre nødvendige beregningselementer (betingelse, valg, gentagelse, dannelse af datastrukturer) kan i teorien repræsenteres i "ren" lambda-kalkule, hvor de eneste operationer er abstraktion og applikation. Tallene 0, 1, 2, 3, *ldots** kan for eksempel repræsenteres ved *λ f.λ x.x, λ f.λ x.f(x), λ f.λ x.f(f(x)), λ f.λ x.f(f(f(x))), ..., og man har også repræsentationer af +, *, true, false, if-then-else og så videre. I ren lambda-kalkule har man kun brug for to omskrivningsregler, som Church benævnte efter de to første bogstaver i det græske alfabet, nemlig alfa-konvertering: at omdøbe en bunden variabel (som ved omskrivning af λ f.λ x.f(x) til λ f.λ y.f(y)), og beta-reduktion: at erstatte en formel parameter med sin aktuelle værdi, det vil sige omskrive (λ x.udtryk)(---) til det, som fremkommer, når man i udtryk erstatter alle forekomster af x med ---.