diff options
| -rw-r--r-- | transp-inf110-02-typage.tex | 41 |
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} |