annotate notes/tex/computation.tex @ 41:5d10471f5585

move frame-definitions out of presentations
author Markus Kaiser <markus.kaiser@in.tum.de>
date Thu, 11 Jul 2013 20:42:36 +0200
parents
children c14b92bfa07f
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
41
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
1 \defineUnit{tmdefinition}{%
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
2 \begin{frame}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
3 \frametitle{Turingmaschinen}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
4 \setbeamercovered{dynamic}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
5
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
6 \begin{definition}[Turingmaschine]
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
7 Eine deterministische \alert{Turingmaschine (TM)} ist ein Tupel $M = (Q, \Sigma, \Gamma, \delta, q_0, \square, F)$ aus einer/einem
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
8 \begin{itemize}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
9 \item endlichen Menge von \alert{Zuständen} $Q$
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
10 \item endlichen \alert{Eingabealphabet} $\Sigma$
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
11 \item endlichen \alert{Bandalphabet} $\Gamma$ mit $\Sigma \subset \Gamma$
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
12 \item \alert{Übergangsfunktion} $\delta : Q \times \Gamma \to Q \times \Gamma \times \left\{ L, R, N \right\}$
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
13 \item \alert{Startzustand} $q_0 \in Q$
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
14 \item \alert{Leerzeichen} $\square \in \Gamma \setminus \Sigma$
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
15 \item Menge von \alert{Endzuständen} $F \subseteq Q$
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
16 \end{itemize}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
17 \end{definition}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
18 \end{frame}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
19 }
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
20
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
21 \defineUnit{tmvisualisierung}{%
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
22 \begin{frame}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
23 \frametitle{Turingmaschinen}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
24 \setbeamercovered{dynamic}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
25
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
26 \begin{definition}[Turingmaschine]
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
27 Eine deterministische \alert{Turingmaschine (TM)} ist ein Tupel $M = (Q, \Sigma, \Gamma, \delta, q_0, \square, F)$ aus einer/einem
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
28 \begin{itemize}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
29 \item \alert{Übergangsfunktion} $\delta : Q \times \Gamma \to Q \times \Gamma \times \left\{ L, R, N \right\}$
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
30 \end{itemize}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
31 \end{definition}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
32
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
33 \vfill
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
34
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
35 \begin{center}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
36 \begin{tikzpicture}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
37 % Tape
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
38 \begin{scope}[start chain, node distance=0]
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
39 \node[on chain] {\ldots};
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
40 \node[tape] {$\square$};
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
41 \node[tape] (l) {$\square$};
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
42 \node[tape] {$0$};
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
43 \node[tape] {$1$};
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
44 \node<1>[tape, active] (a){$0$};
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
45 \node<2>[tape] (a){$1$};
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
46 \node<1>[tape] (b){$0$};
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
47 \node<2>[tape, active] (b){$0$};
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
48 \node[tape] {$\square$};
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
49 \node[on chain] {\ldots};
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
50 \end{scope}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
51
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
52 % Head
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
53 \node<1> [head,yshift=-4mm] at (a.south) (head) {$q_0$};
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
54 \node<2> [head,yshift=-4mm] at (b.south) (head) {$q_1$};
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
55
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
56 % Machine
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
57 \node[machine, below=1.5cm of l] (machine) {Programm};
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
58 \draw[every edge] (machine) .. controls (3.5, -2) .. (head.south);
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
59
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
60 % Example-Transition
5d10471f5585 move frame-definitions out of presentations
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)$};
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
62 \end{tikzpicture}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
63 \end{center}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
64 \end{frame}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
65 }
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
66
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
67 \defineUnit{tmkonfiguration}{%
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
68 \begin{frame}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
69 \frametitle{Turingmaschinen}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
70 \setbeamercovered{dynamic}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
71
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
72 \begin{definition}[Konfiguration]
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
73 Eine \alert{Konfiguration} ist ein Tripel $(\alpha, q, \beta) \in \Gamma^* \times Q \times \Gamma^*$. \\
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
74 Dies modelliert eine TM mit:
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
75 \begin{itemize}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
76 \item \alert{Bandinhalt} $\ldots\square\alpha\beta\square\ldots$
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
77 \item \alert{Zustand} $q$
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
78 \item Kopf auf dem \alert{ersten Zeichen} von $\beta\square$
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
79 \end{itemize}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
80 Die \alert{Startkonfiguration} bei Eingabe $w \in \Sigma^*$ ist $(\epsilon, q_0, w)$.
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
81 \end{definition}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
82
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
83 \vfill
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
84
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
85 \only<1> {
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
86 \begin{center}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
87 \begin{tikzpicture}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
88 % Tape
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
89 \begin{scope}[start chain, node distance=0]
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
90 \node[on chain] {\ldots};
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
91 \node[tape] {$\square$};
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
92 \node[tape] (l) {$\square$};
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
93 \node[tape] {$0$};
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
94 \node[tape] {$1$};
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
95 \node[tape] (a){$1$};
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
96 \node[tape, active] (b){$0$};
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
97 \node[tape] {$\square$};
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
98 \node[on chain] {\ldots};
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
99 \end{scope}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
100
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
101 % Head
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
102 \node [head,yshift=-4mm] at (b.south) (head) {$q_1$};
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
103
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
104 % Machine
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
105 \node[below=1.5cm of l] (machine) {};
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
106 \draw[every edge, dashed] (machine) .. controls (3.5, -2) .. (head.south);
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
107
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
108 % Example-Transition
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
109 \node[yshift=5mm] at (current bounding box.north) {$(011,q_1,0)$};
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
110 \end{tikzpicture}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
111 \end{center}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
112 }
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
113
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
114 \only<2> {
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
115 \begin{definition}[Akzeptanz]
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
116 Eine TM $M$ \alert{akzeptiert} die Sprache
5d10471f5585 move frame-definitions out of presentations
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\} \]
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
118 \end{definition}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
119 }
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
120 \end{frame}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
121 }
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
122
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
123 \defineUnit{chomsky}{%
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
124 \begin{frame}[c]
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
125 \frametitle{Chomsky-Hierarchie}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
126 \setbeamercovered{dynamic}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
127
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
128 \begin{center}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
129 \begin{tikzpicture}[auto]
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
130 \tikzstyle{rect} = [thick];
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
131 \tikzstyle{caption} = [align=left, anchor=north west];
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
132
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
133 \draw[rect, tumblue, fill=tumblue!10] (5.5, 0) rectangle (-5.5, 7) node[caption] {Berechenbare Funktionen};
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
134 \draw[rect, dashed, tumred, fill=tumred!10] (4.5, 0.3) rectangle (-4.5, 6) node[caption] {Typ 0 - Rekursiv aufzählbar\\Turingmaschinen, $\lambda$-Kalkül};
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
135 \draw[rect, tumivory, fill=tumivory!10] (3.5, 0.6) rectangle (-3.5, 4.8) node[caption] {Typ 1 - Kontextsensitiv\\CSG};
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
136 \draw[rect, tumorange, fill=tumorange!10] (2.5, 0.9) rectangle (-2.5, 3.6) node[caption] {Typ 2 - Kontextfrei\\PDA, CFG};
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
137 \draw[rect, tumgreen, fill=tumgreen!10] (1.5, 1.2) rectangle (-1.5, 2.4) node[caption] {Typ 3 - Regulär\\DFA, RE};
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
138 \end{tikzpicture}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
139 \end{center}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
140 \end{frame}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
141 }
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
142
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
143 \defineUnit{berechenbarkeit}{%
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
144 \begin{frame}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
145 \frametitle{Berechenbarkeit}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
146 \setbeamercovered{dynamic}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
147
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
148 \begin{definition}[Intuitive Berechenbarkeit]
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
149 Eine Funktion $f : \N^k \to \N$ heißt \alert{intuitiv berechenbar}, wenn es einen Algorithmus gibt, der bei Eingabe $(n_1, \ldots, n_k) \in \N^k$
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
150 \begin{itemize}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
151 \item nach \alert{endlich vielen Schritten} mit Ergebnis $f(n_1, \ldots, n_k)$ hält, falls $f(\ldots)$ definiert ist,
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
152 \item und \alert{nicht terminiert}, falls $f(\ldots)$ nicht definiert ist.
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
153 \end{itemize}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
154 \end{definition}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
155
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
156 \vfill
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
157
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
158 \begin{block}{Churchsche These (nicht beweisbar)}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
159 Turing-Maschinen können genau \alert{alle} intuitiv berechenbaren Funktionen berechnen.
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
160 \end{block}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
161 \end{frame}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
162 }
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
163
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
164 \defineUnit{berechenbarkeitbeispiel}{%
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
165 \begin{frame}[c]
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
166 \frametitle{Berechenbarkeit}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
167 \setbeamercovered{dynamic}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
168
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
169 \begin{example}[Berechenbarkeit]
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
170 Sind die folgenden Funktionen intuitiv berechenbar?
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
171
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
172 \begin{align*}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
173 f_1(n) &= \begin{cases}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
174 1 & \text{falls $n$ prim}\\
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
175 0 & \text{sonst}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
176 \end{cases} \\
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
177 f_2(n) &= \begin{cases}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
178 1 & \text{falls $n$ die ersten $n$ Ziffern von $\pi$ darstellt}\\
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
179 0 & \text{sonst}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
180 \end{cases} \\
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
181 f_3(n) &= \begin{cases}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
182 1 & \text{falls in $\pi$ $n$ Nullen am Stück vorkommen}\\
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
183 0 & \text{sonst}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
184 \end{cases}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
185 \end{align*}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
186 \end{example}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
187 \end{frame}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
188 }
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
189
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
190 \defineUnit{pr}{%
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
191 \begin{frame}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
192 \frametitle{Primitive Rekursion}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
193 \setbeamercovered{dynamic}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
194
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
195 \begin{definition}[Basisfunktionen]
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
196 \alert{Primitiv Rekursiv} sind:
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
197 \begin{itemize}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
198 \item Die konstante Funktion \alert{0}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
199 \item Die \alert{Nachfolgerfunktion} $s(n) = n + 1$
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
200 \item Die \alert{Projektionsfunktion} $\pi_i^k : \N^k \to \N, i \in [k]$
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
201 \[ \pi_i^k(x_1, \ldots, x_k) = x_i \]
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
202 \end{itemize}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
203 \end{definition}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
204
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
205 \begin{definition}[Komposition]
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
206 Sind $g$ und $h_i$ PR und $\bar{x} = (x_1, \ldots, x_n)$, dann ist auch \alert{$f$} PR:
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
207 \[ f(\bar{x}) = \alert{g(h_1(\bar{x}), \ldots, h_k(\bar{x}))} \]
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
208 \end{definition}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
209 \end{frame}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
210 }
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
211
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
212 \defineUnit{prrekursion}{%
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
213 \begin{frame}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
214 \frametitle{Primitive Rekursion}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
215 \setbeamercovered{dynamic}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
216 \begin{block}{Basisfunktionen und Komposition}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
217 Schon \alert{PR} sind:
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
218 \begin{itemize}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
219 \item Konstante: $0$
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
220 \item Nachfolger: $s(n) = n + 1$
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
221 \item Projektion: $\pi_i^k : \N^k \to \N$
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
222 \item Komposition: $f(\bar{x}) = g(h_1(\bar{x}), \ldots, h_k(\bar{x}))$
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
223 \end{itemize}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
224 \end{block}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
225 \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}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
226 }
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
227
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
228 \defineUnit{prprogramme}{%
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
229 \begin{frame}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
230 \frametitle{PR-Programme}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
231 \setbeamercovered{dynamic}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
232
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
233 U.a. diese Programme sind laut Vorlesung oder Übung PR:
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
234 \begin{itemize}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
235 \item \alert{$add(x, y) = x + y$}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
236 \item \alert{$mult(x, y) = x \cdot y$}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
237 \item $pred(x) = \max \left\{ 0, x - 1 \right\}$
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
238 \item \alert{$x \dot{-} y = \max \left\{ 0, x - y \right\}$}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
239 \item $div(x, y) = x \div y$ (Ganzzahldivision)
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
240 \item $mod(x, y) = x \mod y$
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
241 \vspace{1.5em}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
242 \item $tower(n) = 2^{2^{2^{\iddots}}}$ mit $tower(4) = 2^{16}$
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
243 \item $sqr(x) = x^2$
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
244 \item $twopow(n) = 2^n$
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
245 \item $ifthen(n, a, b) = \begin{cases} a & n \neq 0 \\ b & n = 0 \end{cases}$
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
246 \end{itemize}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
247 \end{frame}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
248 }
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
249
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
250 \defineUnit{prerweitert}{%
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
251 \begin{frame}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
252 \frametitle{Erweitertes PR-Schema}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
253 \setbeamercovered{dynamic}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
254
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
255 \begin{definition}[Erweitertes PR-Schema]
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
256 Das \alert{erweiterte Schema der primitiven Rekursion} erlaubt
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
257 \begin{align*}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
258 f(0, \bar{x}) &= t_0 \\
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
259 f(m + 1, \bar{x}) &= t
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
260 \end{align*}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
261 wobei
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
262 \begin{itemize}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
263 \item $t_0$ enthält nur PR-Funktionen und die $x_i$
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
264 \item $t$ enthält nur \alert{$f(m, \bar{x})$}, PR Funktionen, \alert{$m$} und die $x_i$.
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
265 \end{itemize}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
266 \end{definition}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
267
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
268 \begin{theorem}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
269 Das erweiterte Schema der primitiven Rekursion führt nicht aus \alert{PR} heraus.
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
270 \end{theorem}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
271 \end{frame}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
272 }
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
273
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
274 \defineUnit{tmif}{%
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
275 \begin{frame}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
276 \frametitle{Programmieren mit TMs}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
277 \setbeamercovered{dynamic}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
278
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
279 Sind $f_1$ und $f_2$ Endzustände von $M$, so bezeichnet
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
280 \begin{center}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
281 \begin{tikzpicture}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
282 \node (M) at (0, 0) {$M$};
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
283 \node[above right=0.2cm and 1cm of M] (M1) {$M_1$};
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
284 \node[below right=0.2cm and 1cm of M] (M2) {$M_2$};
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
285 \coordinate[right of=M1] (M1s);
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
286 \coordinate[right of=M2] (M2s);
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
287
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
288 \draw[every edge] (-1, 0) -- (M);
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
289 \draw[every edge] (M) -- node[above left] {$f_1$} (M1);
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
290 \draw[every edge] (M) -- node[below left] {$f_2$} (M2);
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
291 \draw[every edge] (M1) -- (M1s);
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
292 \draw[every edge] (M2) -- (M2s);
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
293 \end{tikzpicture}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
294 \end{center}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
295 eine \alert{Fallunterscheidung}.\\
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
296 \begin{example}[Band=0?]
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
297 \begin{align*}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
298 \delta(q_0, 0) &= (q_0, 0, R) \\
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
299 \delta(q_0, \square) &= (ja, \square, L) \\
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
300 \delta(q_0, a) &= (nein, a, N) \qquad \text{für} a \neq 0, \square
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
301 \end{align*}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
302 \end{example}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
303 \end{frame}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
304 }
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
305
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
306 \defineUnit{while}{%
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
307 \begin{frame}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
308 \frametitle{WHILE-Programme}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
309 \setbeamercovered{dynamic}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
310
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
311 \begin{definition}[WHILE-Programm]
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
312 Syntax von \alert{WHILE-Programmen}.\\
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
313 Es ist $X \in \left\{ x_0, x_1, \ldots \right\}$ und $C \in \N$.
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
314 \begin{align*}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
315 P &\rightarrow X := X + C \\
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
316 &\mid X := X - C \\
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
317 &\mid P; P \\
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
318 &\mid \alert{\mathbf{WHILE}\ X \neq 0 \ \mathbf{DO}\ P \ \mathbf{END}} \\
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
319 &\mid \textcolor{gray}{\mathbf{LOOP}\ X \ \mathbf{DO}\ P \ \mathbf{END}} \\
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
320 &\mid \textcolor{gray}{\mathbf{IF}\ X = 0 \ \mathbf{DO}\ P \ \mathbf{ELSE}\ Q \ \mathbf{END}}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
321 \end{align*}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
322 \end{definition}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
323
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
324 \begin{itemize}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
325 \item Ausgabe steht in $x_0$, Eingaben in $x_1, \ldots, x_n$, Rest ist 0.
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
326 \item Semantik wie erwartet.
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
327 \end{itemize}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
328 \end{frame}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
329 }
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
330
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
331 \defineUnit{goto}{%
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
332 \begin{frame}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
333 \frametitle{GOTO-Programme}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
334 \setbeamercovered{dynamic}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
335
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
336 \begin{definition}[GOTO-Programm]
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
337 Syntax von \alert{GOTO-Programmen}.\\
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
338 Es ist $X \in \left\{ x_0, x_1, \ldots \right\}$ und $C \in \N$. \\
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
339 Alle Anweisungen haben eine Markierung \alert{$M_1 : A_1; M_2 : A_2$}.
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
340 \begin{align*}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
341 P &\rightarrow X := X + C \\
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
342 &\mid X := X - C \\
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
343 &\mid P; P \\
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
344 &\mid \mathbf{GOTO}\ M_i \\
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
345 &\mid \mathbf{IF}\ X = 0 \ \mathbf{GOTO}\ M_i \\
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
346 &\mid \mathbf{HALT}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
347 \end{align*}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
348 \end{definition}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
349
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
350 \begin{itemize}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
351 \item Ausgabe steht in $x_0$, Eingaben in $x_1, \ldots, x_n$, Rest ist 0.
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
352 \end{itemize}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
353 \end{frame}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
354 }
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
355
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
356 \defineUnit{loop}{%
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
357 \begin{frame}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
358 \frametitle{LOOP-Programme}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
359 \setbeamercovered{dynamic}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
360
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
361 \begin{definition}[LOOP-Programm]
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
362 Syntax von \alert{LOOP-Programmen}.\\
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
363 Es ist $X \in \left\{ x_0, x_1, \ldots \right\}$ und $C \in \N$.
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
364 \begin{align*}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
365 P &\rightarrow X := X + C \\
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
366 &\mid X := X - C \\
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
367 &\mid P; P \\
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
368 &\mid \mathbf{LOOP}\ X \ \mathbf{DO}\ P \ \mathbf{END} \\
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
369 &\mid \textcolor{gray}{\mathbf{IF}\ X = 0 \ \mathbf{DO}\ P \ \mathbf{ELSE}\ Q \ \mathbf{END}}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
370 \end{align*}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
371 \end{definition}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
372
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
373 \begin{itemize}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
374 \item Ausgabe steht in $x_0$, Eingaben in $x_1, \ldots, x_n$, Rest ist 0.
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
375 \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.}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
376 \end{itemize}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
377 \end{frame}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
378 }
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
379
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
380 \defineUnit{prmax}{%
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
381 \begin{frame}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
382 \frametitle{Beschränkte Operationen}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
383 \setbeamercovered{dynamic}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
384 \begin{definition}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
385 Ein Prädikat $P$ ist \alert{PR}, wenn es eine PR Funktion $\hat{P}$ gibt mit
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
386 \[\hat{P}(x) = 1 \Longleftrightarrow P(x)\]
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
387 \end{definition}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
388
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
389 \begin{definition}[Beschränkte Operationen]
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
390 Ist $P$ PR, dann auch
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
391 \begin{itemize}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
392 \item der \alert{beschränkte max-Operator}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
393 \[\max \left\{ x \alert{\leq n} \mid P(x) \right\}, \quad \max \left\{ \emptyset \right\} = 0\]
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
394 \item der \alert{beschränkte Existenzquantor}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
395 \[\exists x \alert{\leq n}. P(x)\]
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
396 \end{itemize}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
397 \end{definition}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
398 \end{frame}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
399 }
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
400
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
401 \defineUnit{murekursion}{%
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
402 \begin{frame}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
403 \frametitle{$\mu$-Rekursion}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
404 \setbeamercovered{dynamic}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
405
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
406 \begin{definition}[$\mu$-Operator]
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
407 Sei $f: \N^{k+1} \to \N$ eine Funktion.\\Der \alert{$\mu$-Operator} definiert eine neue Funktion $\mu f : \N^k \to \N$:
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
408 \[(\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}\]
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
409 \end{definition}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
410
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
411 \vfill
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
412
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
413 \begin{itemize}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
414 \item \alert{$^*$}Für alle \alert{$m \leq n$} muss $f$ definiert sein: $f(m, \bar{x}) \neq \perp$
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
415 \item PR + $\mu$ = $\mu$-Rekursion
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
416 \item In Pseudocode:
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
417 \begin{align*}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
418 \mu f(\bar{x}) &= find(0, \bar{x}) \\
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
419 find(n, \bar{x}) &= \mathbf{if}\ f(n, \bar{x}) = 0 \ \mathbf{then}\ n \ \mathbf{else}\ find(n+1, \bar{x})
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
420 \end{align*}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
421 \end{itemize}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
422 \end{frame}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
423 }
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
424
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
425 \defineUnit{modelluebersetzungen}{%
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
426 \begin{frame}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
427 \frametitle{Übersetzungen}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
428 \setbeamercovered{dynamic}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
429
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
430 \begin{center}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
431 \begin{tikzpicture}[node distance=2.5cm]
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
432 \node (WH) {WHILE};
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
433 \node (GO) [above left of = WH] {GOTO};
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
434 \node (TM) [above right of = WH] {TM};
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
435 \node (LO) [below of = WH] {LOOP};
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
436 \node (PR) [left of = LO] {PR};
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
437 \node (MR) [left of = WH] {$\mu$R};
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
438
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
439 \draw [every edge, ->] (LO) -- (WH);
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
440 \draw [every edge, ->] (PR) -- (MR);
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
441 \draw [every edge, tumgreen, <->] (LO) -- (PR);
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
442 \draw [every edge, tumgreen, <->] (WH) -- (MR);
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
443 \draw [every edge, <->] (WH) -- (GO);
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
444 \draw [every edge, ->] (WH) -- (TM);
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
445 \draw [every edge, ->] (TM) -- (GO);
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
446 \end{tikzpicture}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
447 \end{center}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
448
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
449 \vfill
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
450
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
451 LOOP kann in WHILE \alert{übersetzt} werden, WHILE ist also \alert{mindestens so mächtig} wie LOOP (sogar mächtiger).
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
452 \end{frame}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
453 }
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
454
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
455 \defineUnit{entscheidbarkeit}{%
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
456 \begin{frame}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
457 \frametitle{Entscheidbarkeit}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
458 \setbeamercovered{dynamic}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
459
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
460 \begin{definition}[Entscheidbarkeit]
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
461 Eine Menge $A$ heißt \alert{entscheidbar} gdw ihre \alert{charakteristische Funktion}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
462 \[ \chi_A(x) := \begin{cases}1 & \text{falls } x \in A \\ 0 & \text{falls } x \not \in A \end{cases} \]
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
463 berechenbar ist.
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
464 \end{definition}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
465
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
466 \begin{definition}[Semi-Entscheidbarkeit]
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
467 Eine Menge $A$ heißt \alert{semi-entscheidbar} gdw
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
468 \[ \chi'_A(x) := \begin{cases}1 & \text{falls } x \in A \\ \perp & \text{falls } x \not \in A \end{cases} \]
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
469 berechenbar ist.
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
470 \end{definition}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
471 \end{frame}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
472 }
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
473
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
474 \defineUnit{spezielleshalteproblem}{%
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
475 \begin{frame}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
476 \frametitle{Spezielles Halteproblem}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
477 \setbeamercovered{dynamic}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
478
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
479 \begin{definition}[Spezielles Halteproblem]
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
480 Gegeben ein \structure{Wort} $w \in \left\{ 0, 1 \right\}^*$.\\
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
481 Hält \alert{$M_w$} bei Eingabe \alert{$w$}?
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
482 \[\alert{K} := \left\{ w \mid M_w[w]\downarrow \right\}\]
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
483 \end{definition}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
484
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
485 \begin{theorem}[]
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
486 Das spezielle Halteproblem ist \alert{nicht entscheidbar}.
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
487 \end{theorem}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
488
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
489 \vfill
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
490
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
491 \begin{itemize}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
492 \item Hält eine Turingmaschine mit sich selbst als Eingabe?
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
493 \item $w$ ist die \structure{Gödelisierung} von $M_w$.
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
494 \item $K$ ist semi-entscheidbar, $\overline{K}$ \alert{nicht}.
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
495 \end{itemize}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
496 \end{frame}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
497 }
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
498
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
499 \defineUnit{halteproblem}{%
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
500 \begin{frame}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
501 \frametitle{Allgemeines Halteproblem}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
502 \setbeamercovered{dynamic}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
503
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
504 \begin{definition}[Allgemeines Halteproblem]
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
505 Gegeben \structure{Wörter} $w, x \in \left\{ 0, 1 \right\}^*$.\\
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
506 Hält \alert{$M_w$} bei Eingabe \alert{$x$}?
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
507 \[\alert{H} := \left\{ w\#x \mid M_w[x]\downarrow \right\}\]
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
508 \end{definition}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
509
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
510 \begin{theorem}[]
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
511 Das allgemeine Halteproblem ist \alert{nicht entscheidbar}.
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
512 \end{theorem}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
513
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
514 \vfill
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
515
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
516 \begin{itemize}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
517 \item Es ist $K \leq H$. Warum?
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
518 \end{itemize}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
519 \end{frame}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
520 }
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
521
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
522 \defineUnit{aufzaehlbarkeit}{%
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
523 \begin{frame}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
524 \frametitle{Rekursive Aufzählbarkeit}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
525 \setbeamercovered{dynamic}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
526
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
527 \begin{definition}[Rekursiv aufzählbar]
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
528 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
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
529 \[A = \left\{ f(0), f(1), \ldots \right\} = \bigcup_{n \in \N} \left\{ f(n) \right\}\]
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
530 \end{definition}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
531
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
532 \vfill
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
533
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
534 \structure{Äquivalent:}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
535 \begin{itemize}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
536 \item $A$ rekursiv aufzählbar
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
537 \item $A$ semi-entscheidbar, also $\chi'_A$ berechenbar
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
538 \item $A=L(M)$ für eine TM $M$
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
539 \item $A$ ist Bild oder Urbild einer berechenbaren Funktion
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
540 \end{itemize}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
541 \end{frame}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
542 }
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
543
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
544 \defineUnit{rice}{%
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
545 \begin{frame}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
546 \frametitle{Satz von Rice}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
547 \setbeamercovered{dynamic}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
548
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
549 \begin{theorem}[Rice]
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
550 Sei $F$ eine Menge berechenbarer Funktionen.\\
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
551 Sei weder $F = \emptyset$ noch $F = \text{alle ber. Funktionen}$ (\alert{$F$ nicht trivial}).\\
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
552 Dann ist \alert{unentscheidbar}, ob die von einer gegebenen TM $M_w$ berechnete Funktion in $F$ ist, also ob \alert{$\varphi_w \in F$}.
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
553 \end{theorem}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
554
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
555 \begin{itemize}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
556 \item Nicht-triviale \alert{semantische} Eigenschaften von Programmen sind unentscheidbar.
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
557 \item \alert{Termination} ist unentscheidbar.
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
558 \end{itemize}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
559
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
560 \vfill
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
561
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
562 \structure{Rice-Shapiro:}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
563 \begin{itemize}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
564 \item Termination ist nicht semi-entscheidbar.
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
565 \item Nicht-Termination ist nicht semi-entscheidbar.
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
566 \end{itemize}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
567 \end{frame}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
568 }
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
569
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
570 \defineUnit{pcp}{%
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
571 \begin{frame}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
572 \frametitle{PCP}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
573 \setbeamercovered{dynamic}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
574
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
575 \begin{definition}[Postsches Korrespondenzproblem]
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
576 Gegeben \structure{endliche Folge} $(x_1, y_1), \ldots, (x_k, y_k)$ mit $x_i, y_i \in \Sigma^+$.\\
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
577 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}\]}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
578 \end{definition}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
579
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
580 \vfill
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
581
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
582 \begin{center}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
583 \begin{tikzpicture}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
584 \begin{scope}[start chain, node distance=2em]
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
585 \node[tape, active] {\pcp{$x_i$}{$y_i$}};
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
586 \node[tape] (a) {\pcp{$001$}{$00$}};
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
587 \node[tape] (b) {\pcp{$10$}{$11$}};
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
588 \node[tape] (c) {\pcp{$1$}{$01$}};
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
589 \end{scope}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
590 \node[below of=a] {$1$};
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
591 \node[below of=b] {$2$};
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
592 \node[below of=c] {$3$};
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
593 \end{tikzpicture}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
594 \end{center}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
595
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
596 \vfill
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
597
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
598 \begin{theorem}[]
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
599 Das PCP ist \alert{unentscheidbar}, aber semi-entscheidbar.
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
600 \end{theorem}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
601 \end{frame}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
602 }
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
603
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
604 \defineUnit{pcpbeispiel}{%
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
605 \begin{frame}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
606 \frametitle{PCP lösen}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
607 \setbeamercovered{dynamic}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
608
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
609 \begin{block}{Idee}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
610 \alert{Mögliche Lösungen} aufzählen, richtige Lösungen identifizieren
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
611 \end{block}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
612
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
613 \begin{center}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
614 \begin{tikzpicture}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
615 \begin{scope}[start chain, node distance=2em]
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
616 \node[tape, active] {\pcp{$x_i$}{$y_i$}};
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
617 \node[tape] (a) {\pcp{$001$}{$00$}};
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
618 \node[tape] (b) {\pcp{$01$}{$10$}};
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
619 \node[tape] (c) {\pcp{$1$}{$11$}};
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
620 \end{scope}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
621 \node[below of=a] {$1$};
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
622 \node[below of=b] {$2$};
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
623 \node[below of=c] {$3$};
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
624 \end{tikzpicture}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
625
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
626 \vspace{2em}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
627
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
628 \begin{tikzpicture}[grow=right, level distance = 2cm]
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
629 \tikzstyle{every node} = []
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
630 \tikzstyle{residual} = [rectangular, thin, fill=tumgreen!10, font=\scriptsize]
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
631 \tikzstyle{edge from parent} = [every edge]
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
632
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
633 \tikzstyle{level 1} = [sibling distance = 1.7cm]
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
634 \tikzstyle{level 2} = [sibling distance = 1.1cm]
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
635
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
636 \node[residual] {}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
637 child {
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
638 node[residual] {\pcp{$1$}{}}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
639 child {
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
640 node[residual] {\pcp{$1$}{}}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
641 child {
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
642 node[residual] {\pcp{$1$}{}}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
643 child {
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
644 node[residual]{$\ldots$}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
645 edge from parent
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
646 }
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
647 edge from parent
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
648 node[below] {$2$}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
649 }
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
650 child {
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
651 node[residual, active] {\pcp{}{}}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
652 edge from parent
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
653 node[above] {$3$}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
654 }
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
655 edge from parent
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
656 node[below] {$2$}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
657 }
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
658 child {
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
659 node[residual, active] {\pcp{}{}}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
660 edge from parent
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
661 node[above] {$3$}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
662 }
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
663 edge from parent
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
664 node[below] {$1$}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
665 }
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
666 child {
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
667 node[residual]{\pcp{}{$1$}}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
668 child {
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
669 node[residual]{\pcp{}{$11$}}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
670 child {
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
671 node[residual]{$\ldots$}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
672 edge from parent
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
673 node[above] {$3$}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
674 }
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
675 edge from parent
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
676 node[above] {$3$}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
677 }
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
678 edge from parent
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
679 node[above] {$3$}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
680 };
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
681
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
682 \uncover<2>{\node at (10cm, 0) {$L = \left\{ (12^*3)^+ \right\}$};}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
683 \end{tikzpicture}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
684 \end{center}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
685 \end{frame}
5d10471f5585 move frame-definitions out of presentations
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
686 }