\begin{frame}
  \frametitle{Implicit function definition}

  \begin{block}{}
  Given a CL-term $t$, find $F$ such that  
  $$Fx_1\ldots x_n \;\fromto^*\; t[y:=F]$$
  \end{block}
  \bigskip
  \pause
  Application: \alert{recursion}.
  \begin{exampleblock}{}
    Define functions like: $F\; x =$ ``if $x = 0$ then $1$ else $x \cdot F \;(x-1)$''
  \end{exampleblock}
  \bigskip
  \pause
  
  We take:
  \begin{itemize}
    \item $t' = [y][x_1\ldots x_n]t$, and
    \item $F= Yt'$ for some fixed-point combinator $Y$.
  \end{itemize} 
  \pause  
  Then:
  $$Fx_1\ldots x_n = t'Fx_1\ldots x_n
  = t'yx_1\ldots x_n[y:=F] \to^* t[y:=F]$$
\end{frame}