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.
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.