Vad är det som gör λ-kalkylen så intressant?
Det kan man fråga sig.
Lambda-kalkylen är Turingmaskinens funktionella motsvarighet. Till skillnad från en TM har λ inget tillstånd, utan endast funktionabstraktion och applikation. Det som är fascinerande är att λ är lika kraftfull som en TM.
En snabb introduktion
Observera att detta bara är en snabb intro som förutsätter att man använt sig av lambdafunktioner t.ex. i Haskell. Jag går inte in på formella detaljer här, utan listar bara några grundidéer informellt.
λx.x definierar identitetsfunktionen anonymt. Den tar ett x och ger tillbaka samma x.
Vill vi nu använda vår funktion måste vi skriva ut den (den är ju anonym), så här:
(λx.x) b applicerar funktionen på argumentet b, vilket i detta fall innebär att x byts ut mot b.
Substitution brukar allmänt skrivas E[V := E'], vilket innebär ersättning av variabeln V med E’ där den är fri i E.
Det finns en regel som uttrycker funktionsanvändning, kallad β-reduktion, som ser ut som följer:
β-reduktionen av ((λ V. E) E′) är E[V := E′]. Detta uttrycker den intuitiva substitutionsprincipen.
Tal kan definieras som följer:
0 := λ f x. x
1 := λ f x. f x
2 := λ f x. f (f x)
…
Man kan tänka sig detta som en högre ordningens funktion med två argument, där man upprepade gånger applicerar det ena argumentet på det andra, alltså åstadkommer man något slags uppräkning. Man kan nu definiera ’succ’ och ‘pred’ funktioner, och på den vägen är det.
Fortsättning följer…
