lambdakalkyle | lex.dk – Den Store Danske

Lambdakalkylen er en central matematisk beregningsmodel, der har haft stor betydning både i studiet af beregninger på ideelle computere og i studiet af matematisk logik. Den har også fundet anvendelser i filosofi, linguistik og design af programmeringssprog.

Lambdakalkylen er en notation til specifikation af funktioner med tilhørende regler for, hvordan en funktion anvendes på et argument. Lambdakalkylen blev oprindelig udviklet af bl.a. Alonzo Church i 1930 i forbindelse med studier af matematikkens logiske grundlag. I sin oprindelige form tillader lambdakalkylen logiske paradokser, hvilket blev bevist af Church og hans studerende J.B. Rosser i 1935. På grund af dette lavede Church to nye varianter af lambdakalkylen: En delmængde, der fungerer som model for beregninger (men ikke som model for matematisk logik), og en variant med et typesystem, der hindrer logiske paradokser, men som til gengæld kun kan modellere en begrænset del af matematisk logik.

Lambdakalkylen er en af de grundlæggende beregningsmodeller, der optræder som ækvivalente i Church-Turings tese om beregnelighed, og bruges derfor primært til at bevise egenskaber ved generelle beregninger.

Lambdakalkylen har givet inspiration til funktionsprogrammering, hvor værdier kan være funktioner, og hvor funktionsanvendelse er den primære beregningsmekaniske. Eksempelvis bruger programmeringssproget LISP fra 1958 en syntaks, der minder meget om notationen fra lambdakalkylen.

Modsat Turingmaskiner, der beskriver en beregning som en sekvens af modifikationer af en tilstand, så beskriver lambdakalkylen en beregning som reduktion af et udtryk, ligesom man i matematik forkorter et regneudtryk. Turingmaskiner har en simpel model for køretid, og bruges ofte til at studere beregningsmæssig kompleksitet af forskellige problemer. Lambdakalkylen har ikke nogen simpel model for køretid, så denne model bruges mest til at afgøre om et problem kan beregnes på en ideel computer og i mindre grad til at afgøre tidsforbruget af denne beregning. Endvidere bruges varianter af lambdakalkylen i matematisk logik. Det var til dette formål, at Church udviklede lambdakalkylen, men i den uindskrænkede form tillader lambdakalkylen logiske paradokser, så til brug i logik anvendes indskrænkede versioner af lambdakalkylen, blandt andet ved at påtrykke forskellige typesystemer, så en funktion kun tillader argumenter af en specificeret type. Dette svarer til løsningen på Russell's paradoks i mængdelære, hvor uindskrænket konstruktion af mængder ud fra prædikater giver lignende problemer. Den uindskrænkede version af lambdakalkylen fungerer dog fint som model for beregning, da den er vist ækvivalent med andre modeller for beregning såsom Turingmaskiner.

Lambda-udtryk

Lambdakalkylen arbejder med lambda-udtryk, som består af variabler, funktionsdefinitioner og funktionsanvendelser. En beregning sker ved at reducere et lambda-udtryk indtil det ikke kan reduceres mere. Lambdakalkylen skelner ikke mellem programmer og data, da begge repræsenteres som lambda-udtryk.

Syntaks

Et lambda-udtryk har en af tre følgende former:

En variabel, som angives ved et variabelnavn. Der er ikke nogen begrænsning på antallet af forskellige variabelnavne, så man kan til enhver tid finde et variabelnavn, der ikke allerede er i brug i et lambda-udtryk. Vi skriver et variabelnavn som et bogstav i kursiv, nogen gange suppleret med et indeks. Eksempler er x, y₁, og z.
En funktionsdefinition af formen (λx.e), hvor λ er det græske bogstav lambda, x er et variabelnavn og e er et lambda-udtryk. Intuitivt beskriver udtrykket (λx.e) en funktion, der tager en værdi v (som også er et lambda-udtryk) og beregner udtrykket e, hvor alle forekomster af x er erstattet med værdien v. Det er brugen af bogstavet λ, der har givet lambda-kalkylen sit navn. Bemærk, at den definerede funktion ikke har noget navn, derfor kalder man det ofte en anonym funktion.
En funktionsanvendelse af formen (e₁ e₂), hvor e₁ og e₂ er lambda-udtryk. Dette beregnes ved først at reducere e₁ til en funktionsdefinition og derefter anvende denne på værdien e₂, som beskrevet herover. Det er ikke altid muligt at reducere e₁ til en funktionsdefinition. I så fald kan funktionsanvendelsen heller ikke reduceres.

Forkortelser og parentesregler

Ligesom man i matematisk notation kan sætte og løfte parenteser, kan man også gøre dette i lambda-udtryk. Reglerne er

Udtrykket e₁ e₂ e₃ er ækvivalent med ((e₁ e₂) e₃). Man kan altså undvære parenteser omkring funktionsanvendelser, og hvis der er flere funktionsanvendelser efter hinanden, grupperes de fra venstre mod højre.
Udtrykket λx.e₁ e₂er ækvivalent med (λx.(e₁ e₂)). Man kan altså undvære parenteser omkring funktionsdefinitioner, og fuktionsanvendelse binder stærkere end funktionsdefinition.
Endvidere bruger man ofte λxy.e som forkortelse for λx.(λy.e).

Reduktionsregler

Beregning i lamdakalkylen sker ved hjælp af reduktioner, der bruger en simpel regel kaldet β-reduktion: Et redex (kort for reducable expression) er et udtryk af formen ((λx.e₁) e₂), og det reduceres til e₁[x\e₂], hvor e₁[x\e₂] betyder e₁, hvor alle forekomster af x erstattes af e₂.

Hvis e₁ indeholder deludtryk af formen (λx.e₃), skal forekomster af x i e₃ ikke erstattes af e₂, og hvis e₂ indeholder variablen y, giver det problemer at erstatte x med e₂ i et deludtryk af formen (λy.e₃), så erstatning af variabler med udtryk bruger særlige substitutionsregler, der viser, hvordan en substitution af en variabel x i et sammensat udtryk kan reduceres til substitution af variablen i deludtrykkene, indtil et deludtryk er en variabel, hvor den (hvis variablen er x) erstattes med det ønskede, eller (hvis variablen har et andet navn) bevares uændret.

x[x\e] → e
y[x\e] → y, hvis x≠y
(e₁ e₂)[x\e] → (e₁[x\e] e₂[x\e])
(λy.e₁)[x\e] → (λz.e₁[y\z][x\e]), hvor z er en ny variabel, der ikke bruges andre steder.

Et lambda-udtryk siges at være i normalform, hvis der ikke findes redexer i udtrykket. Hvis der er flere redexer i et lambda-udtryk er rækkefølgen i hvilken man reducerer disse ligegyldig, når blot man på et eller andet tidspunkt får reduceret alle redexer. Der er dog lambda-udtryk, der ikke kan reduceres til normalform, da enhver reduktion tilføjer mindst et nyt redex. Et eksempel på et lambda-udtryk, der ikke har en normalform, er udtrykket ((λx.(x x)) (λx.(x x))), som kaldes ω. Der er kun et redex, og det reducerer ω til ω selv. ω svarer til en uendelig løkke i et program.

Repræsentation af tal som lambdaudtryk

I teori om beregnelighed taler man i reglen om funktioner, der tager naturlige tal som inddata og giver naturlige tal som uddata. For at kunne sige noget om dem slags funktioner i lambdakalkylen, må man repræsentere tal som lambda-udtryk. Det gøres ofte med Church-tal:

Tallet 0 repræsenteres som (λf.(λx.x)).
Tallet 1 repræsenteres som (λf.(λx.(f x))).
Tallet 2 repræsenteres som (λf.(λx.(f (f x)))).
Tallet 3 repræsenteres som (λf.(λx.(f (f (f x))))).
Generelt repræsenteres tallet n som en funktionsdefinition, der tager to argumenter: En funktion f og en værdi x, og anvender f n gange på x.

Ved brug af denne repræsentation kan man definere funktioner, der lægger tal sammen, ganger tal med hinanden, osv. og dermed beregne alle beregnelige funktioner på tal.

Anvendt lambdakalkyle

Selv om man kan repræsentere tal og talberegninger i den rene lambdakalkyle, er det ikke specielt effektivt, så man udvider ofte lambdakalkylen men "almindelige" tal og operatorer, så man fx kan skrive funktionsdefinitioner som λx.x+1, som angiver en funktion, der lægger 1 til sit argument. Reduktion af sådanne udtryk sker med en kombination af β-reduktion og almindelige regneregler. Denne slags udvidelser af lambdakalkylen med konstanter og operatorer med deres egne reduktionsregler kaldes anvendt lambdakalkyle. Funktionsprogrammeringssprog som LISP er reelt anvendt lambdakalkyle, dog ofte med anderledes syntaks (bl.a. fordi symbolet λ ikke findes på et almindeligt tastatur).

Lambdakalkyle med typer

Lambdakalkylen som præsenteret herover egner sig ikke som fundament for logik, da den tillader logiske paradokser. Derfor begrænser man lambdakalkylen på forskellige måder, blandt andet ved at kræve at visse typeregler overholdes. I den simpleste udgave er typer af formen

En typevariabel, som skrives som et græsk bogstav, f.eks. α, eller
En funktionstype af formen (t₁→t₂), hvor t₁ og t₂ er typer. Den beskriver typen af funktioner, der tager argumenter af typen t₁ og giver resultater af typen t₂

Alle lambda-udtryk skal være veltypede, dvs. at det skal være muligt at give et udtryk en type ved hjælp af et sæt typeregler. Derudover skal alle variabler, der introduceres i funktionsdefinitioner eksplicit angive en type: Et udtryk, der i den normale lambdakalkyle skrives som λx.e skal i den typede lamdakalkyle skrives som λx:t.e, hvor t er en type. En funktionsdefinition λx:t.e vil have typen (t→t'), hvis e kan gives typen t' (under antagelsen om, at x har typen t). I en funktionsanvendelse (e₁e₂) skal e₁ kunne gives en type (t₁→t₂) og e₂ skal have typen t₁. Hele udtrykket har så typen t₂. Denne begrænsning betyder, at fx udtrykket ω (som ikke kan reduceres til en normalform) ikke kan gives en type. Faktisk vil ethvert veltypet lambda-udtryk kunne reduceres til en normalform.

Logisk set kan typen (t₁→t₂) betragtes som det logiske udsagn "t₁medfører t₂", og et lambda-udtryk af typen (t₁→t₂) betragtes som et bevis for dette udsagn i intuitionistisk logik.

Læs mere i Den Store Danske

Kommentarer

Kommentarer til artiklen bliver synlige for alle. Undlad at skrive følsomme oplysninger, for eksempel sundhedsoplysninger. Fagansvarlig eller redaktør svarer, når de kan.

Du skal være logget ind for at kommentere.

Fagansvarlig for Datalogi

Torben Ægidius Mogensen

Lektor, Københavns Universitet