diff options
| -rw-r--r-- | transp-inf110-02-typage.tex | 68 |
1 files changed, 67 insertions, 1 deletions
diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex index 60bef3a..c9269d5 100644 --- a/transp-inf110-02-typage.tex +++ b/transp-inf110-02-typage.tex @@ -468,6 +468,7 @@ linéarité. \end{frame} % \begin{frame} +\label{typing-and-termination} \frametitle{Typage et terminaison} Un système de typage \alert{peut} garantir que \textbf{tout programme @@ -543,7 +544,7 @@ restrictions : \item la logique concernée est plutôt « intuitionniste » (sans tiers exclu), \item diverses subtilités notamment dans la correspondance entre types - sommes paramétriques et $\exists$ côté logique. + sommes paramétriques (types $\Sigma$) et $\exists$ côté logique. \end{itemize} \end{frame} @@ -596,4 +597,69 @@ tacite qu'on peut construire un tel $A$. \end{frame} % +\begin{frame} +\frametitle{Théories des types pour la logique (très bref aperçu)} + +\itempoint Langages spécialisés pour servir à la fois à l'écriture de +programmes informatiques et de preuves mathématiques ; ils peuvent +être soit sous forme de systèmes abstraits, soit sous forme +d'implémentation informatique (« assistants de preuve » : Coq, Agda, +Lean…). + +\bigskip + +\itempoint Dans tous les cas il s'agit de langages assurant la +terminaison des programmes (cf. transp. \ref{typing-and-termination}), +ou, dans le contexte du $\lambda$-calcul, la \emph{normalisation +forte}. Le type vide doit être inhabité ! + +\bigskip + +Principales grandes familles (chacune avec énormément de variantes) : +\begin{itemize} +\item théories des types à la Martin-Löf (« MLTT ») : suit jusqu'au + bout la correspondance de Curry-Howard (\emph{aucune} distinction + entre types et propositions ; {\footnotesize pas de $\exists$ mais + plutôt un $\Sigma$}), $\rightarrow$ Agda ; +\item variantes du « calcul des constructions » (« CoC »), + $\rightarrow$ Coq ; +\item théorie homotopique des types (« HoTT ») : « égalité = isomorphisme ». +\end{itemize} + +\end{frame} +% +\begin{frame} +\frametitle{Le $\lambda$-cube de Barendregt (très bref aperçu)} + +Il s'agit d'un ensemble de $8 = 2^3$ théories des types pour la +logique : la plus faible est le « $\lambda$-calcul simplement typé » +($\lambda_\rightarrow$, décrit plus loin), la plus forte le « calcul +des constructions » (« CoC »). + +\medskip + +Chaque théorie du cube est caractérisée par l'absence ou la présence +de chacune des $3$ fonctionnalités suivantes ($\lambda_\rightarrow$ +n'a aucune des trois, CoC a les trois) : + +\begin{itemize} +\item \textcolor{blue}{termes pouvant dépendre de types}, ou + polymorphisme paramétrique « explicitement quantifié » (p.ex. $\prod + t.\; (t \rightarrow t)$) ; +\item \textcolor{blue}{types pouvant dépendre de types}, ou + constructeurs de types ; +\item \textcolor{blue}{types pouvant dépendre de termes}, ou « types + dépendants », correspondant côté logique à la quantification sur les + individus. +\end{itemize} + +\medskip + +{\footnotesize On peut ensuite encore ajouter des fonctionnalités : + par exemple, Coq est basé sur le « calcul des constructions + inductives » qui ajoute au calcul des constructions des mécanismes + systématiques pour former des types (positivement !) récursifs.\par} + +\end{frame} +% \end{document} |