diff options
| -rw-r--r-- | transp-inf110-02-typage.tex | 61 |
1 files changed, 61 insertions, 0 deletions
diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex index 5d43757..25c5720 100644 --- a/transp-inf110-02-typage.tex +++ b/transp-inf110-02-typage.tex @@ -4266,6 +4266,67 @@ $ \end{frame} % +\begin{frame} +\frametitle{Sémantique 2 : les ouverts en topologie} + +Fixons $X$ un espace topologique : si on ne sait pas ce que c'est, +penser à un espace métrique ou simplement $\mathbb{R}^m$ avec sa +topologie ordinaire. On note $\mathcal{O}(X)$ la topologie de $X$, +c'est-à-dire l'ensemble des ouverts de $X$. + +\medskip + +On définit les opérations suivantes sur $\mathcal{O}(X)$ : +\begin{itemize} +\item $U \dottedland V := U\cap V$ +\quad\itempoint $U \dottedlor V := U\cup V$ +\quad\itempoint $\dottedtop := X$ +\quad\itempoint $\dottedbot := \varnothing$ +\item $(U \dottedlimp V) := \operatorname{int}((X\setminus U) \cup V)$ + (où $\operatorname{int}$ désigne l'intérieur) est l'ensemble des + points $x \in X$ tels qu'il y ait un ouvert $W \ni x$ t.q. $(U\cap + W) \subseteq (V\cap W)$ {\footnotesize (= les points « au voisinage + desquels » $U \subseteq V$)}, ou, si on préfère, le plus grand + ouvert $W$ tel que $(U\cap W) \subseteq (V\cap W)$ ; +\item notamment, $\dottedneg U := \operatorname{int}(X\setminus U)$, + plus grand ouvert disjoint de $U$ ; +\item notamment, $\dottedneg \dottedneg U := + \operatorname{int}(\operatorname{adh}(U))$ (intérieur de l'adhérence + de $U$, ou « régularisé » de $U$). +\end{itemize} + +\medskip + +\itempoint Si $\varphi(A_1,\ldots,A_r)$ est une formule +propositionnelle et $U_1,\ldots,U_r \in \mathcal{O}(X)$, on définit +$\dot\varphi(U_1,\ldots,U_r)$ de façon évidente (par induction). + +\end{frame} +% +\begin{frame} +\frametitle{Sémantique des ouverts : correction et complétude} + +De façon surprenante, les opérations qu'on a définies sur les ouverts +de $X$ fournissent un modèle du calcul propositionnel intuitionniste : + +\medskip + +\textbf{Théorème} (Tarski) : la sémantique des ouverts est correcte et +complète pour le calcul propositionnel intuitionniste : +\begin{itemize} +\item\underline{correction :} si $\varphi(A_1,\ldots,A_r)$ est une + théorème du calcul propositionnel intuitionniste, alors quel que + soit $X$ et $U_1,\ldots,U_r$ ouverts de $X$, on a + $\dot\varphi(U_1,\ldots,U_r) = \dottedtop$ (l'espace tout entier) ; +\item\underline{complétude :} réciproquement, si + $\dot\varphi(U_1,\ldots,U_r) = \dottedtop$ pour tous ouverts + $U_1,\ldots,U_r$ de tout espace topologique $X$, \alert{ou même + simplement de $\mathbb{R}^n$}, alors $\varphi$ est démontrable en + calcul propositionnel intuitionniste. +\end{itemize} + +\end{frame} +% % TODO: % - inférence de type de Hindley-Milner % |