Laboratoire de l'Informatique et du Parallélisme » Linear Arithmetic

  \frametitle{Ramification}

 \begin{itemize}

\item   ramification, a.k.a. tiering, safe recursion

\item distinguish two levels of data-types:

${\red{N_1}}$ (\textit{normal}) integers can trigger induction/recursion

${{N_0}}$ (\textit{safe})  integers cannot; they can just be finitely explored

\item ramified recursion scheme:

$$ f({\red{\succ{i} u, \vec v}}{\textbf ;} \vec x)=F_i ({\red{u,\vec v}}{\textbf ; }f(u, \vec v;\vec x), \vec x)$$

\item function algebra for FP: Bellantoni-Cook 92, Leivant 93

          logic for FP: Leivant 95, Cantini 00 

\end{itemize}

 \end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{frame}