\newcommand{\lift}{\operatorname{lift}}

\begin{slide}{Systematische Übersetzung}
Spezifikation:
  \begin{itemize}\itemsep 2pt
  \item Eingabe: geschlossener Lambda-Ausdruck $P$
  \item Ausgabe: äquivalenter Kombinator-Ausdruck $[P]$

    (Applikationen mit $S,K,I$;
    sonst keine Variablen und Lambdas)
  \end{itemize}
benutzt $[\lambda x.A] = \lift_x (A)$ 
mit Spezifikation: $\lift_x(A) x \to^* A$
\begin{itemize}\itemsep 2pt
\item $\lift_x(y) =$ falls $x=y$ dann $I$ sonst $K y$
\item $\lift_x(A B) = S \lift_x(A) \lift_x(B)$
\item $\lift_x(\lambda y.A) = \lift_x(\lift_y(A))$
\end{itemize}

Beispiele: $\lambda x.xx, \lambda xy.y, \lambda xy.yx$
--- Vereinfachungen?

\end{slide}
