diff options
| -rw-r--r-- | transp-inf110-02-typage.tex | 45 |
1 files changed, 28 insertions, 17 deletions
diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex index 32ff068..3899f54 100644 --- a/transp-inf110-02-typage.tex +++ b/transp-inf110-02-typage.tex @@ -1042,16 +1042,16 @@ La dérivation du jugement de typage $\Gamma \vdash M : \sigma$ d'un évidemment à partir de $M$ (\alert{aucun choix} à faire !) : \begin{itemize} \item si $M = x$ est une variable, alors un $x:\sigma$ doit être dans - le contexte $\Gamma$ (sinon : échouer), et la dérivation est par la + le contexte $\Gamma$ (sinon : échouer), et la dérivation finit par la règle « variable » ; \item si $M = PQ$ est une application, construire des dérivations de jugements $\Gamma \vdash P : \rho$ et $\Gamma \vdash Q : \sigma$, on doit avoir $\rho = (\sigma\to\tau)$ (sinon : échouer), et la - dérivation est par la règle « application » ; + dérivation finit par la règle « application » ; \item si $M = \lambda(v:\sigma).E$ est une abstraction, construire une dérivation de jugement $\Gamma' \vdash E : \tau$ dans $\Gamma' := \Gamma \cup \{v:\sigma\}$ {\footnotesize (quitte à renommer $v$)}, - et la dérivation est par la règle « abstraction ». + et la dérivation finit par la règle « abstraction ». \end{itemize} \bigskip @@ -1255,9 +1255,9 @@ On prouve alors successivement : \item tout terme fortement calculable est fortement normalisable (induction facile sur le type), \item si $x_1:\sigma_1,\ldots,x_k:\sigma_k \vdash E:\tau$ et si - $v_1,\ldots,v_k$ sont de types $\sigma_1,\ldots,\sigma_k$, fortement + $P_1,\ldots,P_k$ sont de types $\sigma_1,\ldots,\sigma_k$, fortement calculables et n'impliquant pas $x_1,\ldots,x_k$, alors la - substitution de $v_i$ pour $x_i$ dans $E$ est fortement calculable + substitution de $P_i$ pour $x_i$ dans $E$ est fortement calculable (preuve par induction sur la dérivation du jugement, i.e., induction sur $E$ : le cas délicat est l'abstraction). \end{itemize} @@ -1273,7 +1273,7 @@ On prouve alors successivement : \itempoint Le \textbf{calcul propositionnel} est une forme de logique qui ne parle que de « propositions » (énoncés logiques) : pas de variables d'individus (p.ex. entiers naturels, ensembles…), \alert{pas - de quantification}. + de quantification} (pas de $\forall,\exists$). \medskip @@ -1294,10 +1294,10 @@ abréviation de $P \Rightarrow \bot$ (soit : « $P$ est absurde »). On distingue {\footnotesize (les règles précises seront décrites plus loin)} : \begin{itemize} -\item la logique \textbf{classique} qui admet la règle du \alert{tiers - exclu} (« tertium non datur ») sous une forme ou une autre ; logique - usuelle des mathématiques ; on peut la modéliser par $2$ valeurs de - vérité (« vrai » et « faux ») ; +\item la logique \textbf{classique} ou \textbf{booléenne} qui admet la + règle du \alert{tiers exclu} (« tertium non datur ») sous une forme + ou une autre : logique usuelle des maths ; on peut la modéliser par + $2$ valeurs de vérité (« vrai » et « faux ») ; \item la logique \textbf{intuitionniste}, plus \emph{faible}, qui n'admet pas cette règle : il n'y a pas vraiment de « valeur de vérité ». @@ -1339,6 +1339,12 @@ On distingue {\footnotesize (les règles précises seront décrites plus \vdash Q$ s'appelle un \textbf{séquent}, à comprendre comme « sous les hypothèses $P_1,\ldots,P_r$, on a $Q$ ». +\medskip + +{\footnotesize \itempoint Notation historique : « $\supset$ » pour + notre « $\Rightarrow$ », et « $\Rightarrow$ » pour notre + « $\vdash$ ».\par} + \end{frame} % \begin{frame} @@ -1353,8 +1359,8 @@ et des règles d'\textbf{élimination} permettant de l'\alert{utiliser}. En français, et un peu informellement : \begin{itemize} \item pour introduire $\Rightarrow$ : on démontre $Q$ \alert{sous - l'hypothèse} $P$, ce qui donne $P\Rightarrow Q$ (hypothèse - déchargée) ; + l'hypothèse} $P$, ce qui donne $P\Rightarrow Q$ (sans hypothèse : + « hypothèse déchargée ») ; \item pour éliminer $\Rightarrow$ : si on a $P\Rightarrow Q$ et $P$, on a $Q$ (\textit{modus ponens}) ; \item pour introduire $\land$ : on démontre $Q_1$ et $Q_2$, ce qui @@ -1514,7 +1520,7 @@ pour un gain de place) : \medskip {\footnotesize\textbf{N.B.} : une même hypothèse \emph{peut} être - déchargée à plusieurs endroits ($u$ dans le 1\textsuperscript{er} + déchargée sur plusieurs endroits ($u$ dans le 1\textsuperscript{er} exemple).\par} \end{frame} @@ -1668,7 +1674,7 @@ Bien distinguer : \smallskip \textcolor{teal}{« Supposons $A$ [vrai]. Alors (...), ce qui est - absurde. Donc $A$ est faux. »} + absurde. Donc $A$ est faux [i.e., $\neg A$]. »} \smallskip @@ -1736,7 +1742,7 @@ Tableaux de vérité : \smallskip -\begin{tabular}{c||c||c} +\begin{tabular}{c@{\hskip 30bp}c@{\hskip 30bp}c} $ \begin{array}{c|cc} \land&\bot&\top\\\hline @@ -2119,6 +2125,11 @@ $\inferrule*[left={Inj$_2$}]{\Gamma\vdash t:\tau_2}{\Gamma\vdash \iota_2^{(\tau_ \begin{frame} \frametitle{Remarques sur types produits et sommes} +\itempoint $\iota_1,\iota_2$ sont des \emph{constructeurs} dans la +terminologie OCaml. + +\medskip + \itempoint À côté de la $\beta$-réduction usuelle du $\lambda$-calcul, $(\lambda (v:\sigma). e)t \rightsquigarrow e[v\backslash t]$, on introduit des nouvelles règles de réduction pour la conjonction et la @@ -2134,14 +2145,14 @@ disjonction : \medskip \itempoint Côté démonstrations : cette réduction court-circuite une -règle \textsc{Intro} immédiatement suivie par une règle \textsc{Élim} +règle \textsc{Intro} immédiatement suivie par sa règle \textsc{Élim} (ce qu'on appelle un « détour »). \medskip \itempoint Le $\lambda$-calcul simplement typé reste fortement normalisant avec ces extensions par types produits et sommes et les -réductions ci-dessus. +réductions ci-dessus {\footnotesize (et types $1$ et $0$ après)}. \medskip |