3-lambda.tex

\section{Der $\lambda$-Kalkül}

\begin{frame}{Der $\lambda$-Kalkül}
	\begin{itemize}
		\item Programmierlogik
		\item wichtige Grundlage für Programmiersprache
		\item Weite Verbreitung in der Lehre (KIT 5. Semester)
		\item Beispiel: $(\lambda x.\lambda y.x) (\lambda y.y)$
	\end{itemize}
\end{frame}

\begin{frame}[<+->]{Der $\lambda$-Kalkül}
	Visualisierung von Bret Victor:
	\begin{center}
		\begin{tabular}{rcl}
			\raisebox{-.5\height}{\includegraphics[height=1.cm]{media/egg_blank}}
			& $\Leftrightarrow$ &
			$x$
			\\[1cm]
			\raisebox{-.5\height}{\includegraphics[height=1.cm]{media/alligator_blank}}
			& $\Leftrightarrow$ &
			$\lambda x.$
		\end{tabular}
	\end{center}
\end{frame}

\begin{frame}{Die $\beta$-Reduktion}
	\begin{center}
		\begin{tabular}{lccl}
			&
			\raisebox{-.5\height}{
				\begin{tabular}{cc}
					\tikz[remember picture] \node(a) {
						\includegraphics[height=1.cm]{media/alligator_green}
					};
					&
					\tikz[remember picture] \node(b) {
						\includegraphics[height=.75cm]{media/egg_yellow}
					};
					\\
					\includegraphics[height=.75cm]{media/egg_green}
				\end{tabular}
				\begin{tikzpicture}[remember picture,overlay]
					\draw<2->[<-,thick,bend left=45] 
						($(a.east)+(-0.5,-0.1)$) to node[auto, swap] {}($(b.west)+(0.1,0)$);
				\end{tikzpicture}
			}
			& $\Leftrightarrow$ &
			$(\lambda x.x) y$
			
			\\[2cm]
			% SLIDE 3
			\action<3->{
				$\Rightarrow$
				&
				\visible<3->{
					\raisebox{-.5\height}{
						\parbox{3cm}{
							\begin{center}
								\begin{turn}{180}
									\includegraphics[height=1.cm]{media/alligator_green}
								\end{turn}
								\\
								\includegraphics[height=.75cm]{media/egg_yellow}
							\end{center}
						}
					}
				}
				& $\Leftrightarrow$ &
				$\cancel{\lambda x.}y$
			}
			
			\\[2cm]
			% SLIDE 4
			\action<4->{
				$\Rightarrow$
				&
				\visible<4->{\includegraphics[height=.75cm]{media/egg_yellow}}
				& $\Leftrightarrow$ &
				$y$
			}
		\end{tabular}
	\end{center}
\end{frame}