
\section{What is λ-Calculus?}

\frame{\frametitle{\color{white} dummy}
  \begin{itemize}
    \item {\color{lightgray}What can Haskell do?}
    \item {What is λ-Calculus?}
    \item {\color{lightgray} Why Implement λ-Calculus?}
    \item {\color{lightgray} Let's Implement λ-Calculus}
    \item {\color{lightgray} Questions?}
    \item {\color{lightgray} References}
  \end{itemize}
}

\frame{\frametitle{What is λ-Calculus?}
\begin{itemize}
  \item[] {}
  \item[] {}
  \item[] {An important formal system}
  \item[] {for functional programming}
  \item[] {}
  \item[] {}
\end{itemize}
}

\subsection{Turing Machine}

\ftc{Turing Machine}

\ftc{by Alan Turing \\ in 1936}

\frame{
  \centering
  \includegraphics[width=1\textwidth]{image/turing-machine.png}
}

\frame{\frametitle{Turing Machine}
  \begin{itemize}
    \item<1->{\normalsize Infinite {\color{darkblue}tape} which stores symbols {\small(memory)}}
    \item<2->{\normalsize Finite {\color{darkblue}action table} which represents\\{\small (state, symbol) $\to$ action (program)}}
    \item<3->{\normalsize {\color{darkblue}Robotic arm} {\small (CPU with a register which stores current state)}
      \begin{itemize}
      \item<4->{\small Read the symbol on the tape at current position}
      \item<5->{\small Write a symbol on the tape at current position}
      \item<6->{\small Move the tape left or right}
      \end{itemize}
    }
  \end{itemize}
}

\ftc{Turing Complete}
\subsection{}
\ftc{So what is λ-calculus?}

\frame{\frametitle{Alligator Eggs!}
  \begin{figure}[h!]
    \centering
      \includegraphics[width=0.85\textwidth]{image/eating.png}
      \caption{\jref{http://worrydream.com/AlligatorEggs/}{http://worrydream.com/AlligatorEggs/}}
  \end{figure}
}

\ftc{by Alonzo Church \\ in 1930s}
\ftc{Also Turing complete}
\ftc{but why?}
\subsection{λ-Complete}
\ftc{Define λ-Complete}
\ftc{Whatever λ-calculus can do}
\frame{\frametitle{Implement Turing machine in λ-calculus}
  \hskip 7mm
  \centering
  \includegraphics[width=0.85\textwidth]{image/turing-machine-lambda.png}
}
\frame{\frametitle{λ-Complete}
\begin{itemize}
  \item<1->{\normalsize So λ-calculus can do anything TM can do}
  \item<2->{\normalsize Plus what λ-calculus can do without a TM}
  \item<3->{\normalsize Thus λ-calculus is Turing complete}
\end{itemize}
}
\ftc{On the other hand...}
\frame{\frametitle{Implement λ-calculus in Turing machine}
  \hskip 7mm
  \centering
  \includegraphics[width=0.85\textwidth]{image/lambda-turing-machine.png}
}
\ftc{So Turing machine is also λ-complete}
\frame{\frametitle{They have the same computability}
  \hskip 7mm
  \centering
  \includegraphics[width=0.85\textwidth]{image/inf.png}
}

\subsection{}

\frame{\frametitle{What exactly is λ-calculus?}
\begin{itemize}
  \item[]{}
  \item<1->{\usebeamerfont*{font DejaVu Sans Mono} (λx. x+1)}
  \item<2->{\usebeamerfont*{font DejaVu Sans Mono} (λx. x+1) 1}
  \item<3->{\usebeamerfont*{font DejaVu Sans Mono} = (1+1)}
  \item<4->{\usebeamerfont*{font DejaVu Sans Mono} = 2}
  \item[]{}
  \item[]{}
\end{itemize}
}

\frame{\frametitle{Does it look like Lisp?}
\begin{itemize}
  \item[]{}
  \item[]{}
  \item[]{\usebeamerfont*{font DejaVu Sans Mono} (λf.(λx.f (x x)) (λx.f (x x)))}
  \item[]{}
  \item[]{}
  \item[]{}
\end{itemize}
}

\subsection{Church Encoding}
\ftc{Church Encoding}

\frame{\frametitle{Natural Numbers}
\begin{itemize}
  \item[]{}
  \item{\usebeamerfont*{font DejaVu Sans Mono} 0 ≡ λf.λx. x}
  \item{\usebeamerfont*{font DejaVu Sans Mono} 1 ≡ λf.λx. f x}
  \item{\usebeamerfont*{font DejaVu Sans Mono} ...}
  \item{\usebeamerfont*{font DejaVu Sans Mono} n ≡ λf.λx. f$^{\text{n}}$ x}
  \item[]{}
\end{itemize}
}

\frame{\frametitle{Computation with Natural Numbers}
\begin{itemize}
  \item[]{}
  \item[]{}
  \item{\usebeamerfont*{font DejaVu Sans Mono} succ \ ≡ λn.λf.λx. f (n f x)}
  \item{\usebeamerfont*{font DejaVu Sans Mono} plus \ ≡ λm.λn.λf.λx. m f (n f x)}
  \item[]{}
  \item[]{}
\end{itemize}
}

\frame{\frametitle{Booleans}
\begin{itemize}
  \item[]{}
  \item[]{}
  \item{\usebeamerfont*{font DejaVu Sans Mono} true \ ≡ λa.λb. a}
  \item{\usebeamerfont*{font DejaVu Sans Mono} false ≡ λa.λb. b}
  \item[]{}
  \item[]{}
\end{itemize}
}

\frame{\frametitle{Computation with Booleans}
\begin{itemize}
  \item[]{}
  \item{\usebeamerfont*{font DejaVu Sans Mono} and \ \ ≡ λm.λn. m n m}
  \item{\usebeamerfont*{font DejaVu Sans Mono} or \ \ \ ≡ λm.λn. m m n}
  \item{\usebeamerfont*{font DejaVu Sans Mono} not \ \ ≡ λm.λa.λb. m b a}
  \item{\usebeamerfont*{font DejaVu Sans Mono} if \ \ \ ≡ λm.λa.λb. m a b}
  \item[]{}
\end{itemize}
}

\subsection{}

\frame{
\vskip 10mm%
\frametitlecenter{Recursion?\\No problems}
}

\subsection{Y combinator}

\frame{\frametitle{Y combinator}
\begin{itemize}
  \item[]{}
  \item<1->{Discovered by Haskell Curry}
  \item<1->{\normalsize\usebeamerfont*{font DejaVu Sans Mono} y \ \ = (λf.(λx.f (x x)) (λx.f (x x)))}
  \item<2->{\normalsize\usebeamerfont*{font DejaVu Sans Mono} y f = (λf.(λx.f (x x)) (λx.f (x x))) f}
  \item<3->{\normalsize\usebeamerfont*{font DejaVu Sans Mono} y f = f (y f)}
  \item[]{}
\end{itemize}
}

\frame{
\vskip 22mm%
\frametitlecenter{{\color{black} Paul Graham,}\\I know what is\\Y combinator!}
}

\subsection{Fixed Point Combinator}

\frame{\frametitle{Fixed Point Combinator}
\begin{itemize}
  \item[]{}
  \item{\normalsize Strict languages need some delay}
  \item{\footnotesize\usebeamerfont*{font DejaVu Sans Mono} Z = (λx.f (λv.((x x) v))) (λx.f (λv.((x x) v)))}
  \item{\normalsize Discovered by Alan Turing}
  \item{\footnotesize\usebeamerfont*{font DejaVu Sans Mono} Θ = (λx.λy. (y (x x y))) (λx.λy. (y (x x y)))}
  \item[]{}
\end{itemize}
}

\frame{\frametitle{Fixed Point Combinator}
\begin{itemize}
  \item[]{}
  \item{\normalsize Constructed by Jan Willem Klop}
  \item{\footnotesize\usebeamerfont*{font DejaVu Sans Mono} Yk = (L L L L L L L L L L L . . .)}
  \item[]{\tiny\usebeamerfont*{font DejaVu Sans Mono} where L = λabcdefghijklmnopqstuvwxyzr. (r (thisisafixedpointcombinator))}
  \item[]{}
  \item[]{}
\end{itemize}
}
