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