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)


Johannes Waldmann 2007-01-30