Semantik des Lambda-Kalküls

Relation →_β auf Λ (ein Reduktionsschritt)

Es gilt t→_βt', falls

• ∃p∈Pos(t), so daß
• t[p] = (λx.B)A mit bvar(B)∩fvar(A) = ∅
• t' = t[p : = B[x : = A]]

  dabei bezeichnet B[x : = A] ein Kopie von B, bei der jedes freie Vorkommen von x durch A ersetzt ist

Ein (Teil-)Ausdruck der Form (λx.B)A heißt Redex.
    (Dort kann weitergerechnet werden.)

Ein Term ohne Redex heißt Normalform.
    (Normalformen sind Resultate von Rechnungen.)