\newcommand{\FV}{\operatorname{FV}}

\begin{slide}{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.

\bigskip

(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)
\end{slide}
%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "~/edu/ws06/sym/folien/sym"
%%% End: 
