summaryrefslogtreecommitdiffstats
path: root/transp-inf110-02-typage.tex
diff options
context:
space:
mode:
Diffstat (limited to 'transp-inf110-02-typage.tex')
-rw-r--r--transp-inf110-02-typage.tex68
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}