replace DEFINITIONS by constants

4b4cd44b · Michael Leuschel · dfa653d7 · 4b4cd44b
Commit 4b4cd44b authored 5 years ago by Michael Leuschel
--- a/info4/kapitel-3/PDA-Kellerautomaten.ipynb
+++ b/info4/kapitel-3/PDA-Kellerautomaten.ipynb
@@ -31,7 +31,7 @@
  },
  {
   "cell_type": "code",
-   "execution_count": 59,
+   "execution_count": 1,
   "metadata": {},
   "outputs": [
    {
@@ -40,7 +40,7 @@
       "Loaded machine: PDA"
      ]
     },
-     "execution_count": 59,
+     "execution_count": 1,
     "metadata": {},
     "output_type": "execute_result"
    }
@@ -53,16 +53,18 @@
    " Z = {z0,z1}; // die Zustände des Automaten, z0 ist der Startzustand\n",
    " SYMBOLE={a,b, A, BOT, lambda} /* BOT = # = Bottom-Symbol im Keller*/\n",
    "DEFINITIONS\n",
-    " Σ == {a,b};   // das Eingabe-Alphabet\n",
-    " Γ == {A,BOT}; // das Kelleralphabet\n",
    " \n",
    " ANIMATION_FUNCTION_DEFAULT == {(1,1,z)};\n",
    " ANIMATION_FUNCTION == {2}*α ∪ {3}*(γ);\n",
    " ANIMATION_FUNCTION1 == {(1,0,\"z: \"),(2,0,\"α:\"),(3,0,\"γ:\")};\n",
    " ANIMATION_STR_JUSTIFY_LEFTx == TRUE;\n",
    " SET_PREF_PP_SEQUENCES == TRUE\n",
-    "CONSTANTS δ\n",
+    "CONSTANTS δ, Σ, Γ\n",
    "PROPERTIES\n",
+    " Σ = {a,b}    // das Eingabe-Alphabet\n",
+    " ∧\n",
+    " Γ = {A,BOT} // das Kelleralphabet\n",
+    " ∧\n",
    " /* Der PDA für {a^m b^m| m>=1} ; Beispiel von Info 4 (Folie 95ff) */\n",
    " δ = {     (z0,a,BOT)      ↦  (z0,[A,BOT]),\n",
    "           (z0,a,A)        ↦  (z0,[A,A]),\n",
@@ -104,7 +106,7 @@
  },
  {
   "cell_type": "code",
-   "execution_count": 60,
+   "execution_count": 2,
   "metadata": {},
   "outputs": [
    {
@@ -113,7 +115,7 @@
       "Machine constants set up using operation 0: $setup_constants()"
      ]
     },
-     "execution_count": 60,
+     "execution_count": 2,
     "metadata": {},
     "output_type": "execute_result"
    }
@@ -124,7 +126,7 @@
  },
  {
   "cell_type": "code",
-   "execution_count": 61,
+   "execution_count": 3,
   "metadata": {},
   "outputs": [
    {
@@ -133,7 +135,7 @@
       "Machine initialised using operation 1: $initialise_machine()"
      ]
     },
-     "execution_count": 61,
+     "execution_count": 3,
     "metadata": {},
     "output_type": "execute_result"
    }
@@ -144,7 +146,7 @@
  },
  {
   "cell_type": "code",
-   "execution_count": 62,
+   "execution_count": 4,
   "metadata": {},
   "outputs": [
    {
@@ -178,7 +180,7 @@
       "<Animation function visualisation>"
      ]
     },
-     "execution_count": 62,
+     "execution_count": 4,
     "metadata": {},
     "output_type": "execute_result"
    }

 %% Cell type:markdown id: tags:
 # PDA (Push Down Automata - Kellerautomaten)
 %% Cell type:markdown id: tags:
 Ein __(nichtdeterministischer) Kellerautomat__
 (kurz PDA für __push-down automaton__) ist ein $6$-Tupel
  $M = (\Sigma, \Gamma, Z, \delta , z_0, \#)$, wobei
 * $\Sigma$ das Eingabe-Alphabet ist,
 * $\Gamma$ das Kelleralphabet,
 * $Z$ eine endliche Menge von Zuständen,
 * $\delta : Z \times (\Sigma \cup \{\lambda\}) \times \Gamma
  \rightarrow \mathfrak{P}_e(Z \times \Gamma^{\ast})$ die
  Überführungsfunktion,
 * $z_0 \in Z$ der Startzustand,
 * $\# \in \Gamma$ das Bottom-Symbol im Keller.
 Anmerkung: $\mathfrak{P}_e(Z \times \Gamma^{\ast})$ ist die Menge aller
  __endlichen__ Teilmengen von $Z \times \Gamma^{\ast}$.
 %% Cell type:code id: tags:
 ``` prob
 ::load
 MACHINE PDA
 /* B Modell eines PDA */
 SETS
 Z = {z0,z1}; // die Zustände des Automaten, z0 ist der Startzustand
 SYMBOLE={a,b, A, BOT, lambda} /* BOT = # = Bottom-Symbol im Keller*/
 DEFINITIONS
- Σ == {a,b};   // das Eingabe-Alphabet
- Γ == {A,BOT}; // das Kelleralphabet
 ANIMATION_FUNCTION_DEFAULT == {(1,1,z)};
 ANIMATION_FUNCTION == {2}*α ∪ {3}*(γ);
 ANIMATION_FUNCTION1 == {(1,0,"z: "),(2,0,"α:"),(3,0,"γ:")};
 ANIMATION_STR_JUSTIFY_LEFTx == TRUE;
 SET_PREF_PP_SEQUENCES == TRUE
-CONSTANTS δ
+CONSTANTS δ, Σ, Γ
 PROPERTIES
+ Σ = {a,b}    // das Eingabe-Alphabet
+ ∧
+ Γ = {A,BOT} // das Kelleralphabet
+ ∧
 /* Der PDA für {a^m b^m| m>=1} ; Beispiel von Info 4 (Folie 95ff) */
 δ = {     (z0,a,BOT)      ↦  (z0,[A,BOT]),
           (z0,a,A)        ↦  (z0,[A,A]),
           (z0,b,A)        ↦  (z1,[]),
           (z1,lambda,BOT) ↦  (z1,[]),
           (z1,b,A)        ↦  (z1,[]) }
 // Anmerkung: δ ist hier als Relation anstatt als Funktion zu Mengen definiert
 //  Deshalb entspricht δ[{(z,a,g)}] in der B Maschine δ(z,a,g) aus dem Skript
 VARIABLES
  z, α, γ  // Konfiguration in dem sich der PDA befindet
 INVARIANT
 z ∈ Z ∧ // der aktuelle Zustand
 α ∈ seq(Σ) ∧ // der noch zu lesende Teil des Eingabeworts
 γ ∈ seq(Γ) // aktuelle Kellerinhalt
 INITIALISATION
  z := z0 ||
  γ := [BOT] || // Initialisierung des Stapels
  α := [a,a,b,b] // das Eingabewort
 OPERATIONS
 // die Operationen Schritt und LambdaSchritt modellieren
 // Schritte in der Ableitungsrelation
  Schritt(z‘,s) = PRE α ≠ ∅ ∧ γ ≠ ∅ ∧
                z‘↦s ∈ δ[{(z,first(α),first(γ))}] THEN
     z := z‘ || // in den neuen Zustand wechseln
     α := tail(α) || // das erste Symbol auf der Eingabe löschen
     γ := s^tail(γ) // s auf den Stapel packen
  END;
  LambdaSchritt(z‘,s) = PRE γ ≠ ∅ ∧
                      z‘↦s ∈ δ[{(z,lambda,first(γ))}] THEN
     z := z‘ ||  // in den neuen Zustand wechseln
     γ := s^tail(γ) // s auf den Stapel packen
  END;
  Akzeptieren = PRE γ = ∅ ∧ α = ∅ THEN
              /* Wir akzeptieren wenn Eingabe und Stapel leer sind */
   skip END
 END
 ```
 %% Output
    Loaded machine: PDA
 %% Cell type:code id: tags:
 ``` prob
 :constants
 ```
 %% Output
    Machine constants set up using operation 0: $setup_constants()
 %% Cell type:code id: tags:
 ``` prob
 :init
 ```
 %% Output
    Machine initialised using operation 1: $initialise_machine()
 %% Cell type:code id: tags:
 ``` prob
 :show
 ```
 %% Output
    <table style="font-family:monospace"><tbody>
    <tr>
    <td style="padding:10px">z: </td>
    <td style="padding:10px">z0</td>
    <td style="padding:0px"></td>
    <td style="padding:0px"></td>
    <td style="padding:0px"></td>
    </tr>
    <tr>
    <td style="padding:10px">α:</td>
    <td style="padding:10px">a</td>
    <td style="padding:10px">a</td>
    <td style="padding:10px">b</td>
    <td style="padding:10px">b</td>
    </tr>
    <tr>
    <td style="padding:10px">γ:</td>
    <td style="padding:10px">BOT</td>
    <td style="padding:0px"></td>
    <td style="padding:0px"></td>
    <td style="padding:0px"></td>
    </tr>
    </tbody></table>
    <Animation function visualisation>
 %% Cell type:code id: tags:
 ``` prob
 :browse
 ```
 %% Output
    Machine: PDA
    Sets: Z, SYMBOLE
    Constants: δ
    Variables: z, α, γ
    Operations:
    Schritt(z0,[A,BOT])
 %% Cell type:code id: tags:
 ``` prob
 :exec Schritt
 ```
 %% Output
    Executed operation: Schritt(z0,[A,BOT])
 %% Cell type:code id: tags:
 ``` prob
 :show
 ```
 %% Output
    <table style="font-family:monospace"><tbody>
    <tr>
    <td style="padding:10px">z: </td>
    <td style="padding:10px">z0</td>
    <td style="padding:0px"></td>
    <td style="padding:0px"></td>
    </tr>
    <tr>
    <td style="padding:10px">α:</td>
    <td style="padding:10px">a</td>
    <td style="padding:10px">b</td>
    <td style="padding:10px">b</td>
    </tr>
    <tr>
    <td style="padding:10px">γ:</td>
    <td style="padding:10px">A</td>
    <td style="padding:10px">BOT</td>
    <td style="padding:0px"></td>
    </tr>
    </tbody></table>
    <Animation function visualisation>
 %% Cell type:code id: tags:
 ``` prob
 (z,α,γ)
 ```
 %% Output
    $(\mathit{z0}\mapsto [a,\mathit{b},b]\mapsto [A,BOT])$
    (z0↦[a,b,b]↦[A,BOT])
 %% Cell type:code id: tags:
 ``` prob
 :browse
 ```
 %% Output
    Machine: PDA
    Sets: Z, SYMBOLE
    Constants: δ
    Variables: z, α, γ
    Operations:
    Schritt(z0,[A,A])
 %% Cell type:code id: tags:
 ``` prob
 :exec Schritt
 ```
 %% Output
    Executed operation: Schritt(z0,[A,A])
 %% Cell type:code id: tags:
 ``` prob
 :show
 ```
 %% Output
    <table style="font-family:monospace"><tbody>
    <tr>
    <td style="padding:10px">z: </td>
    <td style="padding:10px">z0</td>
    <td style="padding:0px"></td>
    <td style="padding:0px"></td>
    </tr>
    <tr>
    <td style="padding:10px">α:</td>
    <td style="padding:10px">b</td>
    <td style="padding:10px">b</td>
    <td style="padding:0px"></td>
    </tr>
    <tr>
    <td style="padding:10px">γ:</td>
    <td style="padding:10px">A</td>
    <td style="padding:10px">A</td>
    <td style="padding:10px">BOT</td>
    </tr>
    </tbody></table>
    <Animation function visualisation>
 %% Cell type:code id: tags:
 ``` prob
 :browse
 ```
 %% Output
    Machine: PDA
    Sets: Z, SYMBOLE
    Constants: δ
    Variables: z, α, γ
    Operations:
    Schritt(z1,[])
 %% Cell type:code id: tags:
 ``` prob
 :exec Schritt
 ```
 %% Output
    Executed operation: Schritt(z1,[])
 %% Cell type:code id: tags:
 ``` prob
 :show
 ```
 %% Output
    <table style="font-family:monospace"><tbody>
    <tr>
    <td style="padding:10px">z: </td>
    <td style="padding:10px">z1</td>
    <td style="padding:0px"></td>
    </tr>
    <tr>
    <td style="padding:10px">α:</td>
    <td style="padding:10px">b</td>
    <td style="padding:0px"></td>
    </tr>
    <tr>
    <td style="padding:10px">γ:</td>
    <td style="padding:10px">A</td>
    <td style="padding:10px">BOT</td>
    </tr>
    </tbody></table>
    <Animation function visualisation>
 %% Cell type:code id: tags:
 ``` prob
 :browse
 ```
 %% Output
    Machine: PDA
    Sets: Z, SYMBOLE
    Constants: δ
    Variables: z, α, γ
    Operations:
    Schritt(z1,[])
 %% Cell type:code id: tags:
 ``` prob
 :exec Schritt
 ```
 %% Output
    Executed operation: Schritt(z1,[])
 %% Cell type:code id: tags:
 ``` prob
 :show
 ```
 %% Output
    <table style="font-family:monospace"><tbody>
    <tr>
    <td style="padding:10px">z: </td>
    <td style="padding:10px">z1</td>
    </tr>
    <tr>
    <td style="padding:10px">α:</td>
    <td style="padding:0px"></td>
    </tr>
    <tr>
    <td style="padding:10px">γ:</td>
    <td style="padding:10px">BOT</td>
    </tr>
    </tbody></table>
    <Animation function visualisation>
 %% Cell type:code id: tags:
 ``` prob
 :browse
 ```
 %% Output
    Machine: PDA
    Sets: Z, SYMBOLE
    Constants: δ
    Variables: z, α, γ
    Operations:
    LambdaSchritt(z1,[])
 %% Cell type:code id: tags:
 ``` prob
 :exec LambdaSchritt
 ```
 %% Output
    Executed operation: LambdaSchritt(z1,[])
 %% Cell type:code id: tags:
 ``` prob
 :show
 ```
 %% Output
    <table style="font-family:monospace"><tbody>
    <tr>
    <td style="padding:10px">z: </td>
    <td style="padding:10px">z1</td>
    </tr>
    <tr>
    <td style="padding:10px">α:</td>
    <td style="padding:0px"></td>
    </tr>
    <tr>
    <td style="padding:10px">γ:</td>
    <td style="padding:0px"></td>
    </tr>
    </tbody></table>
    <Animation function visualisation>
 %% Cell type:code id: tags:
 ``` prob
 :browse
 ```
 %% Output
    Machine: PDA
    Sets: Z, SYMBOLE
    Constants: δ
    Variables: z, α, γ
    Operations:
    Akzeptieren()
 %% Cell type:code id: tags:
 ``` prob
 :exec Akzeptieren
 ```
 %% Output
    Executed operation: Akzeptieren()
 %% Cell type:markdown id: tags:
 Das Eingabewort ``aabb`` wurde akzeptiert.
 %% Cell type:markdown id: tags:
 ## PDA für eine kfG
 Aus einer kontextfreien Grammatik kann man einen PDA konstruieren der die gleiche Sprache akzeptiert.
 %% Cell type:code id: tags:
 ``` prob
 ::load
 MACHINE PDA_für_kfG
 /* B Modell eines PDA */
 SETS
 Z = {z0}; // die Zustände des Automaten, z0 ist der Startzustand
 SYMBOLE={a,b, S, C, lambda} /* BOT = # = Bottom-Symbol im Keller*/
 DEFINITIONS
 Σ == {a,b};   // das Eingabe-Alphabet
 BOT == S;
 Γ == {S,C}; // das Kelleralphabet
 ANIMATION_FUNCTION_DEFAULT == {(1,1,z)};
 ANIMATION_FUNCTION == {2}*α ∪ {3}*(γ);
 ANIMATION_FUNCTION1 == {(1,0,"z: "),(2,0,"α:"),(3,0,"γ:")};
 ANIMATION_STR_JUSTIFY_LEFTx == TRUE;
 SET_PREF_PP_SEQUENCES == TRUE
 CONSTANTS P, δ
 PROPERTIES
 /* Die Grammatik Regeln */
 P = { S ↦ [a,S,b], S ↦ [C],
       C ↦ [a,b] } ∧
 /* Berechnung von δ aus P */
  δ =  /* lässt sich eine Regel auf das Top-Symbol im Keller anwenden tue
          dies ohne etwas zu lesen :*/
         { lhs,rhs | ∃(A,q).( A↦q ∈ P ∧ lhs=(z0,lambda,A) ∧ rhs=(z0,q))}
         ∪
          /* ist das Top-Symbol im Keller ein Terminalzeichen a welches
             auf der Eingabe steht, so wird dies aus dem Keller gePOPt */
         { lhs,rhs | ∃a.(a∈Σ ∧ lhs = (z0,a,a) & rhs = (z0,[]))}
 VARIABLES
  z, α, γ  // Konfiguration in dem sich der PDA befindet
 INVARIANT
 z ∈ Z ∧ // der aktuelle Zustand
 α ∈ seq(Σ) ∧ // der noch zu lesende Teil des Eingabeworts
 γ ∈ seq(Γ) // aktuelle Kellerinhalt
 INITIALISATION
  z := z0 ||
  γ := [BOT] || // Initialisierung des Stapels
  α := [a,a,b,b] // das Eingabewort
 OPERATIONS
 // die Operationen Schritt und LambdaSchritt modellieren
 // Schritte in der Ableitungsrelation
  Schritt(z‘,s) = PRE α ≠ ∅ ∧ γ ≠ ∅ ∧
                z‘↦s ∈ δ[{(z,first(α),first(γ))}] THEN
     z := z‘ || // in den neuen Zustand wechseln
     α := tail(α) || // das erste Symbol auf der Eingabe löschen
     γ := s^tail(γ) // s auf den Stapel packen
  END;
  LambdaSchritt(z‘,s) = PRE γ ≠ ∅ ∧
                      z‘↦s ∈ δ[{(z,lambda,first(γ))}] THEN
     z := z‘ ||  // in den neuen Zustand wechseln
     γ := s^tail(γ) // s auf den Stapel packen
  END;
  Akzeptieren = PRE γ = ∅ ∧ α = ∅ THEN
              /* Wir akzeptieren wenn Eingabe und Stapel leer sind */
   skip END
 END
 ```
 %% Output
    Loaded machine: PDA_für_kfG
 %% Cell type:code id: tags:
 ``` prob
 :constants
 ```
 %% Output
    Machine constants set up using operation 0: $setup_constants()
 %% Cell type:code id: tags:
 ``` prob
 :init
 ```
 %% Output
    Machine initialised using operation 1: $initialise_machine()
 %% Cell type:code id: tags:
 ``` prob
 :table {z,x,X,z2,Xs| ((z,x,X)↦(z2,Xs)) : δ}
 ```
 %% Output
    |z|x|X|z2|Xs|
    |---|---|---|---|---|
    |$\mathit{z0}$|$\mathit{a}$|$\mathit{a}$|$\mathit{z0}$|$[]$|
    |$\mathit{z0}$|$\mathit{b}$|$\mathit{b}$|$\mathit{z0}$|$[]$|
    |$\mathit{z0}$|$\mathit{S}$|$\mathit{S}$|$\mathit{z0}$|$[]$|
    |$\mathit{z0}$|$\mathit{C}$|$\mathit{C}$|$\mathit{z0}$|$[]$|
    |$\mathit{z0}$|$\mathit{lambda}$|$\mathit{S}$|$\mathit{z0}$|$[C]$|
    |$\mathit{z0}$|$\mathit{lambda}$|$\mathit{S}$|$\mathit{z0}$|$[a,\mathit{S},b]$|
    |$\mathit{z0}$|$\mathit{lambda}$|$\mathit{C}$|$\mathit{z0}$|$[a,b]$|
    |$\mathit{z0}$|$\mathit{lambda}$|$\mathit{lambda}$|$\mathit{z0}$|$[]$|
    z	x	X	z2	Xs
    z0	a	a	z0	[]
    z0	b	b	z0	[]
    z0	S	S	z0	[]
    z0	C	C	z0	[]
    z0	lambda	S	z0	[C]
    z0	lambda	S	z0	[a,S,b]
    z0	lambda	C	z0	[a,b]
    z0	lambda	lambda	z0	[]
 %% Cell type:code id: tags:
 ``` prob
 :show
 ```
 %% Output
    <table style="font-family:monospace"><tbody>
    <tr>
    <td style="padding:10px">z: </td>
    <td style="padding:10px">z0</td>
    <td style="padding:0px"></td>
    <td style="padding:0px"></td>
    <td style="padding:0px"></td>
    </tr>
    <tr>
    <td style="padding:10px">α:</td>
    <td style="padding:10px">a</td>
    <td style="padding:10px">a</td>
    <td style="padding:10px">b</td>
    <td style="padding:10px">b</td>
    </tr>
    <tr>
    <td style="padding:10px">γ:</td>
    <td style="padding:10px">S</td>
    <td style="padding:0px"></td>
    <td style="padding:0px"></td>
    <td style="padding:0px"></td>
    </tr>
    </tbody></table>
    <Animation function visualisation>
 %% Cell type:code id: tags:
 ``` prob
 :browse
 ```
 %% Output
    Machine: PDA_für_kfG
    Sets: Z, SYMBOLE
    Constants: P, δ
    Variables: z, α, γ
    Operations:
    LambdaSchritt(z0,[C])
    LambdaSchritt(z0,[a,S,b])
 %% Cell type:code id: tags:
 ``` prob
 :exec LambdaSchritt s = [a,S,b]
 ```
 %% Output
    Executed operation: LambdaSchritt(z0,[a,S,b])
 %% Cell type:code id: tags:
 ``` prob
 :show
 ```
 %% Output
    <table style="font-family:monospace"><tbody>
    <tr>
    <td style="padding:10px">z: </td>
    <td style="padding:10px">z0</td>
    <td style="padding:0px"></td>
    <td style="padding:0px"></td>
    <td style="padding:0px"></td>
    </tr>
    <tr>
    <td style="padding:10px">α:</td>
    <td style="padding:10px">a</td>
    <td style="padding:10px">a</td>
    <td style="padding:10px">b</td>
    <td style="padding:10px">b</td>
    </tr>
    <tr>
    <td style="padding:10px">γ:</td>
    <td style="padding:10px">a</td>
    <td style="padding:10px">S</td>
    <td style="padding:10px">b</td>
    <td style="padding:0px"></td>
    </tr>
    </tbody></table>
    <Animation function visualisation>
 %% Cell type:code id: tags:
 ``` prob
 :browse
 ```
 %% Output
    Machine: PDA_für_kfG
    Sets: Z, SYMBOLE
    Constants: P, δ
    Variables: z, α, γ
    Operations:
    Schritt(z0,[])
 %% Cell type:code id: tags:
 ``` prob
 :exec Schritt
 ```
 %% Output
    Executed operation: Schritt(z0,[])
 %% Cell type:code id: tags:
 ``` prob
 :show
 ```
 %% Output
    <table style="font-family:monospace"><tbody>
    <tr>
    <td style="padding:10px">z: </td>
    <td style="padding:10px">z0</td>
    <td style="padding:0px"></td>
    <td style="padding:0px"></td>
    </tr>
    <tr>
    <td style="padding:10px">α:</td>
    <td style="padding:10px">a</td>
    <td style="padding:10px">b</td>
    <td style="padding:10px">b</td>
    </tr>
    <tr>
    <td style="padding:10px">γ:</td>
    <td style="padding:10px">S</td>
    <td style="padding:10px">b</td>
    <td style="padding:0px"></td>
    </tr>
    </tbody></table>
    <Animation function visualisation>
 %% Cell type:code id: tags:
 ``` prob
 :browse
 ```
 %% Output
    Machine: PDA_für_kfG
    Sets: Z, SYMBOLE
    Constants: P, δ
    Variables: z, α, γ
    Operations:
    LambdaSchritt(z0,[C])
    LambdaSchritt(z0,[a,S,b])
 %% Cell type:code id: tags:
 ``` prob
 :exec LambdaSchritt s = [C]
 ```
 %% Output
    Executed operation: LambdaSchritt(z0,[C])
 %% Cell type:code id: tags:
 ``` prob
 :show
 ```
 %% Output
    <table style="font-family:monospace"><tbody>
    <tr>
    <td style="padding:10px">z: </td>
    <td style="padding:10px">z0</td>
    <td style="padding:0px"></td>
    <td style="padding:0px"></td>
    </tr>
    <tr>
    <td style="padding:10px">α:</td>
    <td style="padding:10px">a</td>
    <td style="padding:10px">b</td>
    <td style="padding:10px">b</td>
    </tr>
    <tr>
    <td style="padding:10px">γ:</td>
    <td style="padding:10px">C</td>
    <td style="padding:10px">b</td>
    <td style="padding:0px"></td>
    </tr>
    </tbody></table>
    <Animation function visualisation>
 %% Cell type:code id: tags:
 ``` prob
 :browse
 ```
 %% Output
    Machine: PDA_für_kfG
    Sets: Z, SYMBOLE
    Constants: P, δ
    Variables: z, α, γ
    Operations:
    LambdaSchritt(z0,[a,b])
 %% Cell type:code id: tags:
 ``` prob
 :exec LambdaSchritt s=[a,b]
 ```
 %% Output
    Executed operation: LambdaSchritt(z0,[a,b])
 %% Cell type:code id: tags:
 ``` prob
 :show
 ```
 %% Output
    <table style="font-family:monospace"><tbody>
    <tr>
    <td style="padding:10px">z: </td>
    <td style="padding:10px">z0</td>
    <td style="padding:0px"></td>
    <td style="padding:0px"></td>
    </tr>
    <tr>
    <td style="padding:10px">α:</td>
    <td style="padding:10px">a</td>
    <td style="padding:10px">b</td>
    <td style="padding:10px">b</td>
    </tr>
    <tr>
    <td style="padding:10px">γ:</td>
    <td style="padding:10px">a</td>
    <td style="padding:10px">b</td>
    <td style="padding:10px">b</td>
    </tr>
    </tbody></table>
    <Animation function visualisation>
 %% Cell type:code id: tags:
 ``` prob
 :browse
 ```
 %% Output
    Machine: PDA_für_kfG
    Sets: Z, SYMBOLE
    Constants: P, δ
    Variables: z, α, γ
    Operations:
    Schritt(z0,[])
 %% Cell type:code id: tags:
 ``` prob
 :exec Schritt
 ```
 %% Output
    Executed operation: Schritt(z0,[])
 %% Cell type:code id: tags:
 ``` prob
 :show
 ```
 %% Output
    <table style="font-family:monospace"><tbody>
    <tr>
    <td style="padding:10px">z: </td>
    <td style="padding:10px">z0</td>
    <td style="padding:0px"></td>
    </tr>
    <tr>
    <td style="padding:10px">α:</td>
    <td style="padding:10px">b</td>
    <td style="padding:10px">b</td>
    </tr>
    <tr>
    <td style="padding:10px">γ:</td>
    <td style="padding:10px">b</td>
    <td style="padding:10px">b</td>
    </tr>
    </tbody></table>
    <Animation function visualisation>
 %% Cell type:code id: tags:
 ``` prob
 :exec Schritt
 ```
 %% Output
    Executed operation: Schritt(z0,[])
 %% Cell type:code id: tags:
 ``` prob
 :show
 ```
 %% Output
    <table style="font-family:monospace"><tbody>
    <tr>
    <td style="padding:10px">z: </td>
    <td style="padding:10px">z0</td>
    </tr>
    <tr>
    <td style="padding:10px">α:</td>
    <td style="padding:10px">b</td>
    </tr>
    <tr>
    <td style="padding:10px">γ:</td>
    <td style="padding:10px">b</td>
    </tr>
    </tbody></table>
    <Animation function visualisation>
 %% Cell type:code id: tags:
 ``` prob
 :exec Schritt
 ```
 %% Output
    Executed operation: Schritt(z0,[])
 %% Cell type:code id: tags:
 ``` prob
 :show
 ```
 %% Output
    <table style="font-family:monospace"><tbody>
    <tr>
    <td style="padding:10px">z: </td>
    <td style="padding:10px">z0</td>
    </tr>
    <tr>
    <td style="padding:10px">α:</td>
    <td style="padding:0px"></td>
    </tr>
    <tr>
    <td style="padding:10px">γ:</td>
    <td style="padding:0px"></td>
    </tr>
    </tbody></table>
    <Animation function visualisation>
 %% Cell type:code id: tags:
 ``` prob
 :exec Akzeptieren
 ```
 %% Output
    Executed operation: Akzeptieren()
 %% Cell type:markdown id: tags:
 Das Wort ``aabb`` wird sowohl von der Grammatik generiert als auch von diesem generierten PDA akzeptiert.
 %% Cell type:code id: tags:
 ``` prob
 ```