Typing and termination.

1 files changed, 41 insertions, 0 deletions

diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex
index 9f53895..f84f192 100644
--- a/transp-inf110-02-typage.tex
+++ b/transp-inf110-02-typage.tex
@@ -467,4 +467,45 @@ linéarité.
 
 \end{frame}
 %
+\begin{frame}
+\frametitle{Typage et terminaison}
+
+Un système de typage \alert{peut} garantir que \textbf{tout programme
+  bien typé termine}.
+
+\bigskip
+
+Ce \alert{n'est pas le cas} pour les langages de programmation usuels
+(en OCaml, Haskell, etc., un programme bien typé peut faire une boucle
+infinie).
+
+\bigskip
+
+Si on veut que le système de typage soit décidable, ceci met forcément
+des \alert{limites sur l'expressivité} du langage
+($\leftarrow$ indécidabilité du problème de l'arrêt).
+
+\bigskip
+
+Notamment, le langage ne permettra pas d'écrire son propre
+interpréteur (même argument « diagonal » que pour les fonctions p.r.
+par thm. de réc\textsuperscript{sion} de Kleene).
+
+\bigskip
+
+Notamment aussi : pas de boucle illimitée, pas d'appels récursifs
+\emph{non contraints}, pas de type tel que $\mathtt{t} \,\cong\,
+(\mathtt{t}\rightarrow \mathtt{t})$.  Aucun terme de type vide !
+
+\bigskip
+
+Néanmoins, le langage peut être \alert{beaucoup plus puissant} que les
+fonctions p.r.
+
+\bigskip
+
+Exemple de tel langage : Coq.
+
+\end{frame}
+%
 \end{document}