diff options
| -rw-r--r-- | transp-inf110-02-typage.tex | 142 |
1 files changed, 142 insertions, 0 deletions
diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex index 74e36e4..e548e6f 100644 --- a/transp-inf110-02-typage.tex +++ b/transp-inf110-02-typage.tex @@ -32,6 +32,11 @@ \newcommand{\dbllangle}{\mathopen{\langle\!\langle}} \newcommand{\dblrangle}{\mathclose{\rangle\!\rangle}} \newcommand{\cps}{\mathrm{CPS}} +\newcommand{\dottedlimp}{\mathbin{\dot\Rightarrow}} +\newcommand{\dottedland}{\mathbin{\dot\land}} +\newcommand{\dottedlor}{\mathbin{\dot\lor}} +\newcommand{\dottedtop}{\mathord{\dot\top}} +\newcommand{\dottedbot}{\mathord{\dot\bot}} \mathchardef\emdash="07C\relax \newcommand{\mpdotsabove}[1]{\inferrule*{\vdots}{#1}} \setlength{\derivskip}{4pt} @@ -3966,6 +3971,143 @@ premier ordre : tout énoncé vrai dans tout modèle est démontrable). \end{frame} % +\begin{frame} +\frametitle{Sémantiques du calcul propositionnel intuitionniste ?} + +\itempoint On a vu les \alert{règles syntaxiques} du calcul +propositionnel intuitionniste (déduction naturelle, ou calcul des +séquents). Mais quel est le \textbf{sens} des connecteurs ? + +\medskip + +\begin{itemize} +\item En logique classique, c'est facile : la sémantique des tableaux + de vérité est correcte et complète, donc on peut considérer qu'elle + définit le sens. +\item En logique intuitionniste, on n'a donné pour l'instant qu'une + interprétation intuitive (Brouwer-Heyting-Kolmogorov) des + connecteurs. +\end{itemize} + +\medskip + +\itempoint Avoir une sémantique (correcte) complète, ou « moins +incomplète » que celle des tableaux de vérité permet de prouver qu'une +formule logique n'est \alert{pas démontrable} (si elle n'est pas +validée par cette sémantique). + +\medskip + +{\footnotesize + +\itempoint On peut considérer \alert{Curry-Howard} comme une +sémantique : le « sens » de $\Rightarrow,\land,\lor,\top,\bot$ est +donné par les opérations sur les types d'un langage de programmation, +et les énoncés validés par le modèle sont ceux dont le type est +habité. Elle est complète si le langage est le $\lambda$CST. Mais +elle est peu maniable et/ou un peu triviale ! + +\par} + +\end{frame} +% +\begin{frame} +\frametitle{Sémantique 0 : tableaux de vérité} + +{\footnotesize (Reprise de ce qui a déjà été dit.)\par} + +\medskip + +\itempoint On définit $\mathbb{B} := \{0,1\}$, $\dottedtop = 1$, +$\dottedbot = 0$ et $\dottedland, \dottedlor, \dottedlimp \colon +\mathbb{B}^2 \to \mathbb{B}$ par les tableaux de vérité usuels : + +\smallskip + +\begin{tabular}{c@{\hskip 30bp}c@{\hskip 30bp}c} +$ +\begin{array}{c|cc} +\dottedland&0&1\\\hline +0&0&0\\ +1&0&1\\ +\end{array} +$ +& +$ +\begin{array}{c|cc} +\dottedlor&0&1\\\hline +0&0&1\\ +1&1&1\\ +\end{array} +$ +& +$ +\begin{array}{c|cc} +A \dottedlimp B&B=0&B=1\\\hline +A=0&1&1\\ +A=1&0&1\\ +\end{array} +$ +\end{tabular} + +\medskip + +\itempoint Si $\varphi$ est une formule propositionnelle en $r$ +variables, ceci définit une fonction $\dot\varphi \colon \mathbb{B}^r +\to \mathbb{B}$ par composition. + +\medskip + +\itempoint Un \textbf{modèle booléen} du calcul propositionnel est une +affectation $\{\mathrm{variables}\} \to \mathbb{B}$ : chaque formule +$\varphi$ a donc une valeur de vérité ($0$ ou $1$) dans le modèle, +donnée par $\dot\varphi$. On dit que $\mathcal{M} \vDash \varphi$ +lorsque c'est $1$. + +\medskip + +\itempoint On dit que la sémantique booléenne valide $\varphi$ lorsque +$\mathcal{M} \vDash \varphi$ pour tout modèle (i.e., $\dot\varphi$ +vaut constamment $1$). + +\end{frame} +% +\begin{frame} +\frametitle{Correction et complétude classique des tableaux de vérité} + +\textbf{Théorème :} la sémantique booléenne est \alert{correcte et + complète} pour le calcul propositionnel classique. + +\medskip + +\underline{Esquisse de preuve :} + +\smallskip + +\itempoint\underline{Correction :} on montre par induction sur la +preuve que si $\eta_1,\ldots,\eta_r \vdash \varphi$ alors $\dot\varphi += 1$ dans tout modèle où $\dot\eta_1 = \cdots = \dot\eta_r = 1$ : la +vérification est très facile sur chaque règle du calcul +propositionnel. + +\medskip + +\itempoint\underline{Complétude :} on démontre \alert{classiquement} +$\vdash A_i \lor \neg A_i$ pour chaque variable $A_i$, puis on utilise +l'élimination du $\lor$ pour se placer dans chacun des $2^r$ cas +possibles (i.e., avec $A_i$ ou $\neg A_i$ dans les hypothèses). Dans +chaque cas on a $A_i \Leftrightarrow \top$ ou $A_i \Leftrightarrow +\bot$ pour chaque variable, donc en suivant les tableaux de vérité on +a $\varphi$ (vraie). L'élimination du $\lor$ montre alors $\varphi$ +vraie.\qed + +\bigskip + +\alert{Intuitionnistement}, la correction vaut toujours, mais plus la +complétude ($A\lor\neg A$ n'est pas démontrable). + +\end{frame} +% % TODO: % - Kripke % - CPS et fragment négatif |