Various minor changes (upon re-reading).

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