diff options
| -rw-r--r-- | transp-inf110-02-typage.tex | 162 |
1 files changed, 159 insertions, 3 deletions
diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex index e548e6f..5d43757 100644 --- a/transp-inf110-02-typage.tex +++ b/transp-inf110-02-typage.tex @@ -37,6 +37,7 @@ \newcommand{\dottedlor}{\mathbin{\dot\lor}} \newcommand{\dottedtop}{\mathord{\dot\top}} \newcommand{\dottedbot}{\mathord{\dot\bot}} +\newcommand{\dottedneg}{\mathop{\dot\neg}} \mathchardef\emdash="07C\relax \newcommand{\mpdotsabove}[1]{\inferrule*{\vdots}{#1}} \setlength{\derivskip}{4pt} @@ -1748,7 +1749,8 @@ logique intuitionniste. sémantique booléenne du calcul propositionnel classique »)} : $P$ est une tautologie de la logique classique \alert{ssi} pour toute substitution de $\bot$ ou $\top$ à chacune des variables -propositionnelles de $P$ a la valeur de vérité $\top$. +propositionnelles de $P$ a la valeur de vérité $\top$. (Voir +transp. \ref{truth-table-semantics} plus loin pour précisions.) \bigskip @@ -4012,6 +4014,7 @@ elle est peu maniable et/ou un peu triviale ! \end{frame} % \begin{frame} +\label{truth-table-semantics} \frametitle{Sémantique 0 : tableaux de vérité} {\footnotesize (Reprise de ce qui a déjà été dit.)\par} @@ -4108,9 +4111,162 @@ complétude ($A\lor\neg A$ n'est pas démontrable). \end{frame} % +\begin{frame} +\frametitle{Sémantique 1 : cadres de Kripke} + +\textbf{Définitions :} +\begin{itemize} +\item un \textbf{cadre de Kripke} est {\footnotesize (dans ce + contexte)} un ensemble partiellement ordonné $(W,\leq)$ ; les + éléments de $W$ s'appellent les \textbf{mondes} ; si $w\leq w'$, on + dit que $w'$ est \textbf{accessible} depuis $w$ ; +\item dans un cadre de Kripke, une \textbf{affectation de vérité} est + une fonction $p\colon W \to \mathbb{B}$ (où $\mathbb{B} = \{0,1\}$) + telle que si $p(w) = 1$ et $w\leq w'$ alors $p(w') = 1$ (i.e., $p$ + est croissante, on dit aussi « permanente ») ; +\item on définit des opérations $\dottedland, \dottedlor, \dottedlimp$ + sur les affectations de vérité : +\begin{itemize} +\item $(q_1\dottedland q_2)(w) = 1$ ssi $q_1(w) = 1$ et $q_2(w) = 1$ ; +\item $(q_1\dottedlor q_2)(w) = 1$ ssi $q_1(w) = 1$ ou $q_2(w) = 1$ ; +\item $(q_1\dottedlimp q_2)(w) = 1$ ssi pour tout $w' \geq w$ t.q. + $q_1(w') = 1$, on a $q_2(w') = 1$ ; +\item $\dottedtop(w) = 1$ partout ; +\quad\itempoint $\dottedbot(w) = 0$ partout. +\end{itemize} +\item un \textbf{modèle de Kripke} est {\footnotesize (dans ce + contexte)} un cadre de Kripke $(W,\leq)$ muni d'une affectation de + vérité pour chaque variable propositionnelle ; +\item $\varphi$ est \textbf{validée} par le modèle de Kripke lorsque + $\dot\varphi$ vaut $1$ dans tout monde $w$. +\end{itemize} + +\end{frame} +% +\begin{frame} +\frametitle{Cadres de Kripke (suite)} + +{\footnotesize Recopie : \itempoint $(q_1\dottedland q_2)(w) = 1$ ssi + $q_1(w) = 1$ et $q_2(w) = 1$ ;\quad\itempoint $(q_1\dottedlor + q_2)(w) = 1$ ssi $q_1(w) = 1$ ou $q_2(w) = 1$ ;\quad\itempoint + $(q_1\dottedlimp q_2)(w) = 1$ ssi pour tout $w' \geq w$ t.q. + $q_1(w') = 1$, on a $q_2(w') = 1$.\par} + +\medskip + +Par exemple : +\begin{itemize} +\item $\dottedneg p$ (c'est-à-dire $p\dottedlimp \dottedbot$) vaut $1$ + dans le monde $w$ lorsque $p$ vaut $0$ dans \alert{tout monde + accessible} depuis $w$ ; +\item $p\dottedlor\dottedneg p$ vaut $1$ dans le monde $w$ lorsque $p$ + vaut $0$ dans \alert{tout monde accessible} depuis $w$ ou bien $1$ + dans $w$ (donc dans tout monde accessible depuis $w$, par + permanence) : \textcolor{teal}{$p$ est « décidé » à vrai ou à + faux} ; +\item $\dottedneg \dottedneg p$ vaut $1$ dans le monde $w$ lorsque + $\forall w'\geq w.\, \exists w''\geq w'.\, p(w'')=1$ + \textcolor{teal}{(« dans tout futur possible, $p$ finit par devenir + vrai »)}. +\end{itemize} + +\bigskip + +\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 +« dans tout monde possible où $A$ est vrai, $B$ l'est ». + +\end{frame} +% +\begin{frame} +\frametitle{Sémantique des cadres de Kripke} + +\textbf{Définitions} (suite) : +\begin{itemize} +\item {\footnotesize (déjà dit :)} $\varphi$ est \textbf{validée} par + le \alert{modèle} de Kripke (= valide dedans, = valable) lorsque + $\dot\varphi$ vaut $1$ dans tout monde $w$ ; +\item $\varphi$ est \textbf{validée} par le \alert{cadre} de Kripke + lorsqu'elle est validée par toute affectation de vérité pour chacune + de ses variables (= tout modèle sur ce cadre) ; +\item $\varphi$ est \textbf{validée} par \alert{la sémantique de + Kripke} lorsque $\varphi$ est validée par tout cadre (i.e., tout + modèle de Kripke). +\end{itemize} + +\bigskip + +\textbf{Théorème} (Kripke) : la sémantique de Kripke est correcte et +complète pour le calcul propositionnel intuitionniste : +\begin{itemize} +\item\underline{correction :} tout théorème propositionnel + intuitionniste est valide dans tout modèle de Kripke, +\item\underline{complétude :} toute formule propositionnelle valide + dans tout modèle de Kripke est démontrable en calcul propositionnel + intuitionniste. +\end{itemize} + +\end{frame} +% +\begin{frame} +\frametitle{Cadres de Kripke : remarques} + +La sémantique de Kripke n'est complète que quand on considèe +\alert{tous les cadres}. Si on se limite aux modèles sur un cadre +donné, ils peuvent valider des formules non démontrables. +\begin{itemize} +\item Le cadre réduit à un singleton valide la logique classique : + c'est exactement la sémantique booléenne ; +\item Si $(W,\leq)$ est totalement ordonné, il valide la formule + $(A\Rightarrow B) \lor (B\Rightarrow A)$ {\footnotesize + (\underline{preuve :} sinon il y a un monde $w$ dans lequel + $p_A(w)=1$ mais $p_B(w)=0$ et un $w'$ dans lequel $p_A(w')=0$ mais + $p_B(w')=1$ ; mais si $w\leq w'$ ceci contredit la permanence de + $p_A$ et si $w\geq w'$ ceci contredit la permanence de + $p_B$~\qedsymbol)} qui n'est pas prouvable en logique + propositionnelle intuitionniste. +\item Le cadre le plus simple après un singleton est $(\{0,1\},\leq)$, + qui correspond à une logique à trois valeurs de vérité, avec les + tableaux suivants. +\end{itemize} + +{\footnotesize + +\begin{tabular}{c@{\hskip 30bp}c@{\hskip 30bp}c} +$ +\begin{array}{c|ccc} +\dottedland&0&?&1\\\hline +0&0&0&0\\ +?&0&?&?\\ +1&0&?&1\\ +\end{array} +$ +& +$ +\begin{array}{c|ccc} +\dottedlor&0&?&1\\\hline +0&0&?&1\\ +?&?&?&1\\ +1&1&1&1\\ +\end{array} +$ +& +$ +\begin{array}{c|ccc} +A \dottedlimp B&B=0&B={?}&B=1\\\hline +A=0&1&1&1\\ +A={?}&0&1&1\\ +A=1&0&?&1\\ +\end{array} +$ +\end{tabular} + +\par} + +\end{frame} +% % TODO: -% - Kripke -% - CPS et fragment négatif % - inférence de type de Hindley-Milner % \end{document} |