\input{preamble.tex}

\title{Übung 11: Aussagen über TMs und PCP}
\subtitle{Theoretische Informatik Sommersemester 2013}
\author{\href{mailto:markus.kaiser@in.tum.de}{Markus Kaiser}}

\begin{document}

\begin{frame}
    \titlepage
\end{frame}

\begin{frame}
    \frametitle{Spezielles Halteproblem}
    \setbeamercovered{dynamic}

    \begin{definition}[Spezielles Halteproblem]
        Gegeben ein \structure{Wort} $w \in \left\{ 0, 1 \right\}^*$.\\
        Hält \alert{$M_w$} bei Eingabe \alert{$w$}?
        \[\alert{K} := \left\{ w \mid M_w[w]\downarrow \right\}\]
    \end{definition}

    \begin{theorem}[]
        Das spezielle Halteproblem ist \alert{nicht entscheidbar}.
    \end{theorem}

    \vfill

    \begin{itemize}
        \item Hält eine Turingmaschine mit sich selbst als Eingabe?
        \item $w$ ist die \structure{Gödelisierung} von $M_w$.
        \item $K$ ist semi-entscheidbar, $\overline{K}$ \alert{nicht}.
    \end{itemize}
\end{frame}

\begin{frame}
    \frametitle{Allgemeines Halteproblem}
    \setbeamercovered{dynamic}

    \begin{definition}[Allgemeines Halteproblem]
        Gegeben \structure{Wörter} $w, x \in \left\{ 0, 1 \right\}^*$.\\
        Hält \alert{$M_w$} bei Eingabe \alert{$x$}?
        \[\alert{H} := \left\{ w\#x \mid M_w[x]\downarrow \right\}\]
    \end{definition}

    \begin{theorem}[]
        Das allgemeine Halteproblem ist \alert{nicht entscheidbar}.
    \end{theorem}

    \vfill

    \begin{itemize}
        \item Es ist $K \leq H$. Warum?
    \end{itemize}
\end{frame}

\begin{frame}
    \frametitle{Rekursive Aufzählbarkeit}
    \setbeamercovered{dynamic}

    \begin{definition}[Rekursiv aufzählbar]
        Eine Menge $A$ heißt \alert{rekursiv aufzählbar} wenn $A = \emptyset$ oder es eine \alert{berechenbare} totale Funktion $f : \N \to A$ gibt, so dass
        \[A = \left\{ f(0), f(1), \ldots \right\} = \bigcup_{n \in \N} \left\{ f(n) \right\}\]
    \end{definition}

    \vfill

    \structure{Äquivalent:}
    \begin{itemize}
        \item $A$ rekursiv aufzählbar
        \item $A$ semi-entscheidbar, also $\chi'_A$ berechenbar
        \item $A=L(M)$ für eine TM $M$
        \item $A$ ist Bild oder Urbild einer berechenbaren Funktion
    \end{itemize}
\end{frame}

\begin{frame}
    \frametitle{Satz von Rice}
    \setbeamercovered{dynamic}

    \begin{theorem}[Rice]
        Sei $F$ eine Menge berechenbarer Funktionen.\\
        Sei weder $F = \emptyset$ noch $F = \text{alle ber. Funktionen}$ (\alert{$F$ nicht trivial}).\\
        Dann ist \alert{unentscheidbar}, ob die von einer gegebenen TM $M_w$ berechnete Funktion in $F$ ist, also ob \alert{$\varphi_w \in F$}.
    \end{theorem}

    \begin{itemize}
        \item Nicht-triviale \alert{semantische} Eigenschaften von Programmen sind unentscheidbar.
        \item \alert{Termination} ist unentscheidbar.
    \end{itemize}

    \vfill

    \structure{Rice-Shapiro:}
    \begin{itemize}
        \item Termination ist nicht semi-entscheidbar.
        \item Nicht-Termination ist nicht semi-entscheidbar.
    \end{itemize}
\end{frame}

\begin{frame}
    \frametitle{PCP}
    \setbeamercovered{dynamic}

    \begin{definition}[Postsches Korrespondenzproblem]
        Gegeben \structure{endliche Folge} $(x_1, y_1), \ldots, (x_k, y_k)$ mit $x_i, y_i \in \Sigma^+$.\\
        Gibt es eine \alert{Folge von Indizes} $i_1, \ldots, i_n \in \left\{ 1, \ldots, k \right\}$ mit \alert{\[x_{i_1}, \ldots, x_{i_n} = y_{i_1}, \ldots, y_{i_n}\]}
    \end{definition}

    \vfill

    \begin{center}
        \begin{tikzpicture}
            \begin{scope}[start chain, node distance=2em]
                \node[tape, active] {\pcp{$x_i$}{$y_i$}};
                \node[tape] (a) {\pcp{$001$}{$00$}};
                \node[tape] (b) {\pcp{$10$}{$11$}};
                \node[tape] (c) {\pcp{$1$}{$10$}};
            \end{scope}
            \node[below of=a] {$1$};
            \node[below of=b] {$2$};
            \node[below of=c] {$3$};
        \end{tikzpicture}
    \end{center}

    \vfill

    \begin{theorem}[]
        Das PCP ist \alert{unentscheidbar}, aber semi-entscheidbar.
    \end{theorem}
\end{frame}

\begin{frame}
    \frametitle{PCP lösen}
    \setbeamercovered{dynamic}

    \begin{block}{Idee}
        \alert{Mögliche Lösungen} aufzählen, richtige Lösungen identifizieren
    \end{block}

    \begin{center}
        \begin{tikzpicture}
            \begin{scope}[start chain, node distance=2em]
                \node[tape, active] {\pcp{$x_i$}{$y_i$}};
                \node[tape] (a) {\pcp{$001$}{$00$}};
                \node[tape] (b) {\pcp{$01$}{$10$}};
                \node[tape] (c) {\pcp{$1$}{$11$}};
            \end{scope}
            \node[below of=a] {$1$};
            \node[below of=b] {$2$};
            \node[below of=c] {$3$};
        \end{tikzpicture}

        \vspace{2em}

        \begin{tikzpicture}[grow=right, level distance = 2cm]
            \tikzstyle{every node} = []
            \tikzstyle{residual} = [rectangular, thin, fill=tumgreen!10, font=\scriptsize]
            \tikzstyle{edge from parent} = [every edge]

            \tikzstyle{level 1} = [sibling distance = 1.7cm]
            \tikzstyle{level 2} = [sibling distance = 1.1cm]

            \node[residual] {}
            child {
                node[residual] {\pcp{$1$}{}}
                child {
                    node[residual] {\pcp{$1$}{}}
                    child {
                        node[residual] {\pcp{$1$}{}}
                        child {
                            node[residual]{$\ldots$}
                            edge from parent
                        }
                        edge from parent
                        node[below] {$2$}
                    }
                    child {
                        node[residual, active] {\pcp{}{}}
                        edge from parent
                        node[above] {$3$}
                    }
                    edge from parent
                    node[below] {$2$}
                }
                child {
                    node[residual, active] {\pcp{}{}}
                    edge from parent
                    node[above] {$3$}
                }
                edge from parent
                node[below] {$1$}
            }
            child {
                node[residual]{\pcp{}{$1$}}
                child {
                    node[residual]{\pcp{}{$11$}}
                    child {
                        node[residual]{$\ldots$}
                        edge from parent
                        node[above] {$3$}
                    }
                    edge from parent
                    node[above] {$3$}
                }
                edge from parent
                node[above] {$3$}
            };

            \uncover<2>{\node at (10cm, 0) {$L = \left\{ (12^*3)^+ \right\}$};}
        \end{tikzpicture}
    \end{center}
\end{frame}

\end{document}