Lambda-Kalkül
Formales Berechnungsmodell. Alonzo Church, 1930er Jahre. Drei Grundregeln: Variablen, Abstraktion (λx.Rumpf), Applikation (f x). Turing-vollständig — kann alles berechnen, was ein Computer berechnen kann.
Grundlage der funktionalen Programmierung. Currying (einstellige Funktionen, die wieder Funktionen zurückgeben) ist nach Haskell Curry benannt. Der Y-Kombinator ermöglicht Rekursion ohne benannte Funktionen. Getypte Lambda-Kalküle (Simply Typed → System F → Calculus of Constructions) führten zu Haskell, ML, Coq, Agda, Lean. Funktionale Programmierung ist eine direkte Erbin. Die Church-Turing-These besagt, dass Lambda-Kalkül und Turingmaschinen dieselbe Berechenbarkeitsklasse ausdrücken.