\begin{frame}
  \frametitle{Church Pairs}
  
  \begin{block}{}
    Church encoding of pairs: $\mathsf{pair} = \lambda x.\; \lambda y.\;\lambda f.f x y$.
    \pause
    In CL:
    \begin{align*}
      \mathsf{pair} &= [xyf]\; f\;x\;y\\
      \mathsf{fst} &= [p]\; p\; K\\
      \mathsf{snd} &= [p]\; p\; (KI)
    \end{align*}    
  \end{block}
  \pause
  \medskip
  We have:
  \begin{align*}
    \mathsf{pair}\; s\; t
      &\pause= ([xyf]\; f\;x\;y) \; s\; t
      \pause\to^* ([f]\; f\;x\;y) [x \mapsto s,\; y \mapsto t] \pause \approx [f]\;f\;s\;t\\
    \pause
    \mathsf{fst}\; (\mathsf{pair}\; s\; t) 
      &\pause\to^* ([p]\;p\;K) \; ([f]\; f\;s\;t)
      \pause\to^* ([f]\; f\;s\;t) K
      \pause\to^* K\;s\;t
      \pause\to^* s\\
    \pause
    \mathsf{snd}\; (\mathsf{pair}\; s\; t) 
      &\pause\to^* ([p]\;p\;(KI)) \; ([f]\; f\;s\;t)
      \pause\to^* ([f]\; f\;s\;t) (KI)
      \pause\to^* KI\;s\;t
      \pause\to^* t
  \end{align*}
  \pause
  \medskip
  Exercise:\\[-2ex]
  \begin{itemize}
    \item compute \quad $[xyf]\; f\;x\;y$,\quad $[p]\; p\; K$, \quad and \quad $[p]\; p\; (KI)$.
    \item devise an encoding of triples
  \end{itemize}
\end{frame}