Fix a bunch of minor mistakes (mostly typos)HEADmaster

Pointed out by LLMs while converting slides to expanded handout.

3 files changed, 27 insertions, 27 deletions

diff --git a/transp-inf110-01-calc.tex b/transp-inf110-01-calc.tex
index 8ebfc53..145ed81 100644
--- a/transp-inf110-01-calc.tex
+++ b/transp-inf110-01-calc.tex
@@ -1239,7 +1239,7 @@ induction suivant la déf\textsuperscript{n} de $\mathbf{R}$
 \[
 \begin{aligned}
 \varphi_e^{(k+1)}(\underline{x},0) &= g(\underline{x})\\
-\varphi_e^{(k+1)}(\underline{x},z+1) &= h(\underline{x},f(\underline{x},z),z)
+\varphi_e^{(k+1)}(\underline{x},z+1) &= h(\underline{x}, \varphi_e^{(k+1)}(\underline{x},z),z)
 \end{aligned}
 \]
 \item si $e = \dbllangle 5, k, c\dblrangle$ et $g :=
@@ -3267,7 +3267,7 @@ d'entiers naturels.
 
 \bigskip
 
-\itempoint La fonction $T \mapsto 1$ qui à un terme $T$ associe $0$ si
+\itempoint La fonction qui à un terme $T$ associe $0$ si
 $T$ est en forme normale et $1$ si non, \textbf{est p.r.}
 
 \medskip
@@ -3469,7 +3469,7 @@ $\pi_1,\pi_2$ (projections).
 est représentée par
 \[
 \lambda x_1\cdots x_k z.
-\pi_1(z(\lambda p.\Pi(w x_1\cdots x_k (\pi_1 p)(\pi_2 p))A(\pi_2 p))(\Pi(vx_1\cdots x_k)\overline{0}))
+\pi_1(z(\lambda p.\Pi(w x_1\cdots x_k (\pi_1 p)(\pi_2 p))(A(\pi_2 p)))(\Pi(vx_1\cdots x_k)\overline{0}))
 \]
 où
 \[
@@ -3598,8 +3598,8 @@ Cette fois :
 &= (\lambda f. ((\lambda x.f(\lambda v.x x v)) (\lambda x.f(\lambda v.x x v))))(\lambda h.E)\\
 &\rightarrow (\lambda x.(\lambda h.E)(\lambda v.x x v)) (\lambda x.(\lambda h.E)(\lambda v.x x v))
 =: h_{\mathrm{fix}}\\
-&\rightarrow (\lambda h.E)(\lambda v.(\lambda x.(\lambda h.E)(x x)) (\lambda x.(\lambda h.E)(x x))v)
-= (\lambda h.E)(\lambda v. h_{\mathrm{fix}} v)\\
+&\rightarrow (\lambda h.E)(\lambda v.(\lambda x.(\lambda h.E)(\lambda v.x x v)) (\lambda x.(\lambda h.E)(\lambda v.x x v))v)\\
+&= (\lambda h.E)(\lambda v. h_{\mathrm{fix}} v)\\
 &\rightarrow E[h\backslash \lambda v. h_{\mathrm{fix}} v]
 \text{~(substitution de $\lambda v. h_{\mathrm{fix}} v$ pour $h$ dans $E$)}
 \end{aligned}
diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex
index 0694479..e8ff03e 100644
--- a/transp-inf110-02-typage.tex
+++ b/transp-inf110-02-typage.tex
@@ -310,7 +310,7 @@ Pas seulement pour les fonctions !  $\texttt{[]} :
 \smallskip
 
 {\footnotesize Et même : $\texttt{while~true~do~pass~done} :
-  (\forall\mathtt{t})\; \mathtt{t}$ (boule infinie)\par}
+  (\forall\mathtt{t})\; \mathtt{t}$ (boucle infinie)\par}
 
 \bigskip
 
@@ -1765,7 +1765,7 @@ logique intuitionniste.
 
 \itempoint\textbf{Théorème} {\footnotesize (« complétude de la
   sémantique booléenne du calcul propositionnel classique »)} : $P$
-est un théorème de la logique classique \alert{ssi} pour toute
+est un théorème de la logique classique \alert{ssi} toute
 substitution de $\bot$ ou $\top$ à chacune des variables
 propositionnelles de $P$ a la valeur de vérité $\top$.  (Voir
 transp. \ref{truth-table-semantics} plus loin pour précisions.)
@@ -3290,7 +3290,7 @@ et invoquer explicitement :
 \item\alert{invoquer} la contin\textsuperscript{ion} avec une valeur
   $v$ a pour effet de faire retourner à $f$ la valeur $v$ (même si
   elle avait \alert{déjà} terminé),
-\item c'est une sorte de \texttt{goto} jusqu'au point à $f$ termine,
+\item c'est une sorte de \texttt{goto} jusqu'au point où $f$ termine,
   avec restauration de la pile (en C : \texttt{getcontext} pour
   capturer, \texttt{setcontext} pour restaurer).
 \end{itemize}
@@ -3763,7 +3763,7 @@ $\mathop{\sim}P := (P\Rightarrow Z)$ et $P^{\cps} :=
 \item $(fx)^{\cps} = \lambda (k:\mathop{\sim}Q^\diamond).\,
   f^{\cps}(\lambda (f_0:P^\diamond\Rightarrow Q^{\cps}).\,
   x^{\cps}(\lambda (x_0:P^\diamond).\, f_0 x_0 k))$ lorsque $f :
-  P\Rightarrow Q$ et $x : Q$ (rappel : $(P\Rightarrow Q)^{\cps} =
+  P\Rightarrow Q$ et $x : P$ (rappel : $(P\Rightarrow Q)^{\cps} =
   \mathop{\sim}\mathop{\sim}(P^\diamond \Rightarrow Q^{\cps})$),
 \item $(\lambda (v:P).t)^{\cps} = \lambda k.\, k(\lambda
   (v:P^\diamond).\, t^{\cps})$ lorsque $\Gamma, v:P \vdash t:Q$,
@@ -3787,7 +3787,7 @@ $\mathop{\sim}P := (P\Rightarrow Z)$ et $P^{\cps} :=
 \item $\bullet^{\cps} = \lambda (k:\mathop{\sim}\top).k{\bullet}$
 \item $(\texttt{exfalso}^{(Q)} r)^{\cps} = \lambda
   (k:\mathop{\sim}Q^\diamond).\, r^{\cps}(\lambda (r_0:\bot).\,
-  (\texttt{exfalso}^{(Q^\diamond)} r_0))$
+  k(\texttt{exfalso}^{(Q^\diamond)} r_0))$
 \end{itemize}
 
 \itempoint $\texttt{callcc}^{\cps} = \lambda (\ell:\cdots).\,
@@ -3893,7 +3893,7 @@ en logique classique, donc on a évidemment
 \[
 \mathsf{CPC} \vdash P\text{~ssi~}\mathsf{CPC} \vdash P^{\cps}
 \]
-Comme par ailleurs $\mathsf{CPC} \vdash Q$ implique $\mathsf{IPC} \vdash
+Comme par ailleurs $\mathsf{IPC} \vdash Q$ implique $\mathsf{CPC} \vdash
 Q$, on déduit des deux affirmations ci-dessus que (pour $Z=\bot$) :
 \[
 \mathsf{CPC} \vdash P\text{~\alert{ssi}~}\mathsf{IPC} \vdash P^{\cps}
@@ -4197,7 +4197,7 @@ Par exemple :
 
 \itempoint La sémantique de Kripke modélise plus ou moins l'intuition
 selon laquelle « $A \Rightarrow B$ » ne signifie pas juste « soit $A$
-est vrai soit $B$ est faux » (sens en logique classique) mais bien
+est faux soit $B$ est vrai » (sens en logique classique) mais bien
 « dans tout monde possible où $A$ est vrai, $B$ l'est ».
 
 \end{frame}
@@ -4394,18 +4394,18 @@ intuitionniste.
   V_1\dottedlor V_2$
 \quad\itempoint Donc $(\dottedneg U \dottedlimp (V_1\dottedlor V_2)) =
 \mathbb{R}^2$
-\item $(\dottedneg U \dottedlimp V_1) = \{(x_1,x_2) : x_1<0
-  \text{~ou~} x_2>0\}$
-\item $(\dottedneg U \dottedlimp V_2) = \{(x_1,x_2) : x_1>0
+\item $(\dottedneg U \dottedlimp V_1) = \{(x_1,x_2) : x_1>0
   \text{~ou~} x_2<0\}$
+\item $(\dottedneg U \dottedlimp V_2) = \{(x_1,x_2) : x_1<0
+  \text{~ou~} x_2>0\}$
 \item $(\dottedneg U \dottedlimp V_1) \dottedlor (\dottedneg U
   \dottedlimp V_2) = \mathbb{R}^2 \setminus\{(0,0)\}$
 \end{itemize}
 Ceci montre que $(\neg A \Rightarrow (B_1\lor B_2)) \Rightarrow (\neg
 A \Rightarrow B_1) \lor (\neg A \Rightarrow B_2)$ (« axiome de
 Kreisel-Putnam ») n'est pas prouvable en logique intuitionniste (et
-\textit{a fortiori} $(C \Rightarrow B_1) \lor (C \Rightarrow B_2)
-\Rightarrow (C \Rightarrow (B_1\lor B_2))$ ne l'est pas).
+\textit{a fortiori} $(C \Rightarrow (B_1\lor B_2)) \Rightarrow (C
+\Rightarrow B_1) \lor (C \Rightarrow B_2)$ ne l'est pas).
 
 \par}
 
@@ -4717,8 +4717,8 @@ $X_1,\ldots,X_r$ de candidats donnés.
 \medskip
 
 \itempoint On dit que $\varphi$ est Medvedev-valide si pour tous
-$X_1,\ldots,X_r$ il existe \alert{un même} $z \in Z$ tel que $z \in
-\dot\varphi((X_1,S_1),\ldots,(X_r,S_r))$ quels que soient
+$X_1,\ldots,X_r$ il existe \alert{un même} $z \in Z$ qui soit solution
+de $\dot\varphi((X_1,S_1),\ldots,(X_r,S_r))$ quels que soient
 $S_1,\ldots,S_r$ (sous-ensembles respectifs de $X_1,\ldots,X_r$).
 
 \medskip
@@ -4753,7 +4753,7 @@ pour le calcul propositionnel intuitionniste.
 
 \smallskip
 
-\itempoint Donné un type du $\lambda$CST, on appelle
+\itempoint Donné un terme du $\lambda$CST, on appelle
 \textbf{désannotation} de celui-ci le type du $\lambda$-calcul non
 typé obtenu en retirant toutes les annotations de type : p.ex.
 \[
@@ -4761,7 +4761,7 @@ typé obtenu en retirant toutes les annotations de type : p.ex.
 \lambda(f:((\alpha\to\beta)\to\beta)\to\gamma).\,
 f(\lambda(h:\alpha\to\beta).hx)
 \]
-de type $\alpha \to ((\alpha\to\beta)\to\beta)\to\gamma \to \gamma$ se
+de type $\alpha \to (((\alpha\to\beta)\to\beta)\to\gamma) \to \gamma$ se
 désannote en $\lambda xf.\, f(\lambda h.hx)$.
 
 \medskip
diff --git a/transp-inf110-03-quantif.tex b/transp-inf110-03-quantif.tex
index 95f05f2..e6c3ddf 100644
--- a/transp-inf110-03-quantif.tex
+++ b/transp-inf110-03-quantif.tex
@@ -432,7 +432,7 @@ de $Q(x)$.
 \frametitle{Notations des $\lambda$-termes pour $\exists$}
 
 \itempoint \textcolor{blue}{\underline{Introduction du $\exists$ :}}
-si $t$ désigne un terme de type type $I$ et $z$ une preuve de
+si $t$ désigne un terme de type $I$ et $z$ une preuve de
 $Q[v\backslash t]$ (pour ce $t$-là, donc), on notera $\langle
 t,z\rangle$ la preuve de $\exists(v:I).\,Q$ obtenue par introduction
 du $\exists$.
@@ -458,7 +458,7 @@ donc), on notera $(\texttt{match~}z\texttt{~with~}\langle v,h\rangle
 \medskip
 
 \itempoint Ceci est conforme à l'idée de BHK : une preuve de
-$\exists(v:I).\, P(v)$ est la donnée d'un $t$ de type $I$ d'une preuve
+$\exists(v:I).\, P(v)$ est la donnée d'un $t$ de type $I$ et d'une preuve
 de $Q(t)$.
 
 \end{frame}
@@ -1394,7 +1394,7 @@ Curry-Howard.
 
 \itempoint Il faut y penser comme le type des \textbf{témoignages
   d'égalité} de $m$ et $n$.  En pratique, ce sera un type ayant
-seul habitant $\{m\}$ lorsque $m=n$ et aucun sinon.
+seul habitant $m$ lorsque $m=n$ et aucun sinon.
 
 \medskip
 
@@ -1754,12 +1754,12 @@ intuitioniste, pas limitée au premier ordre) $T$ telle que :
 \item $T$ permet de formaliser « $\varphi_e(i){\downarrow}$ »
   (calculablement en $e$ et $i$),
 \item si $\varphi_e(i){\downarrow}$ alors on peut tirer d'une trace
-  d'exécution une preuve de ce fait dans $T$, et idem pour une boule
+  d'exécution une preuve de ce fait dans $T$, et idem pour une boucle
   infinie explicite,
 \end{itemize}
 on peut construire le programme $g_T$ qui cherche en parallèle dans
 $T$ une preuve de que $g_T$ termine ou ne termine pas, et fait une
-boule infinie explicite dans le premier cas, termine immédiatement
+boucle infinie explicite dans le premier cas, termine immédiatement
 dans le second.
 
 \medskip
@@ -1797,7 +1797,7 @@ Soit $g''$ le programme qui :
 $0$ soit $1$.  Si $g''$ termine et renvoie $0$, alors $T$ le prouve,
 donc $g''$ termine et renvoie $1$, contradiction ; si $g''$ termine et
 renvoie $1$, alors $T$ le prouve, donc (par $\mathsf{Consis}(T)$) il
-ne proue pas que $g''$ termine et renvoie $0$, donc $g''$ termine et
+ne prouve pas que $g''$ termine et renvoie $0$, donc $g''$ termine et
 renvoie $0$, contradiction.
 
 \end{frame}