diff options
| -rw-r--r-- | transp-inf110-02-typage.tex | 35 |
1 files changed, 34 insertions, 1 deletions
diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex index 55c5de1..9040312 100644 --- a/transp-inf110-02-typage.tex +++ b/transp-inf110-02-typage.tex @@ -170,7 +170,7 @@ sont \emph{souvent} proposées par les systèmes de typage : \bigskip -\itempoint Types \textbf{produits} (= paires, triplets, $k$-uplets). +\itempoint Types \textbf{produits} (= couples, triplets, $k$-uplets). P.ex. $\texttt{Nat} \times \texttt{Bool}$ = type des paires formées d'un entier et d'un booléen. @@ -580,6 +580,39 @@ restrictions : \end{frame} % \begin{frame} +\frametitle{La correspondance de Curry-Howard (premier aperçu)} + +{\footnotesize\textcolor{gray}{Divulgâchis pour la suite !}\par} + +\smallskip + +La correspondance de Curry-Howard fait notamment correspondre : +\begin{itemize} +\item type \textbf{fonction} $A \to B$ avec \textbf{implication} + logique $A \Rightarrow B$, +\item \textbf{application} d'une fonction ($A \to B$ à un argument de + type $A$) avec \textbf{\textit{modus ponens}} (si $A \Rightarrow B$ + et $A$, alors $B$), +\item \textbf{abstraction} (= création d'une fonction) avec ouverture + d'une \textbf{hypothèse} (« supposons $A$ : alors (…) donc $B$ ; + ceci prouve $A \Rightarrow B$ »), +\item type \textbf{produit} (= couples) $A \times B$ avec + \textbf{conjonction} (« et ») logique $A \land B$, +\item type \textbf{somme} $A + B$ avec \textbf{disjonction} (« ou ») + logique $A \lor B$, +\item types \textbf{trivial} ($\texttt{Unit}$) et \textbf{vide} avec + \textbf{vrai} $\top$ et \textbf{faux} $\bot$ logiques, +\item mais pour la \textbf{négation}… c'est plus délicat. +\end{itemize} + +\bigskip + +{\footnotesize Les détails demandent un système de typage et un + système logique précisément définis.\par} + +\end{frame} +% +\begin{frame} \frametitle{Paradoxe de Curry (interlude distrayant)} {\footnotesize Variante plus sophistiquée de « cette phrase est |