lambda-calc-cofc-2019.tex

\documentclass{beamer}

\usetheme{Warsaw}

\definecolor{Indigo}{rgb}{0.18000, 0.00000, 0.50000}
\definecolor{jaredBG}{rgb}{0.00000, 0.00000, 0.50000}

\usecolortheme[named=Indigo]{structure}
\setbeamercolor*{block title example}{fg=white, bg=jaredBG}

\newcommand{\vs}{\\~\\}
\newcommand{\redexL}[1]{{\color{red} #1}}
\newcommand{\redexR}[1]{{\color{blue} #1}}

\title[Introduction to the Lambda Calculus]{Introduction to the Lambda Calculus}
\author[]{Jared Corduan}
\date{November 5, 2019}

\usepackage{verbatim}
\usepackage{graphicx}
\usepackage{tikz-cd}
\usepackage{tikzsymbols}

\tikzset{
  invisible/.style={opacity=0},
  visible on/.style={alt={#1{}{invisible}}},
  alt/.code args={<#1>#2#3}{%
    \alt<#1>{\pgfkeysalso{#2}}{\pgfkeysalso{#3}}%
  }
}

\begin{document}

\begin{frame}
  \titlepage
\end{frame}

\begin{frame}
  These slides are available at:
  \url{https://github.com/JaredCorduan/lambda-calc-cofc}
\end{frame}

\begin{frame}{models of computation}
  What is a computation?

  \begin{itemize}
    \item $\lambda$-calculus (1935, Church)
    \item $\mu$-recursive functions (1935, G\"odel)
    \item Post machines (1936, Post)
    \item Turing machines (1936, Turing)
    \item flow charts (1947, Goldstine and Von Neumann)
    \item register machines (1963, Shepherdson and Sturgis)
  \end{itemize}
\end{frame}

\begin{frame}{formalization}
  \begin{itemize}
    \item Babylonian division algorithms date 2500 BC
    \item strong intuition
    \item why the 1930's?
  \end{itemize}
\end{frame}

\begin{frame}{Explosion of Math in the 1800's}
  \begin{itemize}
    \item explosion of mathematics in the nineteenth century
    \item more abstract, less attached to the sciences
    \item nonconstructive proofs
    \item rise of first order logic via Frege and Peirce.
  \end{itemize}
\end{frame}

\begin{frame}{What is a good foundation for mathematics?}
  \begin{itemize}
    \item potential infinity vs actual infinity
    \item sets or functions?
    \item types?
    \item What constitutes a proof?
    \item What is an algorithm?
  \end{itemize}
\end{frame}

\begin{frame}{Pricipia}
  \begin{itemize}
    \item Pricipia Mathematica, by Alfred North Whitehead and Bertrand Russell in 1910
    \item Church introduces the lambda calculus
    \item entscheidungsproblem in 1935.
  \end{itemize}
\end{frame}

\begin{frame}{Influence on programming languages}
  \begin{itemize}
    \item Lisp
    \item ALGOL 60
    \item ML
    \item Haskell
  \end{itemize}
\end{frame}

\begin{frame}{Lambda Calculus}
  In math class, you might see
  $$f(x, y) = x^2+y$$
  $$f(1, 2) = 1^2+2$$
  \uncover<2->{
  Or
  $$x,y \mapsto x^2+y$$
  $$1,2 \mapsto 1^2+2$$
  $$1 \mapsto 1^2+y$$
  }
  \uncover<3->{
  Consider the lambda notation:
  $$\lambda x.\lambda y. x^2+y$$
  $$(\lambda x.\lambda y. x^2+y)(1)=\lambda y.1^2+y$$
  $$(\lambda y. 1^2+y)(2)=1^2+2$$
  }
\end{frame}

\begin{frame}{Lambda Terms}
  Lambda Terms build up from:
  \begin{itemize}
    \item variables: $x$, $y$, $f$, \Coffeecup, etc
    \item abstraction: $\lambda x. M$, for a term $M$.
    \item application $MN$, for terms $M$ and $N$.
  \end{itemize}
  \uncover<2>{
    Examples:\\
    \begin{math}
      \begin{array}{rcl}
          I & = & \lambda x. x \\
          I & = & \lambda \Coffeecup. \Coffeecup \\
          K & = & \lambda x. \lambda y. x \\
          S & = & \lambda x.\lambda y. \lambda z.xz(yz) \\
          \Omega & = & (\lambda x. xx)(\lambda x. xx) \\
          Y & = & \lambda f.(\lambda x.f(xx))(\lambda x.f(xx)) \\
      \end{array}
    \end{math}
  }
\end{frame}

\begin{frame}{Substitution:}
    Substitute $N$ for $x$ in $M$:

    $$M[x:=N]$$
  \uncover<2->{
    $$x\Strichmaxerl{x}[x:=\Coffeecup]~=~
  }
  \uncover<3->{
    \Coffeecup\Strichmaxerl\Coffeecup$$
  }
  \uncover<4->{
    \vs
    Caveat emptor:
    care is needed to define capture-avoiding substitution,
    to avoid things like
    $$(\lambda y.x)[y:=x]=\lambda x.x$$
  }
\end{frame}

\begin{frame}{Reducible Expressions}
  A ``reducible expression" or ``redex" is a term of the form:
  $$(\lambda x.M)N$$

  \uncover<2->{
    $\beta-$reduction:

    $$(\lambda x.M)N\to_\beta M[x:=N]$$
  }
  \uncover<3->{
    $$(\lambda x.x\Strichmaxerl{x})~\Coffeecup~~\to_\beta~~
  }
  \uncover<4->{
    \Coffeecup~\Strichmaxerl~\Coffeecup$$
  }
\end{frame}

\begin{frame}{Examples}
  \begin{center}
    \begin{math}
      \begin{array}{rcl}
        \only<1,4->{
          SKK & = & (\lambda x.\lambda y. \lambda z.xz(yz))
                  (\lambda a. \lambda b. a)
                  (\lambda c. \lambda d. c) \\
          }
        \only<2,3>{
          SKK & = & \redexL{(\lambda x.\lambda y. \lambda z.xz(yz))}
                  \redexR{(\lambda a. \lambda b. a)}
                  (\lambda c. \lambda d. c) \\
          }
        \only<3>{
            & \to_\beta
            & \redexL{\lambda y. \lambda z.}\redexR{(\lambda a. \lambda b. a)}\redexL{z(yz)}
              (\lambda c. \lambda d. c) \\
        }
        \only<4,8->{
            & \to_\beta
            & \lambda y. \lambda z.(\lambda a. \lambda b. a)z(yz)(\lambda c. \lambda d. c) \\
        }
        \only<5>{
            & \to_\beta
            & \lambda y. \lambda z.\redexL{(\lambda a. \lambda b. a)}\redexR{z(yz)}
              (\lambda c. \lambda d. c) \\
        }
        \only<6,7>{
            & \to_\beta
            & \redexL{\lambda y. \lambda z.(\lambda a. \lambda b. a)z(yz)}
              \redexR{(\lambda c. \lambda d. c)} \\
        }
        \only<7>{
            & \to_\beta
            & \redexL{\lambda z.(\lambda a. \lambda b. a)z(}
              \redexR{(\lambda c. \lambda d. c)}\redexL{z)} \\
        }
        \only<8,10->{
            & \to_\beta
            & \lambda z.(\lambda a. \lambda b. a)z
              ((\lambda c. \lambda d. c)z) \\
        }
        \only<9>{
            & \to_\beta
            & \lambda z.\redexL{(\lambda a. \lambda b. a)}\redexR{z}
              ((\lambda c. \lambda d. c)z) \\
        }
        \only<9,11->{
            & \to_\beta & \lambda z.(\lambda b. z)((\lambda c. \lambda d. c)z) \\
        }
        \only<10>{
            & \to_\beta
            & \lambda z.(\lambda b. z)(\redexL{(\lambda c. \lambda d. c)}\redexR{z}) \\
        }
        \only<10,12->{
            & \to_\beta & \lambda z.(\lambda b. z)(\lambda d. z) \\
        }
        \only<11>{
            & \to_\beta & \lambda z.\redexL{(\lambda b. z)}\redexR{(\lambda d. z)} \\
        }
        \only<11->{
            & \to_\beta & \lambda z.z \\
        }
        \only<12->{
            & = & I \\
        }
      \end{array}
    \end{math}
  \end{center}
\end{frame}

\begin{frame}{Examples}
  \begin{center}
    \begin{math}
      \begin{array}{rcl}
        \Omega & = & (\lambda x. xx)(\lambda x. xx) \\
        \uncover<2>{
               & \to_\beta & (\lambda x. xx)(\lambda x. xx)
        }
      \end{array}
    \end{math}
  \end{center}
\end{frame}

\begin{frame}{Arithmetic in the Lambda Calculus}
  \begin{itemize}
    \item $0 := \lambda f.\lambda x. x$
    \item $1 := \lambda f.\lambda x. fx$
    \item $2 := \lambda f.\lambda x. f(fx)$
  \end{itemize}
  \begin{itemize}
    \item $\mathsf{SUCC} := \lambda n.\lambda f.\lambda x. f(n f x)$
    \item $\mathsf{PLUS} := \lambda m.\lambda n.\lambda f.\lambda x. m f (n f x)$
  \end{itemize}
\end{frame}

\begin{frame}{One plus one is two!}
  \begin{center}
    \begin{math}
      \begin{array}{rcl}
        \mathsf{PLUS}~1~1
          & =
          & (\lambda m.\lambda n.\lambda f.\lambda x. m f (n f x))
              (\lambda g.\lambda y. gy)
              (\lambda h.\lambda z. hz) \\
        \uncover<2->{
          & \to_\beta
          & (\lambda n.\lambda f.\lambda x. (\lambda g.\lambda y. gy)f(n f x))
              (\lambda h.\lambda z. hz) \\
          }
        \uncover<3->{
          & \to_\beta
          & \lambda f.\lambda x. (\lambda g.\lambda y. gy)f((\lambda h.\lambda z. hz) f x) \\
          }
        \uncover<4->{
          & \to_\beta
          & \lambda f.\lambda x. (\lambda y. fy)((\lambda h.\lambda z. hz) f x) \\
          }
        \uncover<5->{
          & \to_\beta
          & \lambda f.\lambda x. f((\lambda h.\lambda z. hz) f x) \\
          }
        \uncover<6->{
          & \to_\beta
          & \lambda f.\lambda x. f((\lambda z. fz) x) \\
          }
        \uncover<7->{
          & \to_\beta
          & \lambda f.\lambda x. f(f x) \\
          }
        \uncover<8->{
          & =
          & 2
          }
      \end{array}
    \end{math}
  \end{center}
\end{frame}

\begin{frame}{Examples}
  \begin{center}
    \begin{math}
      \begin{array}{rcl}
        Y & = & \lambda f.(\lambda x.f(xx))(\lambda x.f(xx)) \\
        \uncover<2->{
        \\
        YF & = & (\lambda f.(\lambda x.f(xx))(\lambda x.f(xx)))F \\
           & \to_\beta & (\lambda x.F(xx))(\lambda x.F(xx)) \\
           & \to_\beta & F((\lambda x.F(xx))(\lambda x.F(xx))) \\
        }
        \uncover<3->{
        \\
        F(YF) & = & (\lambda f.(\lambda x.f(xx))(\lambda x.f(xx)))F \\
              & \to_\beta & F((\lambda x.F(xx))(\lambda x.F(xx))) \\
        }
        \uncover<4->{
        \\
        YF & \sim_\beta & F(YF)
        }
      \end{array}
    \end{math}
  \end{center}
\end{frame}

\begin{frame}{Factorial!}
  \begin{math}
  \end{math}
  \\
  \begin{center}
    \begin{math}
      \begin{array}{rcl}
        7! & = & 7\cdot 6\cdot 5\cdot 4\cdot 3\cdot 2\cdot 1
        \\
        \\
        \\
        \uncover<2->{
        \mathsf{fact}~n
        & =
        & \begin{cases}
            1 & n = 0 \\
            n\cdot\mathsf{fact}(n-1) & \text{otherwise}
          \end{cases}
        \\
        \\
        \\
        }
        \uncover<3->{
        \mathsf{F}~f~n
          & =
          & \mathsf{ite}~(\mathsf{isZero}~n)~\mathsf{one}~(\mathsf{mul}~n~(f(\mathsf{pred}~n)))
          \\
        }
        \uncover<4->{
        \mathsf{fact}
          & =
          & YF
          \\
        }
        \uncover<5->{
        \mathsf{fact}~n
          & =
          & YFn
          \\
        }
        \uncover<6->{
          & \sim_\beta
          & F(YF)n
          \\
        }
        \uncover<7->{
          & =
          & \mathsf{ite}~(\mathsf{isZero}~n)~\mathsf{one}~(\mathsf{mul}~n~(YF(\mathsf{pred}~n)))
        }
        \uncover<8->{
          \\
          & =
          & \mathsf{ite}~(\mathsf{isZero}~n)~\mathsf{one}~(\mathsf{mul}~n~(fact(\mathsf{pred}~n)))
        }
      \end{array}
    \end{math}
  \end{center}
\end{frame}

\begin{frame}{Logic in the Lambda Calculus}
  \begin{itemize}
    \item $\mathsf{true} := \lambda x.\lambda y. x$
    \item $\mathsf{false} := \lambda x.\lambda y. y$
    \item $\mathsf{and} := \lambda p.\lambda q. pqp$
    \item $\mathsf{or} := \lambda p.\lambda q. ppq$
    \item $\mathsf{not} := \lambda p.p~\mathsf{false}~\mathsf{true}$
    \item $\mathsf{ite} := \lambda p.\lambda a.\lambda b.p a b$
  \end{itemize}
  \uncover<2->{
  Example:
  \begin{center}
    \begin{math}
      \begin{array}{rcl}
        \mathsf{and}~\mathsf{true}~\mathsf{false}
          & =
          & (\lambda p.\lambda q. pqp)(\lambda x.\lambda y. x)(\lambda w.\lambda z. z) \\
        }
        \uncover<3->{
          & \to_\beta
          & (\lambda q. (\lambda x.\lambda y. x)q(\lambda x.\lambda y. x))
            (\lambda w.\lambda z. z) \\
          }
        \uncover<4->{
          & \to_\beta
          & (\lambda x.\lambda y. x)(\lambda w.\lambda z. z)(\lambda x.\lambda y. x) \\
          }
        \uncover<5->{
          & \to_\beta
          & (\lambda y. \lambda w.\lambda z. z)(\lambda x.\lambda y. x) \\
          }
        \uncover<6->{
          & \to_\beta
          & \lambda w.\lambda z. z \\
          }
        \uncover<7->{
          & =
          & \mathsf{false}
          }
      \end{array}
    \end{math}
  \end{center}
\end{frame}

\begin{frame}{Normal Form}
  An lambda expression without a redex is called a \textbf{normal form}.
  \begin{itemize}
    \item We know they do not always exist (such as with $\Omega$).
    \item Are they unique?
    \item Does it matter how you chose each redex?
  \end{itemize}
\end{frame}

\begin{frame}[fragile]{Church-Rosser}
  \begin{theorem}
    Given terms $X$, $Y_1$, and $Y_2$ such that:
    \[
      \begin{tikzcd}
        X \arrow[r, two heads] \arrow[d, two heads]
      & Y_1 \arrow[visible on=<2->, d, two heads] \\
      Y_2 \arrow[visible on=<2->, r, two heads]
      & {\uncover<2->{Z}}
      \end{tikzcd}
    \]
    \uncover<2->{There exists a $Z$ as above.}
  \end{theorem}
  \uncover<3>{
  \begin{corollary}
    Normal forms are unique when they exist.
  \end{corollary}
  }
\end{frame}

\begin{frame}{Reduction Strategies}
  \begin{itemize}
    \item Call by Value - reduce the leftmost innermost redex first.
    \item Call by Name - reduce the leftmost outermost redex first.
    \item Call by Need - optimization of call by name.
  \end{itemize}
  \uncover<2>{
    \begin{theorem}
       Call by Name will always find the normal form if it exists.
    \end{theorem}
  }
\end{frame}

\begin{frame}{Python Examples}

  { \scriptsize
  \url{https://github.com/JaredCorduan/lambda-calc-cofc/blob/master/lambda.py} }
\end{frame}

\begin{frame}{Final Takeaway}
  The lambda calculus explains computer science in three steps:
  \begin{itemize}
    \item variables
    \item abstraction
    \item application
  \end{itemize}
  \uncover<2->{
  ~\\
  It's the ultimate Occam's razor for computation.
  }
  \uncover<3->{
  \\~\\
  Next Steps:
  \begin{itemize}
    \item simply typed lambda calculus
    \item propositions as types
  \end{itemize}
  }
\end{frame}

\begin{frame}
  \centering
  thank you for listening!
\end{frame}

\begin{frame}{Primitive Recursion in the Lambda Calculus}
  Let $f:\mathbb{N}^{k+1}\to\mathbb{N}$ be defined by:
  \vs
  \begin{math}
    \begin{array}{r@{~:=~}l}
      f(0, n_1, \ldots, n_k) & g(n_1, \ldots, n_k) \\
      f(n+1, n_1, \ldots, n_k) & h(f(n, n_1, \ldots, n_k), n, n_1, \ldots, n_k)
    \end{array}
  \end{math}
  \vs
  Define:
  \vs
  \begin{math}
    \begin{array}{r@{~:=~}l}
      \langle M, N\rangle
      &
      \lambda x.x M N
      \\
      \pi_1
      &
      \lambda p.p(\lambda x.\lambda y.x)
      \\
      \pi_2
      &
      \lambda p.p(\lambda x.\lambda y.y)
      \\
      \mathsf{Init}
      &
      \langle 0,G x_1 \ldots x_k \rangle
      \\
      \mathsf{Step}
      &
      \lambda p.\langle \mathsf{SUCC}(\pi_1 p),H(\pi_2 p)(\pi_1 p)x_1\ldots x_k\rangle
      \\
      F
      &
      \lambda x.\lambda x_1.\ldots\lambda x_k.\pi_2(x~\mathsf{Step}~\mathsf{Init})
    \end{array}
  \end{math}

\end{frame}

\end{document}