\begin{slide}{Small-Step-Semantik des Lambda-Kalküls}

Basis-Operation ist $A[x/B]$: 

ersetze jedes freie Vorkommen von $x$ in $A$ durch $B$

  \begin{itemize}
  \item $\beta$-Konversion: 

    $(\lambda x.A)B \to_\beta A[x/B]$

    wobei $\mathsf{FV}(B)$ disjunkt zu $\mathsf{BV}(A)$ 

  \item $\alpha$-Konversion: gebundene Umbenennung

    $(\lambda x.A) \to_\alpha (\lambda y.A[x/y])$
  \end{itemize}
\dots und Abschluß unter Kontext (Inferenz-System?)

Bemerkungen:
\begin{itemize}
\item warum ist die Bedingung bei $\to_\beta$ nötig? (Beispiele)
\end{itemize}



\end{slide}
