\documentclass[a4paper,10pt]{scrartcl}
%\documentclass[a4paper,10pt]{scrreprt}
\setlength{\topmargin}{-2.5cm}
\setlength{\oddsidemargin}{-1.5cm}
\setlength{\evensidemargin}{-1.5cm}
\setlength{\textwidth}{19cm}
\setlength{\textheight}{26.5cm}

\usepackage[active]{srcltx}
\usepackage[german]{babel}
\usepackage[utf8]{inputenc}
\usepackage[%
pdftex,%
a4paper,%
%colorlinks=true,%
%linkcolor=black%
]{hyperref}
\usepackage{enumitem}
\usepackage{amsmath}
\usepackage{bbm}
\usepackage{amssymb}
\usepackage{graphicx}
%\usepackage{trfsigns}
\usepackage[usenames]{color}
%\usepackage{MnSymbol}

% Shortcuts für Matrizen, '&' und '\\' gelten wie gewohnt
\newcommand{\mtrx}[1]{\begin{matrix}#1\end{matrix}} % ( normal Matrix )
\newcommand{\smtrx}[1]{\begin{smallmatrix}#1\end{smallmatrix}} % ( small Matrix )
\newcommand{\pmtrx}[1]{\begin{pmatrix}#1\end{pmatrix}}	% ( (...) )
\newcommand{\bmtrx}[1]{\begin{bmatrix}#1\end{bmatrix}}	% ( [...] )
\newcommand{\Bmtrx}[1]{\begin{Bmatrix}#1\end{Bmatrix}}	% ( {...} )
\newcommand{\e}{\text{e}}
\newcommand{\im}{\text{i}}
\newcommand{\ceq}{\mathrel{\mathop:}=}

% code box
\setlength{\fboxrule}{1.2pt}
%\definecolor{codeFrame}{rgb}{0.1,0.1,0.1}
\definecolor{codeBg}{rgb}{0.96,0.96,0.96}
%\definecolor{codeFg}{rgb}{0.2,0.2,0.2}
%\definecolor{brown}{rgb}{0.6,0.3,0.3}
\definecolor{grey}{rgb}{0.4,0.4,0.4}
\definecolor{dgrey}{rgb}{0.2,0.2,0.2}
%\newcommand{\codebox}[1]{\fcolorbox{codeFrame}{codeBg}{\texttt{#1}}}
%\newcommand{\code}[2][codeFg]{\codebox{\textcolor{#1}{#2}}}

% paragraph settings, http://docutils.sourceforge.net/docs/user/latex.html
\setlength{\parindent}{0pt}
\setlength{\parskip}{6pt plus 2pt minus 1pt}

\begin{document}

%\section{Berechenbarkeit}
\subsection*{Spezielles Halteproblem / Selbstanwendbarkeitsproblem}
\[ K := \{ w | w \in \{ 0, 1 \}^*, M_w \text{ hält auf $w$ bzw. $h_w(w)$ ist definiert} \} \]
$K$ ist rekursiv aufzählbar, da $ch'_K$ berechenbar durch Simulation von $M_w$ auf $w$. \par
$K$ ist nicht berechenbar (Charakteristische Funktion nur semi-entscheidbar), da, wäre $K$ entscheidbar:
\begin{itemize}
	\item $E^* \setminus K$ semi-entscheidbare
	\item TM definiert durch Wort $x \in E^*$ hält auf $w \Leftrightarrow w \in E^* \setminus K$
	\item $h_x(w)$ definiert $\Leftrightarrow w \in E^* \setminus K$
	\item Für $h_x(x)$:
		\begin{eqnarray*}
			h_x(x) \text{ definiert } \Leftrightarrow& x \in K &\text{(Definition von $K$)} \\
			\Leftrightarrow& \text{ TM hält nicht auf $x$ } & \\
			\Leftrightarrow& h_x(x) \text{ nicht definiert } &\text{(Definition von TM)} \\
			\Leftrightarrow& x \in E^* \setminus K \Leftrightarrow x \not\in K &
		\end{eqnarray*}
	\item $\Rightarrow$ Annahme falsch $\Rightarrow K$ nicht entscheidbar (nur utm-Eigenschaft benutzt)
\end{itemize}

\subsection*{Allgemeines Halteproblem}
\[ H:= \{ w \$ x \;\vert\; w \in \{ 0, 1 \}^*, \$ \not\in E^*, \text{ $M_w$ hält auf $x$ an } \} \]
$H$ ist rekursiv aufzählbar (utm-Eigenschaft $\Rightarrow$ Simulation von $M_w$ auf $x$ ($h_w(x)$)). \par
$H$ ist nicht entscheidbar, da
\begin{itemize}
	\item konstruiere berechenbare und totale Reduktionsfunktion $f: E^* \to E^* \$ E^*$, mit $f(w) \mapsto w \$ w$
	\item $\Rightarrow K \leq H \,\Rightarrow\, H$ nicht entscheidbar
\end{itemize}

\subsection*{Satz von Rice}
Sei $R$ Klasse der Turing-berechenbaren Wortfunktionen über $E$, dann für $\varnothing \neq S \subsetneq R$:
\[ C(S) \ceq \{ w \;\vert\; w \in \{ 0, 1 \}^*, h_w \in S \} \]
$C(S)$ ist nicht entscheidbar (unentscheidbar). O.B.d.A. $ud \in S$ (ansonsten setze $q \in S$):
\begin{itemize}
	\item sei Funktion $q \in R \setminus S$, $Q$ eine TM für $q$
	\item Funktion $g$ beschreibe $Q$ mit Eingabe \texttt{w\#x}:
		\begin{enumerate}
			\item Simuliere $M_w$ auf $w$
			\item Simuliere $Q$ mit Eingabe $x$
		\end{enumerate}
	\item mit smn: $\exists r: E^* \to E^*$, sodass $g(w\#x) = h_{r(w)}(x)$ mit
		\begin{itemize}
			\item $M_w$ hält auf $w \Rightarrow g = q$
			\item $M_w$ hält nicht auf $w \Rightarrow g = ud$
		\end{itemize}
		\begin{eqnarray*}
			&\Rightarrow\qquad w \in K \quad\Rightarrow\quad h_{r(w)} = q &\quad\Rightarrow\quad h_{r(w)} \not\in S \quad\Rightarrow\quad r(w) \not\in C(S) \\
			&\wedge\qquad w \not\in K \quad\Rightarrow\quad h_{r(w)} = ud &\quad\Rightarrow\quad h_{r(w)} \in S \quad\Rightarrow\quad r(w) \in C(S)
		\end{eqnarray*}
\end{itemize}
$\Rightarrow r$ reduziert $E^* \setminus K$ auf $C(S)$ ($ud \not\in S$), bzw. $K \leq_r C(S)$ ($ud \in S$) $\quad\Rightarrow\quad C(S)$ nicht entscheidbar.

\paragraph{Folgerungen} Für (reale) Programme $P$ in der Regel unentscheidbar:
\begin{itemize}
	\item $\{\; f \;\vert\; f \text{ berechenbar und total } \}$ ($P$ hält immer)
	\item $\{\; g \;\}$ für gegebenes $g$ ($P$ berechnet genau $g$)
	\item $\{\; g \;\vert\; g(\varepsilon) = \varepsilon \;\}$ ($P$ erfüllt Spezifikation - hier $g(\varepsilon) = \varepsilon$)
\end{itemize}

\end{document}
