Der Lambda-Kalkül

(Alonzo Church, 1936) Syntax:

• Variablen x, y,...
• Applikationen xx, (λx.xx)y
• Abstraktionen λx.xx, λx.(λy.x)

Begriffe: freie Variablen (FV), gebundene Variablen (BV), gebundene Umbenennung

Semantik: Ersetzung von Teiltermen:

• (λx.A)B→A[x/B]
• wobei $\mathsf {FV}$(B) disjunkt zu $\mathsf {BV}$(A)