minor change

42411c6d · Michael Leuschel · 7ffec864 · 42411c6d
Commit 42411c6d authored May 8, 2020 by Michael Leuschel
--- a/info4/kapitel-2/NFA_nach_DFA.ipynb
+++ b/info4/kapitel-2/NFA_nach_DFA.ipynb
@@ -2735,14 +2735,15 @@
    "Es gilt:\n",
    "* Es gibt einen NFA für $L_n$  mit $n+1$ Zuständen.\n",
    "\n",
-    "Anmerkung: im Skript stand fälschlicherweise $n+2$ Zustände.\n",
    "(Beweis: Einfache Modifikation der NFAs für $L_2$ und $L_1$ in \n",
-    "den vorigen Abbildungen.)"
+    "den vorigen Abbildungen.)\n",
+    "\n",
+    "Anmerkung: im Skript stand fälschlicherweise $n+2$ Zustände."
   ]
  },
  {
   "cell_type": "code",
-   "execution_count": 134,
+   "execution_count": 158,
   "metadata": {},
   "outputs": [
    {
@@ -2751,7 +2752,7 @@
       "Loaded machine: NFA_DFA_Explosion"
      ]
     },
-     "execution_count": 134,
+     "execution_count": 158,
     "metadata": {},
     "output_type": "execute_result"
    }
@@ -2801,7 +2802,7 @@
  },
  {
   "cell_type": "code",
-   "execution_count": 146,
+   "execution_count": 159,
   "metadata": {},
   "outputs": [
    {
@@ -2810,7 +2811,7 @@
       "Changed to state with index -1"
      ]
     },
-     "execution_count": 146,
+     "execution_count": 159,
     "metadata": {},
     "output_type": "execute_result"
    }
@@ -2821,16 +2822,16 @@
  },
  {
   "cell_type": "code",
-   "execution_count": 147,
+   "execution_count": 160,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
-       "Machine constants set up using operation 4: $setup_constants()"
+       "Machine constants set up using operation 0: $setup_constants()"
      ]
     },
-     "execution_count": 147,
+     "execution_count": 160,
     "metadata": {},
     "output_type": "execute_result"
    }
@@ -2841,16 +2842,16 @@
  },
  {
   "cell_type": "code",
-   "execution_count": 148,
+   "execution_count": 161,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
-       "Machine initialised using operation 5: $initialise_machine()"
+       "Machine initialised using operation 1: $initialise_machine()"
      ]
     },
-     "execution_count": 148,
+     "execution_count": 161,
     "metadata": {},
     "output_type": "execute_result"
    }
@@ -2861,7 +2862,7 @@
  },
  {
   "cell_type": "code",
-   "execution_count": 149,
+   "execution_count": 162,
   "metadata": {},
   "outputs": [
    {
@@ -2872,7 +2873,7 @@
       "Preference changed: DOT_NORMAL_NODE_SHAPE = circle\n"
      ]
     },
-     "execution_count": 149,
+     "execution_count": 162,
     "metadata": {},
     "output_type": "execute_result"
    }
@@ -2883,7 +2884,7 @@
  },
  {
   "cell_type": "code",
-   "execution_count": 150,
+   "execution_count": 163,
   "metadata": {},
   "outputs": [
    {
@@ -2969,7 +2970,7 @@
       "<Dot visualization: expr_as_graph [(\"0\",{x,y|y:δ(x, 0)})]>"
      ]
     },
-     "execution_count": 150,
+     "execution_count": 163,
     "metadata": {},
     "output_type": "execute_result"
    }
@@ -2987,7 +2988,7 @@
  },
  {
   "cell_type": "code",
-   "execution_count": 151,
+   "execution_count": 164,
   "metadata": {},
   "outputs": [
    {
@@ -2997,7 +2998,7 @@
       "Preference changed: DOT_LIMIT_PAGE_SIZE = TRUE\n"
      ]
     },
-     "execution_count": 151,
+     "execution_count": 164,
     "metadata": {},
     "output_type": "execute_result"
    }
@@ -3008,7 +3009,7 @@
  },
  {
   "cell_type": "code",
-   "execution_count": 152,
+   "execution_count": 165,
   "metadata": {},
   "outputs": [
    {
@@ -3320,7 +3321,7 @@
       "<Dot visualization: custom_graph []>"
      ]
     },
-     "execution_count": 152,
+     "execution_count": 165,
     "metadata": {},
     "output_type": "execute_result"
    }
@@ -3338,7 +3339,7 @@
  },
  {
   "cell_type": "code",
-   "execution_count": 153,
+   "execution_count": 166,
   "metadata": {},
   "outputs": [
    {
@@ -3347,7 +3348,7 @@
       "Executed operation: Compute_Reachable()"
      ]
     },
-     "execution_count": 153,
+     "execution_count": 166,
     "metadata": {},
     "output_type": "execute_result"
    }
@@ -3358,7 +3359,7 @@
  },
  {
   "cell_type": "code",
-   "execution_count": 154,
+   "execution_count": 167,
   "metadata": {},
   "outputs": [
    {
@@ -3370,7 +3371,7 @@
       "{{0},{0,1},{0,2},{0,3},{0,1,2},{0,1,3},{0,1,2,3},{0,2,3}}"
      ]
     },
-     "execution_count": 154,
+     "execution_count": 167,
     "metadata": {},
     "output_type": "execute_result"
    }
@@ -3388,7 +3389,7 @@
  },
  {
   "cell_type": "code",
-   "execution_count": 157,
+   "execution_count": 168,
   "metadata": {},
   "outputs": [
    {
@@ -3400,7 +3401,7 @@
       "8"
      ]
     },
-     "execution_count": 157,
+     "execution_count": 168,
     "metadata": {},
     "output_type": "execute_result"
    }
@@ -3411,7 +3412,7 @@
  },
  {
   "cell_type": "code",
-   "execution_count": 155,
+   "execution_count": 169,
   "metadata": {},
   "outputs": [
    {
@@ -3583,7 +3584,7 @@
       "<Dot visualization: custom_graph []>"
      ]
     },
-     "execution_count": 155,
+     "execution_count": 169,
     "metadata": {},
     "output_type": "execute_result"
    }

 %% Cell type:markdown id: tags:

 # NFA - Nichtdeterministische Automaten

 Nun erweitern wir die Überführungsfunktion in der Definition eines DFA
 und bezeichnen die neuen Automaten als NFA.

 Ein __nichtdeterministischer endlicher Automat__
 (kurz NFA) ist ein  Quintupel $M = (\Sigma, Z, \delta , S, F)$, wobei
 * $\Sigma$ ein Alphabet ist,
 * $Z$ eine endliche Menge von Zuständen mit
  $\Sigma \cap Z = \emptyset$,
 * $\delta : Z \times \Sigma \rightarrow ℙ(Z)$ die
  Überführungsfunktion (hier: $ℙ(Z)$ ist die Potenzmenge
  von $Z$, also die Menge aller Teilmengen von $Z$),
 * $S \subseteq Z$ die Menge der Startzustände und
 * $F \subseteq Z$ die Menge der Endzustände (Finalzustände).

 %% Cell type:markdown id: tags:

 Die Definition ändert sich im Vergleich zum DFA für die Überführungsfunktion $\delta$ und die Startzustände. Im DFA gab es genau einen Startzustand $z_0 \in Z$,
 hier ist es eine Menge $S \subseteq Z$.
 Im DFA war $\delta$ vom Typ:
 * $\delta : Z \times \Sigma \rightarrow Z$ die Überführungsfunktion

 Hier ist ein Beispiel NFA:

 %% Cell type:code id: tags:

 ``` prob
 ::load
 MACHINE NFA
 SETS
   Z = {z0,z1,z2,z3}
 CONSTANTS Σ, S, F, δ
 PROPERTIES
 F ⊆ Z ∧ S ⊆ Z ∧
 δ ∈ (Z×Σ) → ℙ(Z)
 ∧
 /* Der Automat von Folie 21: */
 Σ = {0,1} ∧
 S = {z0} ∧ F = {z2} ∧
 δ = {     (z0,0)↦{z0}, (z0,1)↦{z0,z1},
           (z1,0)↦{z2}, (z1,1)↦{z2},
           (z2,0)↦{z3}, (z2,1)↦{z3},
           (z3,0)↦{z3}, (z3,1)↦{z3} }
 DEFINITIONS // Für den Zustandsgraphen:
  CUSTOM_GRAPH_NODES1 == rec(shape:"doublecircle",nodes:F); // Endzustände
  CUSTOM_GRAPH_NODES2 == rec(shape:"circle",nodes:Z\F); // andere Zustände
  CUSTOM_GRAPH_NODES3 == rec(shape:"none",color:"white",style:"none",nodes:{""});
  CUSTOM_GRAPH_EDGES1 == rec(color:"red",label:"0",edges:{x,y|y∈δ(x,0)});
  CUSTOM_GRAPH_EDGES2 == rec(color:"green",label:"1",edges:{x,y|y∈δ(x,1)});
  CUSTOM_GRAPH_EDGES3 == rec(color:"black",label:"",edges:{""}*S) // Kanten für Startknoten
 END
 ```

 %% Output

    Loaded machine: NFA

 %% Cell type:code id: tags:

 ``` prob
 :constants
 ```

 %% Output

    Machine constants set up using operation 0: $setup_constants()

 %% Cell type:markdown id: tags:

 Die Übergangsfunktion $\delta$ gibt us für einen Zustand und ein Symbol die möglichen nächsten Zustände an.

 %% Cell type:code id: tags:

 ``` prob
 δ(z0,0)
 ```

 %% Output

    $\{\mathit{z0}\}$
    {z0}

 %% Cell type:markdown id: tags:

 Dieser Automat ist nichtdeterministisch, für den Zustand 0 und die Eingabe 1 gibt es zwei mögliche Zielknoten:

 %% Cell type:code id: tags:

 ``` prob
 δ(z0,1)
 ```

 %% Output

    $\{\mathit{z0},\mathit{z1}\}$
    {z0,z1}

 %% Cell type:code id: tags:

 ``` prob
 card(δ(z0,1)) > 1
 ```

 %% Output

    $\mathit{TRUE}$
    TRUE

 %% Cell type:markdown id: tags:

 Wir können die Übergangsfunktion $\delta$ des Automaten auch als Tabelle darstellen:

 %% Cell type:code id: tags:

 ``` prob
 :table {x,a,y|y∈δ(x,a)}
 ```

 %% Output

    |x|a|y|
    |---|---|---|
    |$\mathit{z0}$|$0$|$\mathit{z0}$|
    |$\mathit{z0}$|$1$|$\mathit{z0}$|
    |$\mathit{z0}$|$1$|$\mathit{z1}$|
    |$\mathit{z1}$|$0$|$\mathit{z2}$|
    |$\mathit{z1}$|$1$|$\mathit{z2}$|
    |$\mathit{z2}$|$0$|$\mathit{z3}$|
    |$\mathit{z2}$|$1$|$\mathit{z3}$|
    |$\mathit{z3}$|$0$|$\mathit{z3}$|
    |$\mathit{z3}$|$1$|$\mathit{z3}$|
    x	a	y
    z0	0	z0
    z0	1	z0
    z0	1	z1
    z1	0	z2
    z1	1	z2
    z2	0	z3
    z2	1	z3
    z3	0	z3
    z3	1	z3

 %% Cell type:markdown id: tags:

 Der Zustandsgraph eines NFA ist ähnlich zu dem eines DFA definiert. Die einzigen Unterschiede sind:
 * es gibt möglicherweise mehrere Startzustände
 * es gibt eine Kante von x nach y mit Label a falls $y \in \delta(x,a)$

 Alle Kanten mit dem Label "0" sind:

 %% Cell type:code id: tags:

 ``` prob
 {x,y|y∈δ(x,1)}
 ```

 %% Output

    $\{(\mathit{z0}\mapsto \mathit{z0}),(\mathit{z0}\mapsto \mathit{z1}),(\mathit{z1}\mapsto \mathit{z2}),(\mathit{z2}\mapsto \mathit{z3}),(\mathit{z3}\mapsto \mathit{z3})\}$
    {(z0↦z0),(z0↦z1),(z1↦z2),(z2↦z3),(z3↦z3)}

 %% Cell type:markdown id: tags:

 und grafisch ist der komplette Zustandsgraph:

 %% Cell type:code id: tags:

 ``` prob
 :pref DOT_LIMIT_PAGE_SIZE=FALSE DOT_HORIZONTAL_LAYOUT=TRUE
 ```

 %% Output

    Preference changed: DOT_HORIZONTAL_LAYOUT = TRUE
    Preference changed: DOT_LIMIT_PAGE_SIZE = FALSE

 %% Cell type:code id: tags:

 ``` prob
 :dot custom_graph
 ```

 %% Output


    <Dot visualization: custom_graph []>

 %% Cell type:markdown id: tags:

 ### Sprache eines NFAs

 Die __erweiterte Überführungsfunktion__
  $\widehat{\delta} : ℙ(Z) \times \Sigma^* \rightarrow
  ℙ(Z)$ von $M$ ist induktiv definiert:
 * $\widehat{\delta}(Z', \lambda)   =   Z'$
 * $\widehat{\delta}(Z', ax)   =  \bigcup_{z \in Z'} \widehat{\delta}(\delta(z,a), x) $

 für alle $Z' \subseteq Z$, $a \in \Sigma$ und $x \in \Sigma^*$.

 %% Cell type:markdown id: tags:

 Beim DFA war der zweite Fall etwas einfacher:
 * $\widehat{\delta}(z, ax)       =  \widehat{\delta}(\delta(z,a), x) $

 Die erweiterte Überführungsfunktion ist in folgender B Maschine als rekursive Funktion $\delta s$ umgesetzt worden:

 %% Cell type:code id: tags:

 ``` prob
 ::load
 MACHINE NFA
 SETS
   Z = {z0,z1,z2,z3}
 ABSTRACT_CONSTANTS L, δs
 CONSTANTS Σ, S, F, δ
 PROPERTIES
 F ⊆ Z ∧ S ⊆ Z ∧
 δ ∈ (Z×Σ) → ℙ(Z) ∧

 /* Definition der erweiterten Überführungsfunktion */
 δs ∈ (ℙ(Z)×seq(Σ)) → ℙ(Z) ∧
 δs = λ(Z′,s).(Z′⊆Z ∧ s∈seq(Σ) |
           IF s=[] THEN Z′
           ELSE         ⋃(z).(z∈Z′|δs(δ(z,first(s)),tail(s))) END)
 ∧
 /* Die vom Automaten akzeptierte Sprache L */
 L = {ω|ω∈seq(Σ) ∧ δs(S,ω) ∩ F ≠ ∅}
 ∧
 /* Der Automat von Folie 21: */
 Σ = {0,1} ∧
 S = {z0} ∧ F = {z2} ∧
 δ = {     (z0,0)↦{z0}, (z0,1)↦{z0,z1},
           (z1,0)↦{z2}, (z1,1)↦{z2},
           (z2,0)↦{z3}, (z2,1)↦{z3},
           (z3,0)↦{z3}, (z3,1)↦{z3} }
 DEFINITIONS // Für den Zustandsgraphen:
  CUSTOM_GRAPH_NODES1 == rec(shape:"doublecircle",nodes:F); // Endzustände
  CUSTOM_GRAPH_NODES2 == rec(shape:"circle",nodes:Z\F); // andere Zustände
  CUSTOM_GRAPH_NODES3 == rec(shape:"none",color:"white",style:"none",nodes:{""});
  CUSTOM_GRAPH_EDGES1 == rec(color:"red",label:"0",edges:{x,y|y∈δ(x,0)});
  CUSTOM_GRAPH_EDGES2 == rec(color:"green",label:"1",edges:{x,y|y∈δ(x,1)});
  CUSTOM_GRAPH_EDGES3 == rec(color:"black",label:"",edges:{""}*S) // Kanten für Startknoten
 END
 ```

 %% Output

    Loaded machine: NFA

 %% Cell type:code id: tags:

 ``` prob
 :constants
 ```

 %% Output

    Machine constants set up using operation 0: $setup_constants()

 %% Cell type:markdown id: tags:

 Wir generieren noch einmal den Zustandgraphen:

 %% Cell type:code id: tags:

 ``` prob
 :pref DOT_LIMIT_PAGE_SIZE=FALSE DOT_HORIZONTAL_LAYOUT=TRUE
 ```

 %% Output

    Preference changed: DOT_HORIZONTAL_LAYOUT = TRUE
    Preference changed: DOT_LIMIT_PAGE_SIZE = FALSE

 %% Cell type:code id: tags:

 ``` prob
 :dot custom_graph
 ```

 %% Output


    <Dot visualization: custom_graph []>

 %% Cell type:markdown id: tags:

 Die Funktion $\widehat{\delta}$ berechnet die möglichen Zustände nach dem Abarbeiten eines Wortes. Zum Beispiel, kann sich der Automat nach dem Abarbeiten des Präfixes 111 in folgenden Zuständen befinden.
 Für das leere Wort bekommen wir die Startzustände zurück:

 %% Cell type:code id: tags:

 ``` prob
 δs({z0},[])
 ```

 %% Output

    $\{\mathit{z0}\}$
    {z0}

 %% Cell type:markdown id: tags:

 Das leere Wort $\lambda$ wird nicht akzeptiert da $\widehat{\delta}(S,\lambda) \cap F$ leer ist:

 %% Cell type:code id: tags:

 ``` prob
 δs({z0},[]) ∩ F
 ```

 %% Output

    $\renewcommand{\emptyset}{\mathord\varnothing}\emptyset$
    ∅

 %% Cell type:markdown id: tags:

 Schauen wir uns nun die Wörter $0$ und $01$ an.
 Wir haben
 * $\widehat{\delta}(\{z_0\},0)$ =
 * $\bigcup_{z \in \{z_0\}} \widehat{\delta}(\delta(z,0), \lambda)$ =
 * $\delta(z_0,0)$.

 %% Cell type:code id: tags:

 ``` prob
 δs({z0},[0])
 ```

 %% Output

    $\{\mathit{z0}\}$
    {z0}

 %% Cell type:code id: tags:

 ``` prob
 δ(z0,0)
 ```

 %% Output

    $\{\mathit{z0}\}$
    {z0}

 %% Cell type:code id: tags:

 ``` prob
 δs(δ(z0,0),[])
 ```

 %% Output

    $\{\mathit{z0}\}$
    {z0}

 %% Cell type:markdown id: tags:

 Wir haben per Definition von $\widehat{\delta}$:
 * $\widehat{\delta}(\{z_0\},01)$ =
 * $\bigcup_{z \in \{z_0\}} \widehat{\delta}(\delta(z,0), 1)$ =
 * $\widehat{\delta}(\delta(z_0,0), 1)$ =
 * $\widehat{\delta}(\{z_0\}, 1)$ =
 * $\bigcup_{z \in \{z_0\}} \widehat{\delta}(\delta(z,1), \lambda)$ =
 * $\delta(z_0,1)$.

 %% Cell type:code id: tags:

 ``` prob
 δs({z0},[0,1])
 ```

 %% Output

    $\{\mathit{z0},\mathit{z1}\}$
    {z0,z1}

 %% Cell type:code id: tags:

 ``` prob
 δ(z0,1)
 ```

 %% Output

    $\{\mathit{z0},\mathit{z1}\}$
    {z0,z1}

 %% Cell type:markdown id: tags:

 Das Wort $01$ wird nicht akzeptiert da $\widehat{\delta}(S,01) \cap F$ leer ist:

 %% Cell type:code id: tags:

 ``` prob
 δs({z0},[0,1]) ∩ F
 ```

 %% Output

    $\renewcommand{\emptyset}{\mathord\varnothing}\emptyset$
    ∅

 %% Cell type:markdown id: tags:

 Wir haben wieder per Definition von $\widehat{\delta}$:
 * $\widehat{\delta}(\{z_0\},011)$ =
 * $\bigcup_{z \in \{z_0\}} \widehat{\delta}(\delta(z,0), 11)$ =
 * $\widehat{\delta}(\delta(z_0,0), 11)$ =
 * $\widehat{\delta}(\{z_0\}, 11)$ =
 * $\bigcup_{z \in \{z_0\}} \widehat{\delta}(\delta(z,1), 1)$ =
 * $\widehat{\delta}(\delta(z_0,1), 1)$ =
 * $\widehat{\delta}(\{z_0,z_1\}, 1)$ =
 * $\bigcup_{z \in \{z_0,z_1\}} \widehat{\delta}(\delta(z,1), \lambda)$ =
 * $\delta(z_0,1) \cup \delta(z_1,1)$.

 %% Cell type:code id: tags:

 ``` prob
 δs({z0},[0,1,1])
 ```

 %% Output

    $\{\mathit{z0},\mathit{z1},\mathit{z2}\}$
    {z0,z1,z2}

 %% Cell type:code id: tags:

 ``` prob
 δ(z0,1) ∪ δ(z1,1)
 ```

 %% Output

    $\{\mathit{z0},\mathit{z1},\mathit{z2}\}$
    {z0,z1,z2}

 %% Cell type:markdown id: tags:

 Das Wort $0111$ wird akzeptiert da $\widehat{\delta}(S,0111) \cap F$ nicht leer ist:

 %% Cell type:code id: tags:

 ``` prob
 δs({z0},[0,1,1]) ∩ F
 ```

 %% Output

    $\{\mathit{z2}\}$
    {z2}

 %% Cell type:markdown id: tags:

 Schauen wir uns nun das Wort $0111$ an. Hier erhalten wir mit $\widehat{\delta}$ die komplette Menge Z:

 %% Cell type:code id: tags:

 ``` prob
 δs({z0},[0,1,1,1])
 ```

 %% Output

    $\{\mathit{z0},\mathit{z1},\mathit{z2},\mathit{z3}\}$
    {z0,z1,z2,z3}

 %% Cell type:markdown id: tags:

 Das Wort $0111$ wird akzeptiert da $\widehat{\delta}(S,0111) \cap F$ nicht leer ist:

 %% Cell type:code id: tags:

 ``` prob
 δs({z0},[0,1,1,1]) ∩ F
 ```

 %% Output

    $\{\mathit{z2}\}$
    {z2}

 %% Cell type:markdown id: tags:

 Die von diesem NFA generierte Sprache ist:
 * $L(M) = \{w \in \{0,1\}^* \mid w = u 1 v \text{ mit $u \in
  \{0,1\}^*$ und $v \in \{0,1\}$}\}$.

 %% Cell type:markdown id: tags:

 ## DFA versus NFA, Satz von Rabin und Scott}
 Es stellt sich die Frage, ob NFAs mächtiger sind als DFAs.
 Die  vielleicht überraschende Antwort lautet: Nein.

 ### Theorem (Rabin und Scott)
 Jede von einem NFA akzeptierte Sprache kann auch von einem DFA akzeptiert
 werden.

 %% Cell type:code id: tags:

 ``` prob
 :dot custom_graph
 ```

 %% Output


    <Dot visualization: custom_graph []>

 %% Cell type:markdown id: tags:


 #### Beweis
 Sei $M = (\Sigma, Z, \delta , S, E)$ ein NFA.
 Konstruiere einen zu
  $M$ äquivalenten DFA
  $M' = (\Sigma, ℙ(Z), \delta' ,z_0', F)$ wie folgt:
 * Zustandsmenge von $M'$: die Potenzmenge $ℙ(Z)$ von $Z$,
 * $\delta'(Z' , a) = \widehat{\delta}(Z',a)$ für alle $Z' \subseteq Z$ und $a \in \Sigma$,
 * $z_0'=S$,
 * $F = \{ Z' \subseteq Z \mid Z' \cap E \neq \emptyset\}$.


 %% Cell type:markdown id: tags:

 Für den oben geladen Automaten können wir diese Konstruktion illustrieren.

 %% Cell type:code id: tags:

 ``` prob
 :dot custom_graph
 ```

 %% Output


    <Dot visualization: custom_graph []>

 %% Cell type:markdown id: tags:

 Die Potenzmenge der Zustände ist:

 %% Cell type:code id: tags:

 ``` prob
 ℙ(Z)
 ```

 %% Output

    $\renewcommand{\emptyset}{\mathord\varnothing}\{\emptyset,\{\mathit{z0}\},\{\mathit{z0},\mathit{z1}\},\{\mathit{z0},\mathit{z2}\},\{\mathit{z0},\mathit{z3}\},\{\mathit{z1}\},\{\mathit{z0},\mathit{z1},\mathit{z2}\},\{\mathit{z0},\mathit{z1},\mathit{z3}\},\{\mathit{z1},\mathit{z2}\},\{\mathit{z1},\mathit{z3}\},\{\mathit{z0},\mathit{z1},\mathit{z2},\mathit{z3}\},\{\mathit{z2}\},\{\mathit{z0},\mathit{z2},\mathit{z3}\},\{\mathit{z1},\mathit{z2},\mathit{z3}\},\{\mathit{z2},\mathit{z3}\},\{\mathit{z3}\}\}$
    {∅,{z0},{z0,z1},{z0,z2},{z0,z3},{z1},{z0,z1,z2},{z0,z1,z3},{z1,z2},{z1,z3},{z0,z1,z2,z3},{z2},{z0,z2,z3},{z1,z2,z3},{z2,z3},{z3}}

 %% Cell type:markdown id: tags:

 Jedes Element der Potenzmenge (ist eine Menge) und wird zu einem Zustand des NFAs.
 Tabellarisch können wir $\widehat{\delta}$ für $ℙ(Z)$ und Wörter der Länge 1 wie folgt ausrechnen.
 Anmerkung: $z'\in\widehat{\delta}(x,a)$ bedeutet: es ist möglich von einem Zustand $z$ aus der Menge $x$ einen Übergang im NFA zu wählen, so dass man den Zustand $z'$ erreicht.

 %% Cell type:code id: tags:

 ``` prob
 :table {x,a,y| a∈Σ & x∈ℙ(Z) & y=δs(x,[a])}
 ```

 %% Output

    |x|a|y|
    |---|---|---|
    |$\renewcommand{\emptyset}{\mathord\varnothing}\renewcommand{\emptyset}{\mathord\varnothing}\renewcommand{\emptyset}{\mathord\varnothing}\renewcommand{\emptyset}{\mathord\varnothing}\emptyset$|$0$|$\emptyset$|
    |$\emptyset$|$1$|$\emptyset$|
    |$\{\mathit{z0}\}$|$0$|$\{\mathit{z0}\}$|
    |$\{\mathit{z0}\}$|$1$|$\{\mathit{z0},\mathit{z1}\}$|
    |$\{\mathit{z0},\mathit{z1}\}$|$0$|$\{\mathit{z0},\mathit{z2}\}$|
    |$\{\mathit{z0},\mathit{z1}\}$|$1$|$\{\mathit{z0},\mathit{z1},\mathit{z2}\}$|
    |$\{\mathit{z0},\mathit{z2}\}$|$0$|$\{\mathit{z0},\mathit{z3}\}$|
    |$\{\mathit{z0},\mathit{z2}\}$|$1$|$\{\mathit{z0},\mathit{z1},\mathit{z3}\}$|
    |$\{\mathit{z0},\mathit{z3}\}$|$0$|$\{\mathit{z0},\mathit{z3}\}$|
    |$\{\mathit{z0},\mathit{z3}\}$|$1$|$\{\mathit{z0},\mathit{z1},\mathit{z3}\}$|
    |$\{\mathit{z1}\}$|$0$|$\{\mathit{z2}\}$|
    |$\{\mathit{z1}\}$|$1$|$\{\mathit{z2}\}$|
    |$\{\mathit{z0},\mathit{z1},\mathit{z2}\}$|$0$|$\{\mathit{z0},\mathit{z2},\mathit{z3}\}$|
    |$\{\mathit{z0},\mathit{z1},\mathit{z2}\}$|$1$|$\{\mathit{z0},\mathit{z1},\mathit{z2},\mathit{z3}\}$|
    |$\{\mathit{z0},\mathit{z1},\mathit{z3}\}$|$0$|$\{\mathit{z0},\mathit{z2},\mathit{z3}\}$|
    |$\{\mathit{z0},\mathit{z1},\mathit{z3}\}$|$1$|$\{\mathit{z0},\mathit{z1},\mathit{z2},\mathit{z3}\}$|
    |$\{\mathit{z1},\mathit{z2}\}$|$0$|$\{\mathit{z2},\mathit{z3}\}$|
    |$\{\mathit{z1},\mathit{z2}\}$|$1$|$\{\mathit{z2},\mathit{z3}\}$|
    |$\{\mathit{z1},\mathit{z3}\}$|$0$|$\{\mathit{z2},\mathit{z3}\}$|
    |$\{\mathit{z1},\mathit{z3}\}$|$1$|$\{\mathit{z2},\mathit{z3}\}$|
    |$\{\mathit{z0},\mathit{z1},\mathit{z2},\mathit{z3}\}$|$0$|$\{\mathit{z0},\mathit{z2},\mathit{z3}\}$|
    |$\{\mathit{z0},\mathit{z1},\mathit{z2},\mathit{z3}\}$|$1$|$\{\mathit{z0},\mathit{z1},\mathit{z2},\mathit{z3}\}$|
    |$\{\mathit{z2}\}$|$0$|$\{\mathit{z3}\}$|
    |$\{\mathit{z2}\}$|$1$|$\{\mathit{z3}\}$|
    |$\{\mathit{z0},\mathit{z2},\mathit{z3}\}$|$0$|$\{\mathit{z0},\mathit{z3}\}$|
    |$\{\mathit{z0},\mathit{z2},\mathit{z3}\}$|$1$|$\{\mathit{z0},\mathit{z1},\mathit{z3}\}$|
    |$\{\mathit{z1},\mathit{z2},\mathit{z3}\}$|$0$|$\{\mathit{z2},\mathit{z3}\}$|
    |$\{\mathit{z1},\mathit{z2},\mathit{z3}\}$|$1$|$\{\mathit{z2},\mathit{z3}\}$|
    |$\{\mathit{z2},\mathit{z3}\}$|$0$|$\{\mathit{z3}\}$|
    |$\{\mathit{z2},\mathit{z3}\}$|$1$|$\{\mathit{z3}\}$|
    |$\{\mathit{z3}\}$|$0$|$\{\mathit{z3}\}$|
    |$\{\mathit{z3}\}$|$1$|$\{\mathit{z3}\}$|
    x	a	y
    {}	0	{}
    {}	1	{}
    {z0}	0	{z0}
    {z0}	1	{z0,z1}
    {z0,z1}	0	{z0,z2}
    {z0,z1}	1	{z0,z1,z2}
    {z0,z2}	0	{z0,z3}
    {z0,z2}	1	{z0,z1,z3}
    {z0,z3}	0	{z0,z3}
    {z0,z3}	1	{z0,z1,z3}
    {z1}	0	{z2}
    {z1}	1	{z2}
    {z0,z1,z2}	0	{z0,z2,z3}
    {z0,z1,z2}	1	{z0,z1,z2,z3}
    {z0,z1,z3}	0	{z0,z2,z3}
    {z0,z1,z3}	1	{z0,z1,z2,z3}
    {z1,z2}	0	{z2,z3}
    {z1,z2}	1	{z2,z3}
    {z1,z3}	0	{z2,z3}
    {z1,z3}	1	{z2,z3}
    {z0,z1,z2,z3}	0	{z0,z2,z3}
    {z0,z1,z2,z3}	1	{z0,z1,z2,z3}
    {z2}	0	{z3}
    {z2}	1	{z3}
    {z0,z2,z3}	0	{z0,z3}
    {z0,z2,z3}	1	{z0,z1,z3}
    {z1,z2,z3}	0	{z2,z3}
    {z1,z2,z3}	1	{z2,z3}
    {z2,z3}	0	{z3}
    {z2,z3}	1	{z3}
    {z3}	0	{z3}
    {z3}	1	{z3}

 %% Cell type:markdown id: tags:

 Graphisch lässt sich der Automat wie folgt darstellen; die Start und Endzustände sind noch nicht schön markiert.

 %% Cell type:code id: tags:

 ``` prob
 :pref DOT_DECOMPOSE_NODES=FALSE DOT_NORMAL_NODE_SHAPE=circle DOT_HORIZONTAL_LAYOUT=TRUE
 ```

 %% Output

    Preference changed: DOT_HORIZONTAL_LAYOUT = TRUE
    Preference changed: DOT_DECOMPOSE_NODES = FALSE
    Preference changed: DOT_NORMAL_NODE_SHAPE = circle

 %% Cell type:code id: tags:

 ``` prob
 :dot expr_as_graph ("0",{x,y| x∈ℙ(Z) & δs(x,[0]) = y},
                    "1",{x,y| x∈ℙ(Z) & δs(x,[1]) = y},
                    "start", {x,y|x=y & x={z0}},
                    "end", {x,y|x=y & x∩F ≠ ∅})
 ```

 %% Output


    <Dot visualization: expr_as_graph [("0",{x,y|x:POW(Z) & δs(x, [0])=y})]>

 %% Cell type:markdown id: tags:

 Mit den CUSTOM_GRAPH Fähigkeiten der B Maschine kann man diese Konstruktion schöner darstellen:

 %% Cell type:code id: tags:

 ``` prob
 ::load
 MACHINE NFA_nach_DFA
 SETS
   Z = {z0,z1,z2,z3}
 ABSTRACT_CONSTANTS L, δs
 CONSTANTS Σ, S, F, δ
 PROPERTIES
 F ⊆ Z ∧ S ⊆ Z ∧
 δ ∈ (Z×Σ) → ℙ(Z) ∧

 /* Definition der erweiterten Überführungsfunktion */
 δs ∈ (ℙ(Z)×seq(Σ)) → ℙ(Z) ∧
 δs = λ(Z′,s).(Z′⊆Z ∧ s∈seq(Σ) |
           IF s=[] THEN Z′
           ELSE         ⋃(z).(z∈Z′|δs(δ(z,first(s)),tail(s))) END)
 ∧
 /* Die vom Automaten akzeptierte Sprache L */
 L = {ω|ω∈seq(Σ) ∧ δs(S,ω) ∩ F ≠ ∅}
 ∧
 /* Der Automat von Folie 21: */
 Σ = {0,1} ∧
 S = {z0} ∧ F = {z2} ∧
 δ = {     (z0,0)↦{z0}, (z0,1)↦{z0,z1},
           (z1,0)↦{z2}, (z1,1)↦{z2},
           (z2,0)↦{z3}, (z2,1)↦{z3},
           (z3,0)↦{z3}, (z3,1)↦{z3} }
 DEFINITIONS // Für den Zustandsgraphen des DFAs nach Potenzmengenkonstruktion:
  SET_PREF_DOT_DECOMPOSE_NODES == FALSE;
  CUSTOM_GRAPH_NODES1 == rec(shape:"doublecircle",nodes:{x|x∈ℙ(Z) & x/\F /= {}}); // Endzustände
  CUSTOM_GRAPH_NODES2 == rec(shape:"circle",nodes:{x|x∈ℙ(Z) & x/\F = {}}); // andere Zustände
  CUSTOM_GRAPH_NODES3 == rec(shape:"none",color:"white",style:"none",nodes:{""});
  CUSTOM_GRAPH_EDGES1 == rec(color:"red",label:"0",edges:{x,y|x∈ℙ(Z) & y=δs(x,[0])});
  CUSTOM_GRAPH_EDGES2 == rec(color:"green",label:"1",edges:{x,y|x∈ℙ(Z) & y=δs(x,[1])});
  CUSTOM_GRAPH_EDGES3 == rec(color:"black",label:"",edges:{""}*{S}) // Kanten für Startknoten
 END
 ```

 %% Output

    Loaded machine: NFA_nach_DFA

 %% Cell type:code id: tags:

 ``` prob
 :constants
 ```

 %% Output

    Machine constants set up using operation 0: $setup_constants()

 %% Cell type:code id: tags:

 ``` prob
 :pref DOT_LIMIT_PAGE_SIZE=FALSE DOT_HORIZONTAL_LAYOUT=TRUE
 ```

 %% Output

    Preference changed: DOT_HORIZONTAL_LAYOUT = TRUE
    Preference changed: DOT_LIMIT_PAGE_SIZE = FALSE

 %% Cell type:code id: tags:

 ``` prob
 :dot custom_graph
 ```

 %% Output


    <Dot visualization: custom_graph []>

 %% Cell type:markdown id: tags:

 #### Beweis


 Offenbar sind der DFA $M'$ und der NFA $M$ äquivalent, denn für alle $x = a_1 a_2 \cdots a_n$
 in $\Sigma^*$ gilt:

 \begin{eqnarray*}
 x \in L(M)
 & \Longleftrightarrow & \widehat{\delta}(S,x) \cap E \neq \emptyset \\
 & \Longleftrightarrow & \mbox{es gibt eine Folge von Teilmengen} \\
 &        & \mbox{$Z_1 , Z_2, \ldots , Z_n \subseteq Z$ mit $\widehat{\delta}(S,a_1)=Z_1$,}\\
 &        & \mbox{$\widehat{\delta}(Z_1,a_2)=Z_2$, $\ldots$,
                  $\widehat{\delta}(Z_{n-1},a_{n})=Z_n$ und} \\
 &        & \mbox{$Z_n \cap E  \neq \emptyset$} \\
 & \Longleftrightarrow & \mbox{es gibt eine Folge von Teilmengen} \\
 &        & \mbox{$Z_1 , Z_2, \ldots , Z_n \subseteq Z$ mit $\delta'(S,a_1)=Z_1$,}\\
 &        & \mbox{$\delta'(Z_1,a_2)=Z_2$, $\ldots$,
                  $\delta'(Z_{n-1},a_{n})=Z_n$ und} \\
 &        & \mbox{$Z_n \cap E  \neq \emptyset$} \\
 & \Longleftrightarrow & Z_n = \widehat{\delta'}(z_0',x) \in F \\
 & \Longleftrightarrow & x \in L(M') .
 \end{eqnarray*}

 Somit ist $L(M') = L(M)$.

 %% Cell type:markdown id: tags:

 ### Weitere Beispiele

  Wir modifizieren den NFA aus dem obigen Beispiel etwas und
  betrachten den folgenden um einen Zustand kleineren NFA
  $M=(\Sigma, Z, \delta , S, E)$:


 Dieser NFA akzeptiert die Sprache aller Wörter über $\{0,1\}^*$, die
 an letzter Stelle eine $1$ haben.

 %% Cell type:code id: tags:

 ``` prob
 ::load
 MACHINE NFA
 SETS
   Z = {z0,z1,z2}
 ABSTRACT_CONSTANTS L, δs
 CONSTANTS Σ, S, F, δ
 PROPERTIES
 F ⊆ Z ∧ S ⊆ Z ∧
 δ ∈ (Z×Σ) → ℙ(Z) ∧

 /* Definition der erweiterten Überführungsfunktion */
 δs ∈ (ℙ(Z)×seq(Σ)) → ℙ(Z) ∧
 δs = λ(Z′,s).(Z′⊆Z ∧ s∈seq(Σ) |
           IF s=[] THEN Z′
           ELSE         ⋃(z).(z∈Z′|δs(δ(z,first(s)),tail(s))) END)
 ∧
 /* Die vom Automaten akzeptierte Sprache L */
 L = {ω|ω∈seq(Σ) ∧ δs(S,ω) ∩ F ≠ ∅}
 ∧
 /* Der Automat von Folie 28: */
 Σ = {0,1} ∧
 S = {z0} ∧ F = {z1} ∧
 δ = {     (z0,0)↦{z0}, (z0,1)↦{z0,z1},
           (z1,0)↦{z2}, (z1,1)↦{z2},
           (z2,0)↦{z2}, (z2,1)↦{z2} }
 DEFINITIONS // Für den Zustandsgraphen des DFAs nach Potenzmengenkonstruktion:
  SET_PREF_DOT_DECOMPOSE_NODES == FALSE;
  CUSTOM_GRAPH_NODES1 == rec(shape:"doublecircle",nodes:{x|x∈ℙ(Z) & x/\F /= {}}); // Endzustände
  CUSTOM_GRAPH_NODES2 == rec(shape:"circle",nodes:{x|x∈ℙ(Z) & x/\F = {}}); // andere Zustände
  CUSTOM_GRAPH_NODES3 == rec(shape:"none",color:"white",style:"none",nodes:{""});
  CUSTOM_GRAPH_EDGES1 == rec(color:"red",label:"0",edges:{x,y|x∈ℙ(Z) & y=δs(x,[0])});
  CUSTOM_GRAPH_EDGES2 == rec(color:"green",label:"1",edges:{x,y|x∈ℙ(Z) & y=δs(x,[1])});
  CUSTOM_GRAPH_EDGES3 == rec(color:"black",label:"",edges:{""}*{S}) // Kanten für Startknoten
 END
 ```

 %% Output

    Loaded machine: NFA

 %% Cell type:code id: tags:

 ``` prob
 :constants
 ```

 %% Output

    Machine constants set up using operation 0: $setup_constants()

 %% Cell type:code id: tags:

 ``` prob
 :pref DOT_DECOMPOSE_NODES=FALSE DOT_NORMAL_NODE_SHAPE=circle  DOT_HORIZONTAL_LAYOUT=TRUE
 ```

 %% Output

    Preference changed: DOT_HORIZONTAL_LAYOUT = TRUE
    Preference changed: DOT_DECOMPOSE_NODES = FALSE
    Preference changed: DOT_NORMAL_NODE_SHAPE = circle

 %% Cell type:code id: tags:

 ``` prob
 :dot expr_as_graph ("0",{x,y|y∈δ(x,0)},"1",{x,y|y∈δ(x,1)})
 ```

 %% Output


    <Dot visualization: expr_as_graph [("0",{x,y|y:δ(x, 0)})]>

 %% Cell type:markdown id: tags:

 Wir konstruieren nun einen zu $M$ äquivalenten DFA $M' = (\Sigma,
  Z', \delta' , S, F)$ gemäß dem Satz von Rabin und Scott:

 %% Cell type:code id: tags:

 ``` prob
 :pref DOT_LIMIT_PAGE_SIZE=FALSE DOT_HORIZONTAL_LAYOUT=TRUE
 ```

 %% Output

    Preference changed: DOT_HORIZONTAL_LAYOUT = TRUE
    Preference changed: DOT_LIMIT_PAGE_SIZE = FALSE

 %% Cell type:code id: tags:

 ``` prob
 :dot custom_graph
 ```

 %% Output


    <Dot visualization: custom_graph []>

 %% Cell type:markdown id: tags:

 Die Zustände $\emptyset$, $\{z_1\}$, $\{z_2\}$, $\{z_1,z_2\}$ können
 vom Startzustand $\{z_0\}$ nicht erreicht werden und werden zur
 Vereinfachung weggelassen.

 %% Cell type:markdown id: tags:

 Wir betrachten für $n \geq 1$ die Sprache

 \begin{eqnarray*}
 L_n & = & \{x\in\{0,1\}^*  \mid
            \text{ der $n$-te Buchstabe von hinten in }
            x \text{ ist } 1 \} \\
    & = & \{x \in \{0,1\}^* \mid x = u 1 v \text{ mit $u \in
            \{0,1\}^*$ und $v \in \{0,1\}^{n-1}$}\}.
 \end{eqnarray*}

 Es gilt:
 * Es gibt einen NFA für $L_n$  mit $n+1$ Zuständen.

-Anmerkung: im Skript stand fälschlicherweise $n+2$ Zustände.
 (Beweis: Einfache Modifikation der NFAs für $L_2$ und $L_1$ in
 den vorigen Abbildungen.)

+Anmerkung: im Skript stand fälschlicherweise $n+2$ Zustände.
+
 %% Cell type:code id: tags:

 ``` prob
 ::load
 MACHINE NFA_DFA_Explosion
 ABSTRACT_CONSTANTS δs
 CONSTANTS Σ, Z, S, F, δ, n
 PROPERTIES
 F ⊆ Z ∧ S ⊆ Z ∧
 δ ∈ (Z×Σ) → ℙ(Z) ∧

 /* Definition der erweiterten Überführungsfunktion */
 δs = λ(Z′,s).(Z′⊆Z ∧ s∈seq(Σ) |
           IF s=[] THEN Z′
           ELSE         ⋃(z).(z∈Z′|δs(δ(z,first(s)),tail(s))) END)

 ∧
 /* Für die Automaten ab Folie 31: */
 Σ = {0,1} ∧
 Z = 0..(n) ∧
 S = {0} ∧
 n ∈ 0..8 ∧
 F = {n} ∧
 δ = {     (0,0)↦{0}, (0,1)↦{0,1},
           (n,0)↦{}, (n,1)↦{}
           } \/
        λ(z,i).(z∈1..(n-1) & i∈Σ | {z+1})
 ASSERTIONS
  δs ∈ (ℙ(Z)×seq(Σ)) → ℙ(INTEGER)
 VARIABLES Reachable
 INVARIANT Reachable <: POW(Z)
 INITIALISATION Reachable := POW(Z)
 OPERATIONS Compute_Reachable = // Berechne erreichbaren Konfigurationen von S aus
   BEGIN Reachable := closure({x,y| x:POW(Z) & (y=δs(x,[0]) or y= δs(x,[1]))}) [ {S} ] END
 DEFINITIONS // Für den Zustandsgraphen des DFAs nach Potenzmengenkonstruktion:
  SET_PREF_DOT_DECOMPOSE_NODES == FALSE;
  CUSTOM_GRAPH_NODES1 == rec(shape:"doublecircle",nodes:{x|x∈Reachable & x/\F /= {}}); // Endzustände
  CUSTOM_GRAPH_NODES2 == rec(shape:"circle",nodes:{x|x∈Reachable & x/\F = {}}); // andere Zustände
  CUSTOM_GRAPH_NODES3 == rec(shape:"none",color:"white",style:"none",nodes:{""});
  CUSTOM_GRAPH_EDGES1 == rec(color:"red",label:"0",edges:{x,y|x∈Reachable & y=δs(x,[0])});
  CUSTOM_GRAPH_EDGES2 == rec(color:"green",label:"1",edges:{x,y|x∈Reachable & y=δs(x,[1])});
  CUSTOM_GRAPH_EDGES3 == rec(color:"black",label:"",edges:{""}*{S}) // Kanten für Startknoten
 END
 ```

 %% Output

    Loaded machine: NFA_DFA_Explosion

 %% Cell type:code id: tags:

 ``` prob
 :goto -1
 ```

 %% Output

    Changed to state with index -1

 %% Cell type:code id: tags:

 ``` prob
 :constants n=3
 ```

 %% Output

-    Machine constants set up using operation 4: $setup_constants()
+    Machine constants set up using operation 0: $setup_constants()

 %% Cell type:code id: tags:

 ``` prob
 :init
 ```

 %% Output

-    Machine initialised using operation 5: $initialise_machine()
+    Machine initialised using operation 1: $initialise_machine()

 %% Cell type:code id: tags:

 ``` prob
 :pref DOT_DECOMPOSE_NODES=FALSE DOT_NORMAL_NODE_SHAPE=circle  DOT_HORIZONTAL_LAYOUT=TRUE
 ```

 %% Output

    Preference changed: DOT_HORIZONTAL_LAYOUT = TRUE
    Preference changed: DOT_DECOMPOSE_NODES = FALSE
    Preference changed: DOT_NORMAL_NODE_SHAPE = circle

 %% Cell type:code id: tags:

 ``` prob
 :dot expr_as_graph ("0",{x,y|y∈δ(x,0)},"1",{x,y|y∈δ(x,1)})
 ```

 %% Output


    <Dot visualization: expr_as_graph [("0",{x,y|y:δ(x, 0)})]>

 %% Cell type:markdown id: tags:

 Wir schauen uns nun den NFA mit allen möglichen Untermengen von Z an (bei grösseren Werten von n vorher ```:pref DOT_ENGINE=sfdp``` ausführen):

 %% Cell type:code id: tags:

 ``` prob
 :pref DOT_LIMIT_PAGE_SIZE=TRUE DOT_HORIZONTAL_LAYOUT=TRUE
 ```

 %% Output

    Preference changed: DOT_HORIZONTAL_LAYOUT = TRUE
    Preference changed: DOT_LIMIT_PAGE_SIZE = TRUE

 %% Cell type:code id: tags:

 ``` prob
 :dot custom_graph
 ```

 %% Output


    <Dot visualization: custom_graph []>

 %% Cell type:markdown id: tags:

 Wir können diesen Graphen auch auf die erreichbaren Zustände beschränken:

 %% Cell type:code id: tags:

 ``` prob
 :exec Compute_Reachable
 ```

 %% Output

    Executed operation: Compute_Reachable()

 %% Cell type:code id: tags:

 ``` prob
 Reachable
 ```

 %% Output

    $\{\{0\},\{0,1\},\{0,2\},\{0,3\},\{0,1,2\},\{0,1,3\},\{0,1,2,3\},\{0,2,3\}\}$
    {{0},{0,1},{0,2},{0,3},{0,1,2},{0,1,3},{0,1,2,3},{0,2,3}}

 %% Cell type:markdown id: tags:

 Die Anzahl der Zustände ist $2^n$:

 %% Cell type:code id: tags:

 ``` prob
 card(Reachable)
 ```

 %% Output

    $8$
    8

 %% Cell type:code id: tags:

 ``` prob
 :dot custom_graph
 ```

 %% Output


    <Dot visualization: custom_graph []>

 %% Cell type:code id: tags:

 ``` prob
 ```