\begin{slide}{Wiederholung: Operationale Semantik}

\newcommand{\tobe}{\to_{\beta}}

(SOS - small step operational semantics)

Ein-Schritt-Relation 
\begin{itemize}
\item $\beta$-Reduktion: $(\lambda x.M)N 
  \tobe M[x:=N] $
\end{itemize}
falls $\text{bound-vars}(M)$ 
und $\text{free-vars}(N)$
disjunkt.

bei Bedarf gebundene Var. umbenennen
\begin{itemize}
\item $\alpha$-Reduktion:
 $\lambda x.M \to_{\alpha} \lambda y.M[x:=y]$
\end{itemize}

Abschluß von $\tobe$ unter Kontexten:
\begin{itemize} \itemsep 0pt
\item $A_1 \tobe A_2 \Rightarrow 
  A_1 B \tobe A_2 B,
  B A_1 \tobe B A_2 ,
  \lambda x A_1 \tobe \lambda x A_2$
\end{itemize}

operationale Semantik ($=$ Programmausführung) \\
ist reflexive transitive Hülle $\tobe^*$
(Mehr-Schritt-Relation)

\end{slide}
