From 641c5ce34c11e6e96ba7b118a6c9d6f55653257d Mon Sep 17 00:00:00 2001
From: "David A. Madore" <david+git@madore.org>
Date: Wed, 15 Nov 2023 11:13:52 +0100
Subject: Typing and termination.

---
 transp-inf110-02-typage.tex | 41 +++++++++++++++++++++++++++++++++++++++++
 1 file changed, 41 insertions(+)

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
@@ -465,6 +465,47 @@ linéarité.
 
 \itempoint Idris : langage fonctionnel + assistant de preuve.
 
+\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}
-- 
cgit v1.2.3