\begin{frame}
 \frametitle{Fixed Points}

  Let $F$ be an arbitrary CL-term.
  Consider:
  \begin{block}{}
    \vspace{-3ex}
    \begin{align*}
    P_F = D(BFD)
    \end{align*}
  \end{block}
  \pause
  \bigskip
  
  \begin{align*}
    P_F = D(BFD) \pause \to^* BFD(BFD)\pause \to^* F(D(BFD)) = FP_F
  \end{align*}
  \pause
  
  Hence $FP_F \fromto^* P_F$.
  \pause
  Looks better if we write $=$ for $\fromto^*$:
  \begin{align*}
    FP_F = P_F
  \end{align*}
  \pause
  $P_F$ is a \emph{fixed point} for $F$\pause
  
  \medskip
  
  \begin{block}{}
  Define the {\em fixed-point combinator}
  $P = [x]D(BxD)$.
  \pause
  Then  $F(PF) = PF$ for any $F$.
  \end{block}
\end{frame}