annotate notes/tex/computation.tex @ 27:f7bcd68a0c12

eigth sheet and notes; add hierarchy slides
author Markus Kaiser <markus.kaiser@in.tum.de>
date Fri, 06 Jun 2014 17:13:58 +0200
parents efd13093bd47
children b56fe50e0132
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
1
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
1 \defineUnit{tmdefinition}{%
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
2 \begin{frame}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
3 \frametitle{Turingmaschinen}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
4 \setbeamercovered{dynamic}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
5
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
6 \begin{definition}[Turingmaschine]
27
f7bcd68a0c12 eigth sheet and notes; add hierarchy slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents: 6
diff changeset
7 Eine deterministische \structure{Turingmaschine (TM)} ist ein Tupel $M = (Q, \Sigma, \Gamma, \delta, q_0, \square, F)$ aus einer/einem
1
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
8 \begin{itemize}
27
f7bcd68a0c12 eigth sheet and notes; add hierarchy slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents: 6
diff changeset
9 \item endlichen Menge von \structure{Zuständen} $Q$
f7bcd68a0c12 eigth sheet and notes; add hierarchy slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents: 6
diff changeset
10 \item endlichen \structure{Eingabealphabet} $\Sigma$
f7bcd68a0c12 eigth sheet and notes; add hierarchy slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents: 6
diff changeset
11 \item endlichen \structure{Bandalphabet} $\Gamma$ mit $\Sigma \subset \Gamma$
f7bcd68a0c12 eigth sheet and notes; add hierarchy slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents: 6
diff changeset
12 \item \structure{Übergangsfunktion} $\delta : Q \times \Gamma \to Q \times \Gamma \times \left\{ L, R, N \right\}$
f7bcd68a0c12 eigth sheet and notes; add hierarchy slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents: 6
diff changeset
13 \item \structure{Startzustand} $q_0 \in Q$
f7bcd68a0c12 eigth sheet and notes; add hierarchy slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents: 6
diff changeset
14 \item \structure{Leerzeichen} $\square \in \Gamma \setminus \Sigma$
f7bcd68a0c12 eigth sheet and notes; add hierarchy slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents: 6
diff changeset
15 \item Menge von \structure{Endzuständen} $F \subseteq Q$
1
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
16 \end{itemize}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
17 \end{definition}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
18 \end{frame}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
19 }
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
20
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
21 \defineUnit{tmvisualisierung}{%
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
22 \begin{frame}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
23 \frametitle{Turingmaschinen}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
24 \setbeamercovered{dynamic}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
25
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
26 \begin{definition}[Turingmaschine]
27
f7bcd68a0c12 eigth sheet and notes; add hierarchy slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents: 6
diff changeset
27 Eine deterministische \structure{Turingmaschine (TM)} ist ein Tupel $M = (Q, \Sigma, \Gamma, \delta, q_0, \square, F)$ aus einer/einem
1
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
28 \begin{itemize}
27
f7bcd68a0c12 eigth sheet and notes; add hierarchy slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents: 6
diff changeset
29 \item \structure{Übergangsfunktion} $\delta : Q \times \Gamma \to Q \times \Gamma \times \left\{ L, R, N \right\}$
1
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
30 \end{itemize}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
31 \end{definition}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
32
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
33 \vfill
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
34
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
35 \begin{center}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
36 \begin{tikzpicture}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
37 % Tape
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
38 \begin{scope}[start chain, node distance=0]
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
39 \node[on chain] {\ldots};
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
40 \node[tape] {$\square$};
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
41 \node[tape] (l) {$\square$};
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
42 \node[tape] {$0$};
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
43 \node[tape] {$1$};
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
44 \node<1>[tape, active] (a){$0$};
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
45 \node<2>[tape] (a){$1$};
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
46 \node<1>[tape] (b){$0$};
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
47 \node<2>[tape, active] (b){$0$};
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
48 \node[tape] {$\square$};
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
49 \node[on chain] {\ldots};
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
50 \end{scope}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
51
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
52 % Head
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
53 \node<1> [head,yshift=-4mm] at (a.south) (head) {$q_0$};
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
54 \node<2> [head,yshift=-4mm] at (b.south) (head) {$q_1$};
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
55
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
56 % Machine
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
57 \node[machine, below=1.5cm of l] (machine) {Programm};
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
58 \draw[every edge] (machine) .. controls (3.5, -2) .. (head.south);
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
59
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
60 % Example-Transition
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
61 \node[yshift=5mm] at (current bounding box.north) {$\delta(q_0, 0) = (q_1, 1, R)$};
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
62 \end{tikzpicture}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
63 \end{center}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
64 \end{frame}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
65 }
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
66
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
67 \defineUnit{tmkonfiguration}{%
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
68 \begin{frame}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
69 \frametitle{Turingmaschinen}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
70 \setbeamercovered{dynamic}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
71
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
72 \begin{definition}[Konfiguration]
27
f7bcd68a0c12 eigth sheet and notes; add hierarchy slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents: 6
diff changeset
73 Eine \structure{Konfiguration} ist ein Tripel $(\alpha, q, \beta) \in \Gamma^* \times Q \times \Gamma^*$. \\
1
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
74 Dies modelliert eine TM mit:
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
75 \begin{itemize}
27
f7bcd68a0c12 eigth sheet and notes; add hierarchy slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents: 6
diff changeset
76 \item \structure{Bandinhalt} $\ldots\square\alpha\beta\square\ldots$
f7bcd68a0c12 eigth sheet and notes; add hierarchy slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents: 6
diff changeset
77 \item \structure{Zustand} $q$
f7bcd68a0c12 eigth sheet and notes; add hierarchy slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents: 6
diff changeset
78 \item Kopf auf dem \structure{ersten Zeichen} von $\beta\square$
1
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
79 \end{itemize}
27
f7bcd68a0c12 eigth sheet and notes; add hierarchy slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents: 6
diff changeset
80 Die \structure{Startkonfiguration} bei Eingabe $w \in \Sigma^*$ ist $(\epsilon, q_0, w)$.
1
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
81 \end{definition}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
82
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
83 \vfill
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
84
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
85 \only<1> {
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
86 \begin{center}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
87 \begin{tikzpicture}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
88 % Tape
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
89 \begin{scope}[start chain, node distance=0]
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
90 \node[on chain] {\ldots};
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
91 \node[tape] {$\square$};
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
92 \node[tape] (l) {$\square$};
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
93 \node[tape] {$0$};
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
94 \node[tape] {$1$};
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
95 \node[tape] (a){$1$};
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
96 \node[tape, active] (b){$0$};
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
97 \node[tape] {$\square$};
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
98 \node[on chain] {\ldots};
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
99 \end{scope}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
100
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
101 % Head
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
102 \node [head,yshift=-4mm] at (b.south) (head) {$q_1$};
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
103
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
104 % Machine
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
105 \node[below=1.5cm of l] (machine) {};
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
106 \draw[every edge, dashed] (machine) .. controls (3.5, -2) .. (head.south);
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
107
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
108 % Example-Transition
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
109 \node[yshift=5mm] at (current bounding box.north) {$(011,q_1,0)$};
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
110 \end{tikzpicture}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
111 \end{center}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
112 }
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
113
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
114 \only<2> {
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
115 \begin{definition}[Akzeptanz]
27
f7bcd68a0c12 eigth sheet and notes; add hierarchy slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents: 6
diff changeset
116 Eine TM $M$ \structure{akzeptiert} die Sprache
1
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
117 \[ L(M) = \left\{ w \in \Sigma^* \mid \exists \alert{f \in F}, \alpha, \beta \in \Gamma^* . (\epsilon, q_0, w) \rightarrow_M^* (\alpha, \alert{f}, \beta) \right\} \]
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
118 \end{definition}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
119 }
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
120 \end{frame}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
121 }
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
122
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
123 \defineUnit{ndtm}{%
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
124 \begin{frame}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
125 \frametitle{Nichtdeterministische TM}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
126 \setbeamercovered{dynamic}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
127
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
128 \begin{definition}[Nichtdeterministische Turingmaschine]
27
f7bcd68a0c12 eigth sheet and notes; add hierarchy slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents: 6
diff changeset
129 Eine \structure{nichtdeterministische} Turingmaschine (TM) ist ein Tupel $M = (Q, \Sigma, \Gamma, \delta, q_0, \square, F)$ aus einer/einem
1
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
130 \begin{itemize}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
131 \item \ldots
27
f7bcd68a0c12 eigth sheet and notes; add hierarchy slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents: 6
diff changeset
132 \item \structure{Übergangsfunktion} $\delta : Q \times \Gamma \to \mathcal{P} \left( Q \times \Gamma \times \left\{ L, R, N \right\} \right)$
1
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
133 \item \ldots
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
134 \end{itemize}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
135 \end{definition}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
136
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
137 \vfill
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
138
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
139 \begin{theorem}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
140 Zu jeder nichtdeterministischen TM $N$ gibt es eine deterministische TM $M$ mit \alert{$L(N) = L(M)$}.
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
141 \end{theorem}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
142 \end{frame}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
143 }
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
144
27
f7bcd68a0c12 eigth sheet and notes; add hierarchy slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents: 6
diff changeset
145 \defineUnit{lba}{%
f7bcd68a0c12 eigth sheet and notes; add hierarchy slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents: 6
diff changeset
146 \begin{frame}
f7bcd68a0c12 eigth sheet and notes; add hierarchy slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents: 6
diff changeset
147 \frametitle{Linear Beschränkte Automaten}
f7bcd68a0c12 eigth sheet and notes; add hierarchy slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents: 6
diff changeset
148
f7bcd68a0c12 eigth sheet and notes; add hierarchy slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents: 6
diff changeset
149 \begin{definition}[Linear Beschränkte Automaten]
f7bcd68a0c12 eigth sheet and notes; add hierarchy slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents: 6
diff changeset
150 Eine TM heißt \structure{linear beschränkt (LBA)}, wenn sie den Bereich des Bandes, auf dem das Eingabewort steht, niemals verlässt.
f7bcd68a0c12 eigth sheet and notes; add hierarchy slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents: 6
diff changeset
151 \end{definition}
f7bcd68a0c12 eigth sheet and notes; add hierarchy slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents: 6
diff changeset
152
f7bcd68a0c12 eigth sheet and notes; add hierarchy slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents: 6
diff changeset
153 \vfill
f7bcd68a0c12 eigth sheet and notes; add hierarchy slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents: 6
diff changeset
154
f7bcd68a0c12 eigth sheet and notes; add hierarchy slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents: 6
diff changeset
155 \begin{theorem}[]
f7bcd68a0c12 eigth sheet and notes; add hierarchy slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents: 6
diff changeset
156 Die \structure{linear beschränkten NDTMs} akzeptieren genau die Klasse der \alert{kontextsensitiven Sprachen (Typ 1)}.
f7bcd68a0c12 eigth sheet and notes; add hierarchy slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents: 6
diff changeset
157 \end{theorem}
f7bcd68a0c12 eigth sheet and notes; add hierarchy slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents: 6
diff changeset
158 \end{frame}
f7bcd68a0c12 eigth sheet and notes; add hierarchy slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents: 6
diff changeset
159 }
f7bcd68a0c12 eigth sheet and notes; add hierarchy slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents: 6
diff changeset
160
1
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
161 \defineUnit{chomsky}{%
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
162 \begin{frame}[c]
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
163 \frametitle{Chomsky-Hierarchie}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
164 \setbeamercovered{dynamic}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
165
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
166 \begin{center}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
167 \begin{tikzpicture}[auto]
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
168 \tikzstyle{rect} = [thick];
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
169 \tikzstyle{caption} = [align=left, anchor=north west];
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
170
3
624c6e0e4383 first slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents: 1
diff changeset
171 \chomsky{tumlightblue}{}{0}{Alle formalen Sprachen};
27
f7bcd68a0c12 eigth sheet and notes; add hierarchy slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents: 6
diff changeset
172 \chomsky{tumred}{}{1}{Typ 0 - Rekursiv aufzählbar\\Grammatik\\Turingmaschine, WHILE-Programm, $\mu$-rekursive Funktion};
f7bcd68a0c12 eigth sheet and notes; add hierarchy slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents: 6
diff changeset
173 \chomsky{tumblue}{}{2}{Typ 1 - Kontextsensitiv\\Längenmonotone Grammatik\\Linear Beschränkter Automat (LBA)};
f7bcd68a0c12 eigth sheet and notes; add hierarchy slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents: 6
diff changeset
174 \chomsky{tumorange}{}{3}{Typ 2 - Kontextfrei\\Links nur ein Nichtterminal\\Kellerautomat (PDA)};
f7bcd68a0c12 eigth sheet and notes; add hierarchy slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents: 6
diff changeset
175 \chomsky{tumgreen}{}{4}{Typ 3 - Regulär\\Links- / Rechtsreguläre Grammatik\\DFA, NFA, RE};
1
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
176 \end{tikzpicture}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
177 \end{center}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
178 \end{frame}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
179 }
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
180
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
181 \defineUnit{berechenbarkeit}{%
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
182 \begin{frame}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
183 \frametitle{Berechenbarkeit}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
184 \setbeamercovered{dynamic}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
185
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
186 \begin{definition}[Intuitive Berechenbarkeit]
6
efd13093bd47 use structures instead of alerts
Markus Kaiser <markus.kaiser@in.tum.de>
parents: 3
diff changeset
187 Eine Funktion $f : \N^k \to \N$ heißt \structure{intuitiv berechenbar}, wenn es einen Algorithmus gibt, der bei Eingabe $(n_1, \ldots, n_k) \in \N^k$
1
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
188 \begin{itemize}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
189 \item nach \alert{endlich vielen Schritten} mit Ergebnis $f(n_1, \ldots, n_k)$ hält, falls $f(\ldots)$ definiert ist,
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
190 \item und \alert{nicht terminiert}, falls $f(\ldots)$ nicht definiert ist.
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
191 \end{itemize}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
192 \end{definition}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
193
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
194 \vfill
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
195
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
196 \begin{block}{Churchsche These (nicht beweisbar)}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
197 Turing-Maschinen können genau \alert{alle} intuitiv berechenbaren Funktionen berechnen.
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
198 \end{block}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
199 \end{frame}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
200 }
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
201
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
202 \defineUnit{berechenbarkeitbeispiel}{%
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
203 \begin{frame}[c]
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
204 \frametitle{Berechenbarkeit}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
205 \setbeamercovered{dynamic}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
206
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
207 \begin{example}[Berechenbarkeit]
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
208 Sind die folgenden Funktionen intuitiv berechenbar?
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
209
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
210 \begin{align*}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
211 f_1(n) &= \begin{cases}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
212 1 & \text{falls $n$ prim}\\
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
213 0 & \text{sonst}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
214 \end{cases} \\
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
215 f_2(n) &= \begin{cases}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
216 1 & \text{falls $n$ die ersten $n$ Ziffern von $\pi$ darstellt}\\
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
217 0 & \text{sonst}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
218 \end{cases} \\
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
219 f_3(n) &= \begin{cases}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
220 1 & \text{falls in $\pi$ $n$ Nullen am Stück vorkommen}\\
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
221 0 & \text{sonst}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
222 \end{cases}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
223 \end{align*}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
224 \end{example}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
225 \end{frame}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
226 }
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
227
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
228 \defineUnit{pr}{%
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
229 \begin{frame}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
230 \frametitle{Primitive Rekursion}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
231 \setbeamercovered{dynamic}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
232
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
233 \begin{definition}[Basisfunktionen]
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
234 \alert{Primitiv Rekursiv} sind:
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
235 \begin{itemize}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
236 \item Die konstante Funktion \alert{0}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
237 \item Die \alert{Nachfolgerfunktion} $s(n) = n + 1$
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
238 \item Die \alert{Projektionsfunktion} $\pi_i^k : \N^k \to \N, i \in [k]$
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
239 \[ \pi_i^k(x_1, \ldots, x_k) = x_i \]
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
240 \end{itemize}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
241 \end{definition}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
242
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
243 \begin{definition}[Komposition]
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
244 Sind $g$ und $h_i$ PR und $\bar{x} = (x_1, \ldots, x_n)$, dann ist auch \alert{$f$} PR:
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
245 \[ f(\bar{x}) = \alert{g(h_1(\bar{x}), \ldots, h_k(\bar{x}))} \]
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
246 \end{definition}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
247 \end{frame}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
248 }
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
249
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
250 \defineUnit{prrekursion}{%
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
251 \begin{frame}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
252 \frametitle{Primitive Rekursion}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
253 \setbeamercovered{dynamic}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
254 \begin{block}{Basisfunktionen und Komposition}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
255 Schon \alert{PR} sind:
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
256 \begin{itemize}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
257 \item Konstante: $0$
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
258 \item Nachfolger: $s(n) = n + 1$
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
259 \item Projektion: $\pi_i^k : \N^k \to \N$
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
260 \item Komposition: $f(\bar{x}) = g(h_1(\bar{x}), \ldots, h_k(\bar{x}))$
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
261 \end{itemize}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
262 \end{block}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
263 \begin{definition}[Primitive Rekursion] Das Schema der \alert{primitiven Rekursion} erzeugt aus $g$ und $h$ die Funktion \alert{$f$}: \begin{align*} f(0, \bar{x}) &= g(\bar{x}) \\ f(\alert{m + 1}, \bar{x}) &= h(f(\alert{m}, \bar{x}), \alert{m}, \bar{x}) \end{align*} \end{definition} \end{frame}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
264 }
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
265
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
266 \defineUnit{prprogramme}{%
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
267 \begin{frame}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
268 \frametitle{PR-Programme}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
269 \setbeamercovered{dynamic}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
270
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
271 U.a. diese Programme sind laut Vorlesung oder Übung PR:
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
272 \begin{itemize}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
273 \item $pred(x) = \max \left\{ 0, x - 1 \right\}$
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
274 \item \alert{$add(x, y) = x + y$}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
275 \item \alert{$x \dot{-} y = \max \left\{ 0, x - y \right\}$}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
276 \item \alert{$mult(x, y) = x \cdot y$}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
277 \item $div(x, y) = x \div y$ (Ganzzahldivision)
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
278 \item Die restliche einfache Arithmetik\ldots
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
279 \vspace{1.5em}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
280 \item $tower(n) = 2^{2^{2^{\iddots}}}$ mit $tower(4) = 2^{16}$
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
281 \item $sqr(x) = x^2$, $sqrt(x) = \sqrt{x}$
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
282 \item $c(x), p_1(x), p_2(x)$ (Cantorsche Paarungsfunktion)
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
283 \item $ifthen(n, a, b) = \begin{cases} a & n \neq 0 \\ b & n = 0 \end{cases}$
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
284 \end{itemize}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
285 \end{frame}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
286 }
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
287
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
288 \defineUnit{prerweitert}{%
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
289 \begin{frame}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
290 \frametitle{Erweitertes PR-Schema}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
291 \setbeamercovered{dynamic}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
292
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
293 \begin{definition}[Erweitertes PR-Schema]
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
294 Das \alert{erweiterte Schema der primitiven Rekursion} erlaubt
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
295 \begin{align*}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
296 f(0, \bar{x}) &= t_0 \\
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
297 f(m + 1, \bar{x}) &= t
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
298 \end{align*}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
299 wobei
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
300 \begin{itemize}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
301 \item $t_0$ enthält nur PR-Funktionen und die $x_i$
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
302 \item $t$ enthält nur \alert{$f(m, \bar{x})$}, PR Funktionen, \alert{$m$} und die $x_i$.
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
303 \end{itemize}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
304 \end{definition}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
305
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
306 \begin{theorem}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
307 Das erweiterte Schema der primitiven Rekursion führt nicht aus \alert{PR} heraus.
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
308 \end{theorem}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
309 \end{frame}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
310 }
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
311
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
312 \defineUnit{tmif}{%
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
313 \begin{frame}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
314 \frametitle{Programmieren mit TMs}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
315 \setbeamercovered{dynamic}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
316
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
317 Sind $f_1$ und $f_2$ Endzustände von $M$, so bezeichnet
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
318 \begin{center}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
319 \begin{tikzpicture}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
320 \node (M) at (0, 0) {$M$};
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
321 \node[above right=0.2cm and 1cm of M] (M1) {$M_1$};
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
322 \node[below right=0.2cm and 1cm of M] (M2) {$M_2$};
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
323 \coordinate[right of=M1] (M1s);
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
324 \coordinate[right of=M2] (M2s);
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
325
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
326 \draw[every edge] (-1, 0) -- (M);
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
327 \draw[every edge] (M) -- node[above left] {$f_1$} (M1);
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
328 \draw[every edge] (M) -- node[below left] {$f_2$} (M2);
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
329 \draw[every edge] (M1) -- (M1s);
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
330 \draw[every edge] (M2) -- (M2s);
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
331 \end{tikzpicture}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
332 \end{center}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
333 eine \alert{Fallunterscheidung}.\\
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
334 \begin{example}[Band=0?]
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
335 \begin{align*}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
336 \delta(q_0, 0) &= (q_0, 0, R) \\
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
337 \delta(q_0, \square) &= (ja, \square, L) \\
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
338 \delta(q_0, a) &= (nein, a, N) \qquad \text{für } a \neq 0, \square
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
339 \end{align*}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
340 \end{example}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
341 \end{frame}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
342 }
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
343
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
344 \defineUnit{while}{%
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
345 \begin{frame}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
346 \frametitle{WHILE-Programme}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
347 \setbeamercovered{dynamic}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
348
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
349 \begin{definition}[WHILE-Programm]
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
350 Syntax von \alert{WHILE-Programmen}.\\
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
351 Es ist $X \in \left\{ x_0, x_1, \ldots \right\}$ und $C \in \N$.
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
352 \begin{align*}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
353 P &\rightarrow X := X + C \\
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
354 &\mid X := X - C \\
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
355 &\mid P; P \\
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
356 &\mid \alert{\mathbf{WHILE}\ X \neq 0 \ \mathbf{DO}\ P \ \mathbf{END}} \\
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
357 &\mid \textcolor{gray}{\mathbf{LOOP}\ X \ \mathbf{DO}\ P \ \mathbf{END}} \\
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
358 &\mid \textcolor{gray}{\mathbf{IF}\ X = 0 \ \mathbf{DO}\ P \ \mathbf{ELSE}\ Q \ \mathbf{END}}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
359 \end{align*}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
360 \end{definition}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
361
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
362 \begin{itemize}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
363 \item Ausgabe steht in $x_0$, Eingaben in $x_1, \ldots, x_n$, Rest ist 0.
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
364 \item Semantik wie erwartet.
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
365 \end{itemize}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
366 \end{frame}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
367 }
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
368
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
369 \defineUnit{goto}{%
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
370 \begin{frame}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
371 \frametitle{GOTO-Programme}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
372 \setbeamercovered{dynamic}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
373
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
374 \begin{definition}[GOTO-Programm]
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
375 Syntax von \alert{GOTO-Programmen}.\\
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
376 Es ist $X \in \left\{ x_0, x_1, \ldots \right\}$ und $C \in \N$. \\
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
377 Alle Anweisungen haben eine Markierung \alert{$M_1 : A_1; M_2 : A_2$}.
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
378 \begin{align*}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
379 P &\rightarrow X := X + C \\
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
380 &\mid X := X - C \\
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
381 &\mid P; P \\
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
382 &\mid \mathbf{GOTO}\ M_i \\
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
383 &\mid \mathbf{IF}\ X = 0 \ \mathbf{GOTO}\ M_i \\
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
384 &\mid \mathbf{HALT}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
385 \end{align*}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
386 \end{definition}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
387
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
388 \begin{itemize}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
389 \item Ausgabe steht in $x_0$, Eingaben in $x_1, \ldots, x_n$, Rest ist 0.
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
390 \end{itemize}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
391 \end{frame}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
392 }
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
393
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
394 \defineUnit{loop}{%
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
395 \begin{frame}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
396 \frametitle{LOOP-Programme}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
397 \setbeamercovered{dynamic}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
398
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
399 \begin{definition}[LOOP-Programm]
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
400 Syntax von \alert{LOOP-Programmen}.\\
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
401 Es ist $X \in \left\{ x_0, x_1, \ldots \right\}$ und $C \in \N$.
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
402 \begin{align*}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
403 P &\rightarrow X := X + C \\
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
404 &\mid X := X - C \\
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
405 &\mid P; P \\
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
406 &\mid \mathbf{LOOP}\ X \ \mathbf{DO}\ P \ \mathbf{END} \\
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
407 &\mid \textcolor{gray}{\mathbf{IF}\ X = 0 \ \mathbf{DO}\ P \ \mathbf{ELSE}\ Q \ \mathbf{END}}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
408 \end{align*}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
409 \end{definition}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
410
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
411 \begin{itemize}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
412 \item Ausgabe steht in $x_0$, Eingaben in $x_1, \ldots, x_n$, Rest ist 0.
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
413 \item $\mathbf{LOOP}\ x_i \ \mathbf{DO}\ P \ \mathbf{END}$ führt $P$ genau $n$ mal aus, wobei $n$ der Anfangswert von $x_i$ ist. \alert{Zuweisungen an $x_i$ in $P$ ändern die Anzahl der Durchläufe nicht.}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
414 \end{itemize}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
415 \end{frame}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
416 }
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
417
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
418 \defineUnit{prmax}{%
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
419 \begin{frame}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
420 \frametitle{Beschränkte Operationen}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
421 \setbeamercovered{dynamic}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
422 \begin{definition}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
423 Ein Prädikat $P$ ist \alert{PR}, wenn es eine PR Funktion $\hat{P}$ gibt mit
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
424 \[\hat{P}(x) = 1 \Longleftrightarrow P(x)\]
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
425 \end{definition}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
426
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
427 \begin{definition}[Beschränkte Operationen]
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
428 Ist $P$ PR, dann auch
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
429 \begin{itemize}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
430 \item der \alert{beschränkte max-Operator}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
431 \[\max \left\{ x \alert{\leq n} \mid P(x) \right\}, \quad \max \left\{ \emptyset \right\} = 0\]
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
432 \item der \alert{beschränkte Existenzquantor}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
433 \[\exists x \alert{\leq n}. P(x)\]
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
434 \end{itemize}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
435 \end{definition}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
436 \end{frame}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
437 }
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
438
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
439 \defineUnit{murekursion}{%
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
440 \begin{frame}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
441 \frametitle{$\mu$-Rekursion}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
442 \setbeamercovered{dynamic}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
443
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
444 \begin{definition}[$\mu$-Operator]
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
445 Sei $f: \N^{k+1} \to \N$ eine Funktion.\\Der \alert{$\mu$-Operator} definiert eine neue Funktion $\mu f : \N^k \to \N$:
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
446 \[(\mu f)(\bar{x}) := \begin{cases} \min \left\{ n \in \N \mid \alert{f (n, \bar{x}) = 0}\right\} & \text{falls } n \text{ existent\alert{$^*$}} \\ \perp & \text{sonst}\end{cases}\]
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
447 \end{definition}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
448
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
449 \vfill
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
450
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
451 \begin{itemize}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
452 \item \alert{$^*$}Für alle \alert{$m \leq n$} muss $f$ definiert sein: $f(m, \bar{x}) \neq \perp$
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
453 \item PR + $\mu$ = $\mu$-Rekursion
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
454 \item In Pseudocode:
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
455 \begin{align*}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
456 \mu f(\bar{x}) &= find(0, \bar{x}) \\
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
457 find(n, \bar{x}) &= \mathbf{if}\ f(n, \bar{x}) = 0 \ \mathbf{then}\ n \ \mathbf{else}\ find(n+1, \bar{x})
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
458 \end{align*}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
459 \end{itemize}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
460 \end{frame}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
461 }
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
462
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
463 \defineUnit{modelluebersetzungen}{%
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
464 \begin{frame}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
465 \frametitle{Übersetzungen}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
466 \setbeamercovered{dynamic}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
467
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
468 \begin{center}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
469 \begin{tikzpicture}[node distance=2.5cm]
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
470 \node (WH) {WHILE};
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
471 \node (GO) [above left of = WH] {GOTO};
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
472 \node (TM) [above right of = WH] {TM};
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
473 \node (LO) [below of = WH] {LOOP};
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
474 \node (PR) [left of = LO] {PR};
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
475 \node (MR) [left of = WH] {$\mu$R};
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
476
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
477 \draw [every edge, ->] (LO) -- (WH);
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
478 \draw [every edge, ->] (PR) -- (MR);
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
479 \draw [every edge, tumgreen, <->] (LO) -- (PR);
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
480 \draw [every edge, tumgreen, <->] (WH) -- (MR);
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
481 \draw [every edge, <->] (WH) -- (GO);
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
482 \draw [every edge, ->] (WH) -- (TM);
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
483 \draw [every edge, ->] (TM) -- (GO);
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
484 \end{tikzpicture}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
485 \end{center}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
486
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
487 \vfill
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
488
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
489 LOOP kann in WHILE \alert{übersetzt} werden, WHILE ist also \alert{mindestens so mächtig} wie LOOP (sogar mächtiger).
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
490 \end{frame}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
491 }
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
492
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
493 \defineUnit{entscheidbarkeit}{%
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
494 \begin{frame}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
495 \frametitle{Entscheidbarkeit}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
496 \setbeamercovered{dynamic}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
497
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
498 \begin{definition}[Entscheidbarkeit]
6
efd13093bd47 use structures instead of alerts
Markus Kaiser <markus.kaiser@in.tum.de>
parents: 3
diff changeset
499 Eine Menge $A$ heißt \structure{entscheidbar} gdw ihre \alert{charakteristische Funktion}
1
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
500 \[ \chi_A(x) := \begin{cases}1 & \text{falls } x \in A \\ 0 & \text{falls } x \not \in A \end{cases} \]
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
501 berechenbar ist.
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
502 \end{definition}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
503
6
efd13093bd47 use structures instead of alerts
Markus Kaiser <markus.kaiser@in.tum.de>
parents: 3
diff changeset
504 \vfill
efd13093bd47 use structures instead of alerts
Markus Kaiser <markus.kaiser@in.tum.de>
parents: 3
diff changeset
505
1
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
506 \begin{definition}[Semi-Entscheidbarkeit]
6
efd13093bd47 use structures instead of alerts
Markus Kaiser <markus.kaiser@in.tum.de>
parents: 3
diff changeset
507 Eine Menge $A$ heißt \structure{semi-entscheidbar} gdw
1
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
508 \[ \chi'_A(x) := \begin{cases}1 & \text{falls } x \in A \\ \perp & \text{falls } x \not \in A \end{cases} \]
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
509 berechenbar ist.
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
510 \end{definition}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
511 \end{frame}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
512 }
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
513
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
514 \defineUnit{breduktion}{%
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
515 \begin{frame}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
516 \frametitle{Reduzierbarkeit}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
517 \setbeamercovered{dynamic}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
518
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
519 \begin{definition}[Reduzierbarkeit]
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
520 Eine Menge $A \subseteq \Sigma^*$ ist \alert{reduzierbar} auf eine Menge $B \subseteq \Gamma^*$ gdw es eine totale und berechenbare Funktion $f:\Sigma^* \to \Gamma^*$ gibt mit
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
521 \[\forall w \in \Sigma^*. w \in A \Longleftrightarrow f(w) \in B\]
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
522 Wir schreiben dann \alert{$A \leq B$}.
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
523 \end{definition}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
524
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
525 \vfill
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
526
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
527 \structure{Intuition}:
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
528 \begin{itemize}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
529 \item $B$ ist \alert{mindestens so schwer} zu lösen wie $A$
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
530 \item Ist $A$ unlösbar, dann auch $B$.
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
531 \item Ist $B$ lösbar, dann erst recht $A$.
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
532 \end{itemize}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
533 \end{frame}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
534 }
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
535
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
536 \defineUnit{spezielleshalteproblem}{%
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
537 \begin{frame}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
538 \frametitle{Spezielles Halteproblem}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
539 \setbeamercovered{dynamic}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
540
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
541 \begin{definition}[Spezielles Halteproblem]
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
542 Gegeben ein \structure{Wort} $w \in \left\{ 0, 1 \right\}^*$.\\
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
543 Hält \alert{$M_w$} bei Eingabe \alert{$w$}?
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
544 \[\alert{K} := \left\{ w \mid M_w[w]\downarrow \right\}\]
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
545 \end{definition}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
546
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
547 \begin{theorem}[]
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
548 Das spezielle Halteproblem ist \alert{nicht entscheidbar}.
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
549 \end{theorem}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
550
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
551 \vfill
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
552
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
553 \begin{itemize}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
554 \item Hält eine Turingmaschine mit sich selbst als Eingabe?
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
555 \item $w$ ist die \structure{Gödelisierung} von $M_w$.
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
556 \item $K$ ist semi-entscheidbar, $\overline{K}$ \alert{nicht}.
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
557 \end{itemize}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
558 \end{frame}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
559 }
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
560
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
561 \defineUnit{halteproblem}{%
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
562 \begin{frame}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
563 \frametitle{Allgemeines Halteproblem}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
564 \setbeamercovered{dynamic}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
565
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
566 \begin{definition}[Allgemeines Halteproblem]
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
567 Gegeben \structure{Wörter} $w, x \in \left\{ 0, 1 \right\}^*$.\\
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
568 Hält \alert{$M_w$} bei Eingabe \alert{$x$}?
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
569 \[\alert{H} := \left\{ w\#x \mid M_w[x]\downarrow \right\}\]
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
570 \end{definition}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
571
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
572 \begin{theorem}[]
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
573 Das allgemeine Halteproblem ist \alert{nicht entscheidbar}.
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
574 \end{theorem}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
575
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
576 \vfill
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
577
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
578 \begin{itemize}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
579 \item Es ist $K \leq H$. Warum?
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
580 \end{itemize}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
581 \end{frame}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
582 }
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
583
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
584 \defineUnit{aufzaehlbarkeit}{%
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
585 \begin{frame}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
586 \frametitle{Rekursive Aufzählbarkeit}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
587 \setbeamercovered{dynamic}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
588
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
589 \begin{definition}[Rekursiv aufzählbar]
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
590 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
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
591 \[A = \left\{ f(0), f(1), \ldots \right\} = \bigcup_{n \in \N} \left\{ f(n) \right\}\]
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
592 \end{definition}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
593
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
594 \vfill
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
595
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
596 \structure{Äquivalent:}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
597 \begin{itemize}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
598 \item $A$ rekursiv aufzählbar
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
599 \item $A$ semi-entscheidbar, also $\chi'_A$ berechenbar
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
600 \item $A=L(M)$ für eine TM $M$
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
601 \item $A$ ist Bild oder Urbild einer berechenbaren Funktion
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
602 \end{itemize}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
603 \end{frame}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
604 }
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
605
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
606 \defineUnit{rice}{%
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
607 \begin{frame}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
608 \frametitle{Satz von Rice}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
609 \setbeamercovered{dynamic}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
610
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
611 \begin{theorem}[Rice]
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
612 Sei $F$ eine Menge berechenbarer Funktionen.\\
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
613 Sei weder $F = \emptyset$ noch $F = \text{alle ber. Funktionen}$ (\alert{$F$ nicht trivial}).\\
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
614 Dann ist \alert{unentscheidbar}, ob die von einer gegebenen TM $M_w$ berechnete Funktion in $F$ ist, also ob \alert{$\varphi_w \in F$}.
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
615 \end{theorem}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
616
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
617 \begin{itemize}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
618 \item Nicht-triviale \alert{semantische} Eigenschaften von Programmen sind unentscheidbar.
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
619 \item \alert{Termination} ist unentscheidbar.
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
620 \end{itemize}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
621
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
622 \vfill
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
623
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
624 \structure{Rice-Shapiro:}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
625 \begin{itemize}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
626 \item Termination ist nicht semi-entscheidbar.
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
627 \item Nicht-Termination ist nicht semi-entscheidbar.
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
628 \end{itemize}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
629 \end{frame}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
630 }
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
631
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
632 \defineUnit{pcp}{%
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
633 \begin{frame}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
634 \frametitle{PCP}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
635 \setbeamercovered{dynamic}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
636
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
637 \begin{definition}[Postsches Korrespondenzproblem]
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
638 Gegeben \structure{endliche Folge} $(x_1, y_1), \ldots, (x_k, y_k)$ mit $x_i, y_i \in \Sigma^+$.\\
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
639 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}\]}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
640 \end{definition}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
641
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
642 \vfill
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
643
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
644 \begin{center}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
645 \begin{tikzpicture}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
646 \begin{scope}[start chain, node distance=2em]
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
647 \node[tape, active] {\pcp{$x_i$}{$y_i$}};
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
648 \node[tape] (a) {\pcp{$001$}{$00$}};
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
649 \node[tape] (b) {\pcp{$10$}{$11$}};
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
650 \node[tape] (c) {\pcp{$1$}{$01$}};
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
651 \end{scope}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
652 \node[below of=a] {$1$};
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
653 \node[below of=b] {$2$};
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
654 \node[below of=c] {$3$};
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
655 \end{tikzpicture}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
656 \end{center}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
657
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
658 \vfill
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
659
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
660 \begin{theorem}[]
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
661 Das PCP ist \alert{unentscheidbar}, aber semi-entscheidbar.
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
662 \end{theorem}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
663 \end{frame}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
664 }
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
665
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
666 \defineUnit{pcpbeispiel}{%
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
667 \begin{frame}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
668 \frametitle{PCP lösen}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
669 \setbeamercovered{dynamic}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
670
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
671 \begin{block}{Idee}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
672 \alert{Mögliche Lösungen} aufzählen, richtige Lösungen identifizieren
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
673 \end{block}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
674
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
675 \begin{center}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
676 \begin{tikzpicture}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
677 \begin{scope}[start chain, node distance=2em]
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
678 \node[tape, active] {\pcp{$x_i$}{$y_i$}};
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
679 \node[tape] (a) {\pcp{$001$}{$00$}};
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
680 \node[tape] (b) {\pcp{$01$}{$10$}};
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
681 \node[tape] (c) {\pcp{$1$}{$11$}};
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
682 \end{scope}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
683 \node[below of=a] {$1$};
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
684 \node[below of=b] {$2$};
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
685 \node[below of=c] {$3$};
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
686 \end{tikzpicture}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
687
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
688 \vspace{2em}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
689
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
690 \begin{tikzpicture}[grow=right, level distance = 2cm]
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
691 \tikzstyle{every node} = []
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
692 \tikzstyle{residual} = [rectangular, thin, fill=tumgreen!10, font=\scriptsize]
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
693 \tikzstyle{edge from parent} = [every edge]
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
694
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
695 \tikzstyle{level 1} = [sibling distance = 1.7cm]
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
696 \tikzstyle{level 2} = [sibling distance = 1.1cm]
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
697
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
698 \node[residual] {}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
699 child {
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
700 node[residual] {\pcp{$1$}{}}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
701 child {
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
702 node[residual] {\pcp{$1$}{}}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
703 child {
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
704 node[residual] {\pcp{$1$}{}}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
705 child {
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
706 node[residual]{$\ldots$}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
707 edge from parent
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
708 }
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
709 edge from parent
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
710 node[below] {$2$}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
711 }
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
712 child {
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
713 node[residual, active] {\pcp{}{}}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
714 edge from parent
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
715 node[above] {$3$}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
716 }
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
717 edge from parent
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
718 node[below] {$2$}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
719 }
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
720 child {
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
721 node[residual, active] {\pcp{}{}}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
722 edge from parent
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
723 node[above] {$3$}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
724 }
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
725 edge from parent
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
726 node[below] {$1$}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
727 }
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
728 child {
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
729 node[residual]{\pcp{}{$1$}}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
730 child {
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
731 node[residual]{\pcp{}{$11$}}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
732 child {
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
733 node[residual]{$\ldots$}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
734 edge from parent
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
735 node[above] {$3$}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
736 }
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
737 edge from parent
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
738 node[above] {$3$}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
739 }
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
740 edge from parent
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
741 node[above] {$3$}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
742 };
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
743
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
744 \uncover<2>{\node at (10cm, 0) {$L = \left\{ (12^*3)^+ \right\}$};}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
745 \end{tikzpicture}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
746 \end{center}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
747 \end{frame}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
748 }
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
749
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
750 \defineUnit{time}{%
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
751 \begin{frame}[t]
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
752 \frametitle{$TIME$}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
753 \setbeamercovered{dynamic}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
754
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
755 \begin{definition}[$TIME$]
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
756 Wir bezeichnen die minimale Anzahl der Schritte, bis eine \structure{DTM} $M$ mit Eingabe $w$ hält als $\alert{time_M(w)} \in \N \cup \left\{ \infty \right\}$.\\
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
757 \vspace{1em}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
758 Sei $f : \N \to \N$ total. Dann ist
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
759 \begin{align*}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
760 \alert{TIME(f(n))} := \{ A \subseteq \Sigma^* \mid \exists &\structure{DTM}\ M. A = L(M) \wedge \\
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
761 &\forall w \in \Sigma^*. \structure{time_M(w) \leq f(|w|)} \}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
762 \end{align*}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
763 die Klasse der \structure{in Zeit $f(n)$} von einer \structure{DTM} entscheidbaren Sprachen.
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
764 \end{definition}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
765
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
766 \vfill
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
767
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
768 \begin{itemize}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
769 \item $TIME(\Oh(n))$ enthält alle "\structure{linearen Probleme}".
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
770 \item Also alle Probleme, für die ein Linearzeitalgorithmus existiert.
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
771 \end{itemize}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
772 \end{frame}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
773 }
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
774
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
775 \defineUnit{ntime}{%
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
776 \begin{frame}[t]
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
777 \frametitle{$NTIME$}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
778 \setbeamercovered{dynamic}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
779
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
780 \begin{definition}[$NTIME$]
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
781 Wir bezeichnen die minimale Anzahl der Schritte, bis eine \structure{NTM} $M$ mit Eingabe $w$ hält als $\alert{ntime_M(w)} \in \N$.
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
782 \[ \alert{ntime_M(w)} := \begin{cases} \text{minimale Schrittanzahl} & \text{falls } w \in L(M) \\ 0 & \text{falls } w \not \in L(M)\end{cases} \]
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
783 Dann ist
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
784 \begin{align*}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
785 \alert{NTIME(f(n))} := \{ A \subseteq \Sigma^* \mid \exists &\structure{NTM}\ M. A = L(M) \wedge \\
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
786 &\forall w \in \Sigma^*. \structure{ntime_M(w) \leq f(|w|)} \}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
787 \end{align*}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
788 die Klasse der \structure{in Zeit $f(n)$} von einer \structure{NTM} entscheidbaren Sprachen.
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
789 \end{definition}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
790 \end{frame}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
791 }
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
792
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
793 \defineUnit{pundnp}{%
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
794 \begin{frame}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
795 \frametitle{P und NP}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
796 \setbeamercovered{dynamic}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
797
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
798 \begin{definition}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
799 \alert{P} ist die Menge aller von einer \structure{DTM} in polynomieller Zeit entscheidbaren Sprachen.
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
800 \[\alert{P}:= \bigcup_{p\text{ Polynom}} TIME(p(n)) = \bigcup_{k \in \N} TIME(\alert{\Oh(n^k)}) \]
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
801 \end{definition}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
802
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
803 \begin{definition}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
804 \alert{NP} ist die Menge aller von einer \structure{NTM} in polynomieller Zeit entscheidbaren Sprachen.
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
805 \[\alert{NP}:= \bigcup_{p\text{ Polynom}} NTIME(p(n)) = \bigcup_{k \in \N} NTIME(\alert{\Oh(n^k)}) \]
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
806 \end{definition}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
807 \end{frame}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
808 }
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
809
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
810 \defineUnit{verifikator}{%
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
811 \begin{frame}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
812 \frametitle{Verifikator}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
813 \setbeamercovered{dynamic}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
814
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
815 \begin{definition}[Verifikator]
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
816 Sei $M$ eine \structure{DTM} mit $L(M) \subseteq \left\{ w\# c \mid w \in \Sigma^*, c \in \Delta^* \right\}$.
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
817 \begin{itemize}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
818 \item Falls $w\#c \in L(M)$, dann heißt $c$ \alert{Zertifikat} für $w$.
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
819 \item $M$ ist ein \alert{polynomiell beschränkter Verifikator} für
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
820 \[\left\{ \structure{w \in \Sigma^*} \mid \exists c \in \Delta^* . w\#c \in L(M) \right\}\]
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
821 falls $time_M(w\#c) \leq p(|w|)$ für ein Polynom $p$.
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
822 \end{itemize}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
823 \end{definition}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
824
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
825 \begin{itemize}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
826 \item \structure{NTM} rät Lösung (Zertifikat), \structure{DTM} probiert sie aus.
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
827 \item Verifizieren (wahrscheinlich) einfacher als Lösung finden.
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
828 \end{itemize}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
829
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
830 \vfill
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
831
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
832 \begin{theorem}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
833 \alert{$A \in NP$} gdw es einen pol. beschränkten Verifikator für A gibt.
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
834 \end{theorem}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
835 \end{frame}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
836 }
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
837
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
838 \defineUnit{preduktion}{%
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
839 \begin{frame}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
840 \frametitle{Polynomielle Reduzierbarkeit}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
841 \setbeamercovered{dynamic}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
842
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
843 \begin{definition}[Polynomielle Reduzierbarkeit]
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
844 Eine Menge $A \subseteq \Sigma^*$ ist \alert{polynomiell reduzierbar} auf eine Menge $B \subseteq \Gamma^*$ gdw es eine totale und \structure{von einer DTM in polynomieller Zeit} berechenbare Funktion $f:\Sigma^* \to \Gamma^*$ gibt mit
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
845 \[\forall w \in \Sigma^*. w \in A \Longleftrightarrow f(w) \in B\]
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
846 Wir schreiben dann \alert{$A \leq_P B$}.
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
847 \end{definition}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
848
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
849 \vfill
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
850
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
851 \begin{itemize}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
852 \item Die Relation $\leq_P$ ist \structure{transitiv}.
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
853 \item P und NP sind \structure{nach unten abgeschlossen}:
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
854 \[A \leq_P B \in P/NP \Longrightarrow A \in P/NP\]
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
855 \end{itemize}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
856 \end{frame}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
857 }
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
858
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
859 \defineUnit{npvollstaendigkeit}{%
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
860 \begin{frame}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
861 \frametitle{NP-Vollständigkeit}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
862 \setbeamercovered{dynamic}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
863
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
864 \begin{definition}[NP-Schwere]
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
865 Eine Sprache $L$ heißt \alert{NP-schwer} (NP-hart) wenn sich \structure{alle Sprachen} in NP auf $L$ reduzieren lassen.
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
866 \[\forall A \in NP. A \leq_P L\]
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
867 \end{definition}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
868
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
869 \begin{definition}[NP-Vollständigkeit]
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
870 Eine Sprache $L$ heißt \alert{NP-vollständig} wenn $L$ \structure{NP-schwer} ist und \structure{$L \in NP$}.
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
871 \end{definition}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
872
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
873 \vfill
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
874
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
875 \structure{Fragen}:
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
876 \begin{itemize}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
877 \item Gibt es überhaupt NP-vollständige Sprachen?
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
878 \item Gibt es eine NP-vollständige Sprache in $P$?
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
879 \end{itemize}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
880 \end{frame}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
881 }
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
882
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
883 \defineUnit{sat}{%
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
884 \begin{frame}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
885 \frametitle{SAT}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
886 \setbeamercovered{dynamic}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
887
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
888 \begin{definition}[Aussagenlogik]
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
889 Syntax der \alert{Aussagenlogik}.\\
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
890 \begin{description}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
891 \item[Formeln] $F \rightarrow \neg F \mid (F \wedge F) \mid (F \vee F) \mid X$
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
892 \item[Variablen] $X \rightarrow x \mid y \mid z \mid \ldots$
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
893 \end{description}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
894 \end{definition}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
895
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
896 \vfill
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
897
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
898 \begin{definition}[SAT]
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
899 Gegeben eine \structure{aussagenlogische Formel} $F$.\\
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
900 Ist $F$ \alert{erfüllbar}, also gibt es eine Belegung der Variablen in $F$, sodass $F$ gilt?
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
901 \end{definition}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
902
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
903 \begin{theorem}[Cook 1971]
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
904 $\mathbf{SAT}$ ist \alert{NP-vollständig}.
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
905 \end{theorem}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
906 \end{frame}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
907 }
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
908
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
909 \defineUnit{3col}{%
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
910 \begin{frame}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
911 \frametitle{3COL}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
912 \setbeamercovered{dynamic}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
913
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
914 \begin{definition}[3COL]
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
915 Gegeben ein \structure{Graph} $G = (V, E)$.\\
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
916 Gibt es eine \alert{Färbung der Knoten} $V$ mit $3$ Farben, so dass keine zwei benachbarten Knoten die gleiche Farbe haben?
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
917 \end{definition}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
918
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
919 \vfill
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
920
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
921 \begin{center}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
922 \begin{tikzpicture}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
923 \tikzstyle{red} = [fill=tumred!50]
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
924 \tikzstyle{green} = [fill=tumgreen!50]
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
925 \tikzstyle{blue} = [fill=tumblue!50]
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
926 \tikzstyle{vertex} = [draw, circle, thin, blue]
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
927 \tikzstyle{edge} = [draw, thick]
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
928
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
929 \foreach \name/\angle/\dist/\col in {
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
930 ia/18/0.8cm/blue, ib/90/0.8cm/red, ic/162/0.8cm/red, id/234/0.8cm/green, ie/306/0.8cm/green,
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
931 oa/18/1.6cm/red, ob/90/1.6cm/blue, oc/162/1.6cm/green, od/234/1.6cm/red, oe/306/1.6cm/blue} {
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
932 \node<1>[vertex] (\name) at (\angle:\dist) {};
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
933 \node<2>[vertex, \col] (\name) at (\angle:\dist) {};
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
934 }
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
935
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
936 \foreach \a/\b in {
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
937 ia/oa, ib/ob, ic/oc, id/od, ie/oe,
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
938 oa/ob, ob/oc, oc/od, od/oe, oe/oa,
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
939 ia/ic, ic/ie, ie/ib, ib/id, id/ia} {
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
940 \draw[edge] (\a) -- (\b);
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
941 }
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
942 \end{tikzpicture}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
943 \end{center}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
944
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
945 \begin{theorem}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
946 Es ist \alert{$\mathbf{3COL} \leq_P \mathbf{SAT}$} und $\alert{\mathbf{SAT}} \leq_P \mathbf{3SAT} \alert{\leq_P \mathbf{3COL}}$.
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
947 \end{theorem}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
948 \end{frame}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
949 }
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
950
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
951 \defineUnit{typ0sprachen}{%
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
952 \begin{frame}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
953 \frametitle{Typ 0 Sprachen}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
954 \setbeamercovered{dynamic}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
955
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
956 \begin{center}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
957 \begin{tikzpicture}[node distance=2.5cm]
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
958 \node (WH) {WHILE};
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
959 \node (GO) [above left of = WH] {GOTO};
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
960 \node (TM) [above right of = WH] {TM};
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
961 \node (MR) [left of = WH] {$\mu$R};
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
962
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
963 \draw [every edge, tumgreen, <->] (WH) -- (MR);
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
964 \draw [every edge, <->] (WH) -- (GO);
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
965 \draw [every edge, ->] (WH) -- (TM);
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
966 \draw [every edge, ->] (TM) -- (GO);
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
967 \end{tikzpicture}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
968 \end{center}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
969
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
970 \vfill
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
971
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
972 \begin{theorem}[]
27
f7bcd68a0c12 eigth sheet and notes; add hierarchy slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents: 6
diff changeset
973 Sei $A$ formale Sprache, dann ist äquivalent:
1
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
974 \vspace{1em}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
975 \begin{itemize}
27
f7bcd68a0c12 eigth sheet and notes; add hierarchy slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents: 6
diff changeset
976 \item $A$ ist \structure{Typ 0 Sprache}
f7bcd68a0c12 eigth sheet and notes; add hierarchy slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents: 6
diff changeset
977 \item $A$ \structure{rekursiv aufzählbar}
f7bcd68a0c12 eigth sheet and notes; add hierarchy slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents: 6
diff changeset
978 \item $A$ \structure{semi-entscheidbar}, also $\chi'_A$ berechenbar
f7bcd68a0c12 eigth sheet and notes; add hierarchy slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents: 6
diff changeset
979 \item $A=L(M)$ für eine \structure{TM $M$}
f7bcd68a0c12 eigth sheet and notes; add hierarchy slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents: 6
diff changeset
980 \item $A$ ist \structure{Bild oder Urbild} einer berechenbaren Funktion
1
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
981 \end{itemize}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
982 \end{theorem}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
983 \end{frame}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
984 }
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
985
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
986 \defineUnit{spracheigenschaften}{%
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
987 \begin{frame}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
988 \frametitle{Spracheigenschaften}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
989 \setbeamercovered{dynamic}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
990
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
991 \begin{itemize}
27
f7bcd68a0c12 eigth sheet and notes; add hierarchy slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents: 6
diff changeset
992 \item Abschlusseigenschaften
1
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
993 \end{itemize}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
994 \begin{table}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
995 \begin{tabu}to \textwidth{X[c]|ccccc}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
996 & Schnitt & Vereinigung & Komplement & Produkt & Stern \\ \tabucline{}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
997 REG & ja & ja & ja & ja & ja\\
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
998 CFL & nein & ja & nein & ja & ja\\
27
f7bcd68a0c12 eigth sheet and notes; add hierarchy slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents: 6
diff changeset
999 CSL & ja & ja & ja & ja & ja\\
1
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
1000 TM & \structure{ja} & \structure{ja} & \structure{nein} & \structure{ja} & \structure{ja}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
1001 \end{tabu}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
1002 \end{table}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
1003
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
1004 \vfill
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
1005
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
1006 \begin{itemize}
27
f7bcd68a0c12 eigth sheet and notes; add hierarchy slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents: 6
diff changeset
1007 \item Entscheidbarkeit
1
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
1008 \end{itemize}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
1009 \begin{table}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
1010 \begin{tabu}to \textwidth{X[c]|cccc}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
1011 & Wortproblem & Leerheit & Äquivalenz & Schnittproblem\\ \tabucline{}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
1012 DFA & $\Oh(n)$ & ja & ja & ja\\
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
1013 CFG & $\Oh(n^3)$ & ja & nein & nein\\
27
f7bcd68a0c12 eigth sheet and notes; add hierarchy slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents: 6
diff changeset
1014 CSL & $\Oh(2^n)$ & nein & nein & nein\\
1
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
1015 TM & \structure{nein} & \structure{nein} & \structure{nein} & \structure{nein}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
1016 \end{tabu}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
1017 \end{table}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
1018 \end{frame}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
1019 }
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
1020
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
1021 \defineUnit{formalesprachen}{%
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
1022 \begin{frame}[c]
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
1023 \frametitle{Formale Sprachen}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
1024 \setbeamercovered{dynamic}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
1025
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
1026 \begin{center}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
1027 \begin{tikzpicture}[auto]
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
1028 \tikzstyle{rect} = [thick];
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
1029 \tikzstyle{caption} = [align=left, anchor=north west];
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
1030
27
f7bcd68a0c12 eigth sheet and notes; add hierarchy slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents: 6
diff changeset
1031 \definecolor{hannahyellow}{HTML}{FFB81C}
f7bcd68a0c12 eigth sheet and notes; add hierarchy slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents: 6
diff changeset
1032 \langclass{brown}{}{0}{Formale Sprache $\subseteq \Sigma^*$};
1
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
1033 \langclass{tumblue}{}{1}{Typ 0 - Semi-Entscheidbar};
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
1034 \langclass{tumgreen}{}{2}{Entscheidbar};
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
1035 \langclass{violet}{}{3}{LOOP, PR};
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
1036 \langclass{tumred}{}{4}{NP};
27
f7bcd68a0c12 eigth sheet and notes; add hierarchy slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents: 6
diff changeset
1037 \langclass{hannahyellow}{dashed}{5}{P};
1
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
1038 \langclass{tumgreen!40!black}{}{6}{Typ 2 - Kontextfrei};
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
1039 \langclass{tumlightblue!80!black}{}{7}{Typ 3 - Regulär};
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
1040 \langclass{tumblue!20!black}{}{8}{Endlich};
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
1041 \end{tikzpicture}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
1042 \end{center}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
1043 \end{frame}
a9275b863a0d add old slides
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
1044 }