Gebundene Umbenennungen

wir dürfen ($\lambda$x.B)A$\to$B[x : = A] nur ausführen, wenn x nicht in A frei vorkommt.

falls doch, müssen wir $\lambda$x.B in $\lambda$y.B[x : = y] umbenennen, wobei y weder in A frei noch in B überhaupt vorkommt.

(Beispiel) (Def. FV(t))

eine solche gebundene Umbenennung in einem Teilterm heißt $\alpha$-Konversion.

$\alpha$-konvertierbare Terme sind äquivalent (verhalten sich gleich bzgl. Ableitungen)

(Beispiel)

mit o.g. Bedingung ergibt sich eine vernünftige Relation $\to$ ($\beta$-Reduktion).

(Beispiel-Ableitungen)