\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}