summaryrefslogtreecommitdiffstats
path: root/transp-inf110-01-calc.tex
diff options
context:
space:
mode:
authorDavid A. Madore <david+git@madore.org>2023-11-02 16:20:06 +0100
committerDavid A. Madore <david+git@madore.org>2023-11-02 16:20:06 +0100
commit840c08fb0747fcef6e1102bd2c7165bba89d0a44 (patch)
tree46376597aa9591e8ed2dee88f0498a9162e955ef /transp-inf110-01-calc.tex
parente7c7588f644dfabec67c0070dbf446d6fc0d4c01 (diff)
downloadinf110-lfi-840c08fb0747fcef6e1102bd2c7165bba89d0a44.tar.gz
inf110-lfi-840c08fb0747fcef6e1102bd2c7165bba89d0a44.tar.bz2
inf110-lfi-840c08fb0747fcef6e1102bd2c7165bba89d0a44.zip
Many-to-one reduction, and a new proof of Rice's theorem.
Diffstat (limited to 'transp-inf110-01-calc.tex')
-rw-r--r--transp-inf110-01-calc.tex161
1 files changed, 160 insertions, 1 deletions
diff --git a/transp-inf110-01-calc.tex b/transp-inf110-01-calc.tex
index 8eaa54e..6eaf10d 100644
--- a/transp-inf110-01-calc.tex
+++ b/transp-inf110-01-calc.tex
@@ -2553,7 +2553,7 @@ Exemples :
\end{frame}
%
\begin{frame}
-\frametitle{Le théorème de Rice : preuve}
+\frametitle{Le théorème de Rice : preuve par théorème de récursion}
{\footnotesize $\textbf{PR}^{(1)} = \{f \colon
\mathbb{N}\dasharrow\mathbb{N} : f\text{~calculable}\}$\par}
@@ -2596,6 +2596,165 @@ $\Phi(e) = f$ donc $e \in \Phi^{-1}(F)$, une contradiction.\qed
\end{frame}
%
+\begin{frame}
+\frametitle{Réductions : introduction}
+
+\itempoint Situation typique : on veut montrer qu'une question $D$
+(« problème de décision », souvent déjà semi-décidable) est
+indécidable. Ceci se fait typiquement en \alert{réduisant le problème
+ de l'arrêt} à $D$, c'est-à-dire :
+
+\bigskip
+
+\textcolor{teal}{« Supposons par l'absurde que $D$ soit décidable,
+ c'est-à-dire que j'ai un algorithme qui répond à la question $D$
+ (comprendre : “$n\in D$ ?”).}
+
+\smallskip
+
+\textcolor{teal}{Je montre qu'\alert{en utilisant cet algorithme} je
+ peux résoudre le problème de l'arrêt.}
+
+\smallskip
+
+\textcolor{teal}{Ceci est une contradiction (car le problème de
+ l'arrêt est indécidable),}
+
+\textcolor{teal}{donc $D$ est indécidable. »}
+
+\bigskip
+
+\itempoint Les notions de réduction formalisent cet argument :
+intuitivement,
+
+\centerline{« $A$ se réduit à $B$ »}
+
+\centerline{$\Longleftrightarrow$}
+
+\centerline{« si $B$ est décidable alors $A$ est décidable »}
+
+\centerline{(mais constructivement)}
+
+\end{frame}
+%
+\begin{frame}
+\frametitle{Le théorème de Rice : preuve par réduction (1/2)}
+
+{\footnotesize $\textbf{PR}^{(1)} = \{f \colon
+ \mathbb{N}\dasharrow\mathbb{N} : f\text{~calculable}\}$\par}
+
+\smallskip
+
+\itempoint\textbf{Théorème} (Rice) : si $F \subseteq
+\textbf{PR}^{(1)}$ est tel que $F \neq \varnothing$ et $F \neq
+\textbf{PR}^{(1)}$, alors $\Phi^{-1}(F) := \{e \in \mathbb{N} :
+\varphi^{(1)}_e \in F\}$ \emph{n'est pas décidable}.
+
+\bigskip
+
+\underline{Preuve :} Soit $F \subseteq \textbf{PR}^{(1)}$ avec $F \neq
+\varnothing$ et $F \neq \textbf{PR}^{(1)}$. Quitte à remplacer $F$
+par $\complement F$, o.p.s. ${\uparrow} \not\in F$ où $\uparrow$ est
+la fonction nulle part définie. Soit $f\in F$ où $f =
+\varphi^{(1)}_a$.
+
+\smallskip
+
+Pour $(e,x) \in \mathbb{N}^2$, considérons l'algorithme suivant,
+prenant en entrée $m \in \mathbb{N}$ :
+\begin{itemize}
+\item simuler $\varphi^{(1)}_e(x)$ avec la machine universelle, puis,
+ si l'exécution termine,
+\item calculer $f(m) = \varphi^{(1)}_a(m)$ et (si l'exécution termine)
+ renvoyer sa valeur.
+\end{itemize}
+
+\smallskip
+
+Soit $b(e,x)$ le code de l'algorithme qu'on vient de décrire :
+\centerline{$\varphi^{(1)}_{b(e,x)} = f$ si $\varphi^{(1)}_e(x)\downarrow$
+\quad et\quad
+$\varphi^{(1)}_{b(e,x)} = {\uparrow}$ si $\varphi^{(1)}_e(x)\uparrow$}
+notamment $\varphi^{(1)}_{b(e,x)} \in F$ ssi $\varphi^{(1)}_e(x)\downarrow$
+\textcolor{brown}{($\leftarrow$ c'est là la réduction)}.\hfill …/…
+
+\end{frame}
+%
+\begin{frame}
+\frametitle{Le théorème de Rice : preuve par réduction (2/2)}
+
+{\footnotesize $\textbf{PR}^{(1)} = \{f \colon
+ \mathbb{N}\dasharrow\mathbb{N} : f\text{~calculable}\}$ ; on a
+ supposé $F \subseteq \textbf{PR}^{(1)}$ avec ${\uparrow}\not\in F$
+ et $f \in F$\par}
+
+\smallskip
+
+On a construit (transp. précédent) un $b(e,x)$, avec $b \colon
+\mathbb{N}^2 \to \mathbb{N}$ calculable (même p.r.) tel que
+$\varphi^{(1)}_{b(e,x)} \in F$ ssi $\varphi^{(1)}_e(x)\downarrow$,
+c'est-à-dire
+\[
+b(e,x) \in \Phi^{-1}(F) \;\Longleftrightarrow\; (e,x) \in \mathscr{H}
+\]
+où $\mathscr{H} := \{(e,x)\in\mathbb{N}^2 : \varphi_e(x)\downarrow\}$
+est le problème de l'arrêt.
+
+\medskip
+
+Si $\Phi^{-1}(F)$ était décidable, alors $\mathscr{H}$ le serait aussi, par
+l'algorithme :
+\begin{itemize}
+\item donnés $e,x$, calculer $b(e,x)$, décider si $b(e,x) \in \Phi^{-1}(F)$,
+\item si oui, répondre « oui », sinon répondre « non ».
+\end{itemize}
+
+\smallskip
+
+Or $\mathscr{H}$ n'est pas décidable, donc $\Phi^{-1}(F)$ non plus.\qed
+
+\bigskip
+
+On dit qu'on a \alert{réduit le problème de l'arrêt} à $\Phi^{-1}(F)$
+(\alert{via} la fonction $b$).
+
+\end{frame}
+%
+\begin{frame}
+\frametitle{Réduction « many-to-one »}
+
+\textbf{Définition :} Si $A,B\subseteq\mathbb{N}$, on note $A
+\mathrel{\leq_\mathrm{m}} B$ lorsqu'il existe $\rho \colon \mathbb{N}
+\to \mathbb{N}$ \emph{calculable totale} telle que
+\[
+\rho(m) \in B \;\Longleftrightarrow\; m \in A
+\]
+{\footnotesize (c'est-à-dire $A = \rho^{-1}(B)$)}.
+
+\bigskip
+
+\textcolor{blue}{\textbf{Intuitivement :}} si j'ai un gadget qui
+répond à la question “$n \in B$ ?”, je peux répondre à la question “$m
+\in A$ ?” en transformant $m$ en $\rho(n)$ et en utilisant le gadget.
+
+\bigskip
+
+\textbf{Clairement}, si $A \mathrel{\leq_\mathrm{m}} B$ avec $B$
+décidable, alors $A$ est décidable. \emph{Notamment}, si $\mathscr{H}
+\mathrel{\leq_\mathrm{m}} D$ alors $D$ \emph{n'est pas} décidable.
+
+\bigskip
+
+{\footnotesize La relation $\mathrel{\leq_\mathrm{m}}$ est réflexive
+ et transitive (c'est un « préordre ») ; la relation
+ $\mathrel{\equiv_\mathrm{m}}$ définie par $A
+ \mathrel{\equiv_\mathrm{m}} B$ ssi $A \mathrel{\leq_\mathrm{m}} B$
+ et $B \mathrel{\leq_\mathrm{m}} A$ est une relation d'équivalence,
+ les classes pour laquelle s'appellent « degrés many-to-one » et sont
+ partiellement ordonnés par $\mathrel{\leq_\mathrm{m}}$.\par}
+
+\end{frame}
+%
\section{Le \texorpdfstring{$\lambda$}{lambda}-calcul non typé}
\begin{frame}
\frametitle{Le $\lambda$-calcul : aperçu}