diff options
Diffstat (limited to 'transp-inf110-02-typage.tex')
| -rw-r--r-- | transp-inf110-02-typage.tex | 32 |
1 files changed, 16 insertions, 16 deletions
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 |