Från Rilpedia

Lambdakalkyl (λ-kalkyl) är i ett formellt system som skapades för att undersöka funktioner och rekursion. Lambdakalkylen utvecklades på 1920-talet av Alonzo Church. På 1960-talet förstod man att lambdakalkylen kunde användas för att förstå programspråk.

Det har därför blivit den matematiska grunden för funktionella programspråk.

Objekten i lambdakalkyl är termer (som ibland kallas lambdatermer). Det finns tre typer av termer

1. Variabler, x, y, z, ...
2. abstraktion, λx.t där t är en term
3. applikation, där t₁ och t₂ är termer

Abstraktion kan ses som definition av en funktion och applikation motsvarar tillämpning av en funktion.

På termerna använder man olika typer av reduktioner för att visa satser om lambdakalkylen. Lite förenklat är reduktionerna:

• α-reduktion - namnen på variblerna kan bytas
• β-reduktion - en term reduceras till termen t₂ som är termen t₁ med alla x utbytta mot s
• η-konvertering - termen konverteras till termen f

Churchkodning

För att använda lambdakalkyl för programspråk behöves bland annat tal och booleska värden. De finns inte i lambdakalkylen men de kan kodas med så kallad Churchkodning.

Booleska värden

true

false

Naturliga tal