Something about Medvedev's logic of finite problems.

1 files changed, 68 insertions, 0 deletions

diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex
index db51856..6acf11d 100644
--- a/transp-inf110-02-typage.tex
+++ b/transp-inf110-02-typage.tex
@@ -4627,6 +4627,74 @@ une vraie promesse et donc a vraiment renvoyé un élément de $B_1$.
 
 \end{frame}
 %
+\begin{frame}
+\frametitle{Sémantique 4 : les problèmes finis}
+
+\itempoint Un \textbf{problème fini} est un couple $(X,S)$ où $X$ est
+un ensemble fini non vide appelé les \textbf{candidats} du problème et
+$S \subseteq X$ est un sous-ensemble appelé les \textbf{solutions} du
+problème.
+
+\medskip
+
+On définit les opérations suivantes sur les problèmes finis :
+\begin{itemize}
+\item $(X,S)\dottedland (Y,T) = (X\times Y, S\times T)$ (produit cartésien)
+\item $(X,S)\dottedlor (Y,T) = (X\uplus Y, S\uplus T)$ (réunion disjointe)
+\item $(X,S)\dottedlimp (Y,T) = (Y^X, U)$ où $U := \{f\colon X\to Y :
+  f(S) \subseteq T\}$ (fonctions envoyant une solution de $(X,S)$ en
+  une solution de $(Y,T)$)
+\item $\dottedtop = (\bullet,\{\bullet\})$
+\quad\itempoint $\dottedbot = (\bullet, \varnothing)$
+\end{itemize}
+
+\medskip
+
+\itempoint Si $\varphi(A_1,\ldots,A_r)$ est une formule
+propositionnelle et $(X_1,S_1),\ldots,(X_r,S_r)$ des problèmes finis,
+on définit le problème $\dot\varphi((X_1,S_1),\ldots,(X_r,S_r))$ de
+façon évidente (par induction).
+
+\end{frame}
+%
+\begin{frame}
+\frametitle{Sémantique des problèmes finis}
+
+\itempoint Si $\varphi(A_1,\ldots,A_r)$ est une formule
+propositionnelle et $(X_1,S_1),\ldots,(X_r,S_r)$ des problèmes finis,
+noter que l'ensemble $Z$ de candidats de du problème
+$\dot\varphi((X_1,S_1),\ldots,(X_r,S_r))$ ne dépend que des ensembles
+$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
+$S_1,\ldots,S_r$ (sous-ensembles respectifs de $X_1,\ldots,X_r$).
+
+\medskip
+
+\itempoint Il s'agit d'une autre façon de donner un sens précis à
+l'interprétation de Brouwer-Heyting-Kolmogorov, cette fois sur des
+ensembles finis (donc pas de question de calculabilité).
+
+\medskip
+
+\itempoint\textbf{Théorème} (Medvedev) : cette sémantique est correcte
+pour le calcul propositionnel intuitionniste.
+
+\medskip
+
+{\footnotesize Elle n'est pas complète : p.ex., $(\neg A \Rightarrow
+  B_1) \lor (\neg A \Rightarrow B_2) \Rightarrow (\neg A \Rightarrow
+  (B_1\lor B_2))$ (Kreisel-Putnam, déjà évoqué) ou bien $((\neg\neg A
+  \Rightarrow A) \Rightarrow (A\lor\neg A)) \Rightarrow (\neg
+  A\lor\neg\neg A)$ (Scott) sont Medvedev-valides mais non
+  démontrables.\par}
+
+\end{frame}
+%
 % TODO:
 % - inférence de type de Hindley-Milner
 %