info4/kapitel-2/RegulaereAusdruecke.ipynb

 %% Cell type:markdown id: tags:
 
 # Reguläre Ausdrücke
 
 Sei $\Sigma$ ein Alphabet.
 Die __Menge der regulären Ausdrücke__ (über
   $\Sigma$) ist definiert durch:
 * $\emptyset$ und $\lambda$ sind reguläre Ausdrücke.
 * Jedes $a \in \Sigma$ ist ein regulärer Ausdruck.
 *  Sind $\alpha$ und $\beta$ reguläre Ausdrücke, so sind auch
  * $\alpha \beta$,
  * $(\alpha + \beta)$ und
  * $(\alpha)^{\ast}$
 * reguläre Ausdrücke.
 * Nichts sonst ist ein regulärer Ausdruck.
 
 
 
 %% Cell type:markdown id: tags:
 
 ## Sprache regulärer Ausdrücke
 
 Sei $\Sigma$ ein Alphabet.
 Jedem regulären Ausdruck $\gamma$ ist in
   eindeutiger Weise eine Sprache $L(\gamma) \subseteq \Sigma^*$
   zugeordnet (wir sagen: $\gamma$ beschreibt
       $L(\gamma)$), die so definiert ist:
 
 $L(\gamma)$ =
 * $\emptyset$ falls $\gamma = \emptyset$
 * $\{\lambda\}$ falls $\gamma = \lambda$
 * $\{a\}$ falls $\gamma = a$ für ein $a \in \Sigma$
 * $L(\alpha) L(\beta)$ falls $\gamma = \alpha \beta$
 * $L(\alpha) \cup L(\beta)$ falls $\gamma = (\alpha + \beta)$
 * $L(\alpha)^{*}$ falls $\gamma = (\alpha)^{*}$.
 
 %% Cell type:markdown id: tags:
 
 Zwei reguläre Ausdrücke $\alpha_1$ und $\alpha_2$ heißen
  __äquivalent__ (kurz $\alpha_1 \sim \alpha_2$), falls
   $L(\alpha_1)=L(\alpha_2)$.
 
 %% Cell type:markdown id: tags:
 
 Es sei $\Sigma=\{a,b\}$.
 Der reguläre Ausdruck
 * $\alpha_1 = (\lambda + a(a+b)^{*})$
 beschreibt die Sprache
 * $L(\alpha_1)$ =
 * $L(\lambda + a(a+b)^{*})$ =
 * $L(\lambda) \cup L(a(a+b)^{*})$ =
 * $\{\lambda\} \cup L(a)L((a+b)^{*})$ =
 * $\{\lambda\} \cup \{a\}(L(a+b))^{*}$ =
 * $\{\lambda\} \cup \{a\}(L(a)\cup L(b))^{*}$ =
 * $\{\lambda\} \cup \{a\}(\{a,b\})^{*}$ =
 * $\{\lambda\} \cup \{ax \mid x \in \{a,b\}^{*}\}$
 d.h. das leere Wort und alle Wörter über $\Sigma$, die mit $a$
 beginnen.
 
 Der reguläre Ausdruck
 * $\alpha_2 = ((a+b)^* ab)$
 beschreibt die Sprache:
 * $L(\alpha_2) = \{xab \mid x \in \{a,b\}^{*}\}$
 d.h. alle Wörter über $\Sigma$, die mit $ab$ enden.
 
 %% Cell type:markdown id: tags:
 
 ## Reguläre Ausdrücke in der Praxis
 
 Um mit den praktischen Aspekten der regulären Ausdrücke zu experimentieren laden wir eine Bibliothek.
 In dieser Bibliothek wird der Plus Operator anders geschrieben: ```a|b```.
 
 Es gibt auch nicht den regulären Ausdruck $\emptyset$, aber dafür viele andere (abgeleitete) Operatoren (sogenannter syntaktischer Zucker), zum Beispiel:
 * $\alpha^+$ als Kürzel für $\alpha(\alpha)^*$
 * [a-z] als Kürzel für $(a+b+c+d+...+z)$
 
 
 %% Cell type:code id: tags:
 
 ``` prob
 ::load
 MACHINE Regex
 DEFINITIONS "LibraryRegex.def"
 END
 ```
 
 %% Output
 
     Loaded machine: Regex
 
 %% Cell type:code id: tags:
 
 ``` prob
 :init
 ```
 
 %% Output
 
-    Machine initialised using operation 0: $initialise_machine()
+    Executed operation: INITIALISATION()
 
 %% Cell type:markdown id: tags:
 
 Mit ```REGEX_MATCH(w,r)``` können wir prüfen ob ein Wort ```w``` von einem regulären Ausdruck ```r``` generiert wird:
 
 %% Cell type:code id: tags:
 
 ``` prob
 REGEX_MATCH("a","a")
 ```
 
 %% Output
 
     $\mathit{TRUE}$
     TRUE
 
 %% Cell type:code id: tags:
 
 ``` prob
 REGEX_MATCH("a","a|b")
 ```
 
 %% Output
 
     $\mathit{TRUE}$
     TRUE
 
 %% Cell type:code id: tags:
 
 ``` prob
 REGEX_MATCH("aaaaaaa","a*")
 ```
 
 %% Output
 
     $\mathit{TRUE}$
     TRUE
 
 %% Cell type:code id: tags:
 
 ``` prob
 REGEX_MATCH("","a*")
 ```
 
 %% Output
 
     $\mathit{TRUE}$
     TRUE
 
 %% Cell type:markdown id: tags:
 
 Mit ```REGEX_SEARCH(w,i,r)``` können wir prüfen ob in einem Wort ```w``` ab der Position ```i``` ein Teilwort von ```r``` generiert wird.
 Wenn ja werden die erste Position und das längste Teilwort das von dort aus akzeptiert wird ausgegeben.
 
 %% Cell type:code id: tags:
 
 ``` prob
 REGEX_SEARCH("xxxaabc",1,"a*b")
 ```
 
 %% Output
 
-    $\renewcommand{\emptyset}{\mathord\varnothing}\mathit{rec}(\mathit{length}\in 3,\mathit{position}\in 4,\mathit{string}\in\text{"aab"},\mathit{submatches}\in\emptyset)$
+    $\def\emptyset{\mathord\varnothing}\mathit{rec}(\mathit{length}\in 3,\mathit{position}\in 4,\mathit{string}\in\text{"aab"},\mathit{submatches}\in\emptyset)$
     rec(length∈3,position∈4,string∈"aab",submatches∈∅)
 
 %% Cell type:markdown id: tags:
 
 Mit Mit ```REGEX_SEARCH_ALL(w,r)``` können wir in einem Wort ```w``` nach allen längsten Teilworten suchen die von ```r``` generiert werden.
 
 %% Cell type:code id: tags:
 
 ``` prob
 REGEX_SEARCH_ALL("aabcbbca","(a|b)+")
 ```
 
 %% Output
 
     $\{(1\mapsto\text{"aab"}),(2\mapsto\text{"bb"}),(3\mapsto\text{"a"})\}$
     {(1↦"aab"),(2↦"bb"),(3↦"a")}
 
 %% Cell type:markdown id: tags:
 
 Zum Experimentieren definieren wir einen Auszug aus dem Faust
 (Quelle: The Project Gutenberg EBook of Faust: Der Tragödie erster Teil, by  Johann Wolfgang von Goethe. Lizenz siehe www.gutenberg.net).
 
 %% Cell type:code id: tags:
 
 ``` prob
 :let txt  '''
 FAUST:
   Habe nun, ach!  Philosophie,
   Juristerei und Medizin,
   Und leider auch Theologie
   Durchaus studiert, mit heißem Bemühn.
   Da steh ich nun, ich armer Tor!
   Und bin so klug als wie zuvor;
   Heiße Magister, heiße Doktor gar
   Und ziehe schon an die zehen Jahr
   Herauf, herab und quer und krumm
   Meine Schüler an der Nase herum-
   Und sehe, daß wir nichts wissen können!
   Das will mir schier das Herz verbrennen.
   Zwar bin ich gescheiter als all die Laffen,
   Doktoren, Magister, Schreiber und Pfaffen;
   Mich plagen keine Skrupel noch Zweifel,
   Fürchte mich weder vor Hölle noch Teufel-
   Dafür ist mir auch alle Freud entrissen,
   Bilde mir nicht ein, was Rechts zu wissen,
   Bilde mir nicht ein, ich könnte was lehren,
   Die Menschen zu bessern und zu bekehren.
   Auch hab ich weder Gut noch Geld,
   Noch Ehr und Herrlichkeit der Welt;
   Es möchte kein Hund so länger leben!
   Drum hab ich mich der Magie ergeben,
   Ob mir durch Geistes Kraft und Mund
   Nicht manch Geheimnis würde kund;
   Daß ich nicht mehr mit saurem Schweiß
   Zu sagen brauche, was ich nicht weiß;
   Daß ich erkenne, was die Welt
   Im Innersten zusammenhält,
   Schau alle Wirkenskraft und Samen,
   Und tu nicht mehr in Worten kramen.
   '''
 ```
 
 %% Output
 
     $\text{"\nFAUST:\n  Habe nun, ach!  Philosophie,\n  Juristerei und Medizin,\n  Und leider auch Theologie\n  Durchaus studiert, mit heißem Bemühn.\n  Da steh ich nun, ich armer Tor!\n  Und bin so klug als wie zuvor;\n  Heiße Magister, heiße Doktor gar\n  Und ziehe schon an die zehen Jahr\n  Herauf, herab und quer und krumm\n  Meine Schüler an der Nase herum-\n  Und sehe, daß wir nichts wissen können!\n  Das will mir schier das Herz verbrennen.\n  Zwar bin ich gescheiter als all die Laffen,\n  Doktoren, Magister, Schreiber und Pfaffen;\n  Mich plagen keine Skrupel noch Zweifel,\n  Fürchte mich weder vor Hölle noch Teufel-\n  Dafür ist mir auch alle Freud entrissen,\n  Bilde mir nicht ein, was Rechts zu wissen,\n  Bilde mir nicht ein, ich könnte was lehren,\n  Die Menschen zu bessern und zu bekehren.\n  Auch hab ich weder Gut noch Geld,\n  Noch Ehr und Herrlichkeit der Welt;\n  Es möchte kein Hund so länger leben!\n  Drum hab ich mich der Magie ergeben,\n  Ob mir durch Geistes Kraft und Mund\n  Nicht manch Geheimnis würde kund;\n  Daß ich nicht mehr mit saurem Schweiß\n  Zu sagen brauche, was ich nicht weiß;\n  Daß ich erkenne, was die Welt\n  Im Innersten zusammenhält,\n  Schau alle Wirkenskraft und Samen,\n  Und tu nicht mehr in Worten kramen.\n  "}$
     "\nFAUST:\n  Habe nun, ach!  Philosophie,\n  Juristerei und Medizin,\n  Und leider auch Theologie\n  Durchaus studiert, mit heißem Bemühn.\n  Da steh ich nun, ich armer Tor!\n  Und bin so klug als wie zuvor;\n  Heiße Magister, heiße Doktor gar\n  Und ziehe schon an die zehen Jahr\n  Herauf, herab und quer und krumm\n  Meine Schüler an der Nase herum-\n  Und sehe, daß wir nichts wissen können!\n  Das will mir schier das Herz verbrennen.\n  Zwar bin ich gescheiter als all die Laffen,\n  Doktoren, Magister, Schreiber und Pfaffen;\n  Mich plagen keine Skrupel noch Zweifel,\n  Fürchte mich weder vor Hölle noch Teufel-\n  Dafür ist mir auch alle Freud entrissen,\n  Bilde mir nicht ein, was Rechts zu wissen,\n  Bilde mir nicht ein, ich könnte was lehren,\n  Die Menschen zu bessern und zu bekehren.\n  Auch hab ich weder Gut noch Geld,\n  Noch Ehr und Herrlichkeit der Welt;\n  Es möchte kein Hund so länger leben!\n  Drum hab ich mich der Magie ergeben,\n  Ob mir durch Geistes Kraft und Mund\n  Nicht manch Geheimnis würde kund;\n  Daß ich nicht mehr mit saurem Schweiß\n  Zu sagen brauche, was ich nicht weiß;\n  Daß ich erkenne, was die Welt\n  Im Innersten zusammenhält,\n  Schau alle Wirkenskraft und Samen,\n  Und tu nicht mehr in Worten kramen.\n  "
 
 %% Cell type:code id: tags:
 
 ``` prob
 REGEX_SEARCH_ALL(txt,"ich")
 ```
 
 %% Output
 
     $\{(1\mapsto\text{"ich"}),(2\mapsto\text{"ich"}),(3\mapsto\text{"ich"}),(4\mapsto\text{"ich"}),(5\mapsto\text{"ich"}),(6\mapsto\text{"ich"}),(7\mapsto\text{"ich"}),(8\mapsto\text{"ich"}),(9\mapsto\text{"ich"}),(10\mapsto\text{"ich"}),(11\mapsto\text{"ich"}),(12\mapsto\text{"ich"}),(13\mapsto\text{"ich"}),(14\mapsto\text{"ich"}),(15\mapsto\text{"ich"}),(16\mapsto\text{"ich"}),(17\mapsto\text{"ich"}),(18\mapsto\text{"ich"}),(19\mapsto\text{"ich"}),(20\mapsto\text{"ich"})\}$
     {(1↦"ich"),(2↦"ich"),(3↦"ich"),(4↦"ich"),(5↦"ich"),(6↦"ich"),(7↦"ich"),(8↦"ich"),(9↦"ich"),(10↦"ich"),(11↦"ich"),(12↦"ich"),(13↦"ich"),(14↦"ich"),(15↦"ich"),(16↦"ich"),(17↦"ich"),(18↦"ich"),(19↦"ich"),(20↦"ich")}
 
 %% Cell type:code id: tags:
 
 ``` prob
 REGEX_SEARCH(txt,1,"G[a-z]*")
 ```
 
 %% Output
 
     $\renewcommand{\emptyset}{\mathord\varnothing}\mathit{rec}(\mathit{length}\in 3,\mathit{position}\in 802,\mathit{string}\in\text{"Gut"},\mathit{submatches}\in\emptyset)$
     rec(length∈3,position∈802,string∈"Gut",submatches∈∅)
 
 %% Cell type:code id: tags:
 
 ``` prob
 REGEX_SEARCH_ALL(txt,"G[a-z]*")
 ```
 
 %% Output
 
     $\{(1\mapsto\text{"Gut"}),(2\mapsto\text{"Geld"}),(3\mapsto\text{"Geistes"}),(4\mapsto\text{"Geheimnis"})\}$
     {(1↦"Gut"),(2↦"Geld"),(3↦"Geistes"),(4↦"Geheimnis")}
 
 %% Cell type:code id: tags:
 
 ``` prob
 REGEX_SEARCH_ALL(txt,"der ([A-Z][a-z]*)")
 ```
 
 %% Output
 
     $\{(1\mapsto\text{"der Nase"}),(2\mapsto\text{"der Gut"}),(3\mapsto\text{"der Welt"}),(4\mapsto\text{"der Magie"})\}$
     {(1↦"der Nase"),(2↦"der Gut"),(3↦"der Welt"),(4↦"der Magie")}
 
 %% Cell type:markdown id: tags:
 
 Kleine Anmerkung: mit Klammern kann man oft Gruppen bilden und herausfinden welches Teilwort von einer Gruppe generiert wurde.
 
 %% Cell type:code id: tags:
 
 ``` prob
 REGEX_SEARCH(txt,1,"der ([A-Z][a-z]*)")
 ```
 
 %% Output
 
     $\mathit{rec}(\mathit{length}\in 8,\mathit{position}\in 326,\mathit{string}\in\text{"der Nase"},\mathit{submatches}\in\{(1\mapsto\text{"Nase"})\})$
     rec(length∈8,position∈326,string∈"der Nase",submatches∈{(1↦"Nase")})
 
 %% Cell type:markdown id: tags:
 
 Zusätzlich zu * und + gibt es ein Reihe weiter Wiederholungsoperatoren:
 * ```R?``` 0 oder 1 Wiederholung von R
 * ```R{n}``` $n$ Wiederholungen von R
 * ```R{n,}``` $n$ oder mehr Wiederholungen von R
 * ```R{m,n}``` $m$ bis $n$ Wiederholungen von R
 
 %% Cell type:code id: tags:
 
 ``` prob
 REGEX_SEARCH_ALL(txt,"G[a-z]{3}")
 ```
 
 %% Output
 
     $\{(1\mapsto\text{"Geld"}),(2\mapsto\text{"Geis"}),(3\mapsto\text{"Gehe"})\}$
     {(1↦"Geld"),(2↦"Geis"),(3↦"Gehe")}
 
 %% Cell type:code id: tags:
 
 ``` prob
 REGEX_SEARCH_ALL(txt,"G[a-z]{3,}")
 ```
 
 %% Output
 
     $\{(1\mapsto\text{"Geld"}),(2\mapsto\text{"Geistes"}),(3\mapsto\text{"Geheimnis"})\}$
     {(1↦"Geld"),(2↦"Geistes"),(3↦"Geheimnis")}
 
 %% Cell type:code id: tags:
 
 ``` prob
 REGEX_SEARCH_ALL(txt,"G[a-z]{2,3}")
 ```
 
 %% Output
 
     $\{(1\mapsto\text{"Gut"}),(2\mapsto\text{"Geld"}),(3\mapsto\text{"Geis"}),(4\mapsto\text{"Gehe"})\}$
     {(1↦"Gut"),(2↦"Geld"),(3↦"Geis"),(4↦"Gehe")}
 
 %% Cell type:markdown id: tags:
 
 Es gibt natürlich in der Praxis noch eine Reihe an Sonderzeichen die man erkennen will.
 Man kann deshalb alle Symbole der Syntax der regulären Ausdruckssprache mit ```\``` escapen. So zum Beispiel, ```a\|b``` oder ```a\+```:
 
 %% Cell type:code id: tags:
 
 ``` prob
 REGEX_SEARCH("abca|bd",1,"a|b")
 ```
 
 %% Output
 
     $\renewcommand{\emptyset}{\mathord\varnothing}\mathit{rec}(\mathit{length}\in 1,\mathit{position}\in 1,\mathit{string}\in\text{"a"},\mathit{submatches}\in\emptyset)$
     rec(length∈1,position∈1,string∈"a",submatches∈∅)
 
 %% Cell type:code id: tags:
 
 ``` prob
 REGEX_SEARCH("abca|bd",1,"a\|b")
 ```
 
 %% Output
 
     $\renewcommand{\emptyset}{\mathord\varnothing}\mathit{rec}(\mathit{length}\in 3,\mathit{position}\in 4,\mathit{string}\in\text{"a|b"},\mathit{submatches}\in\emptyset)$
     rec(length∈3,position∈4,string∈"a|b",submatches∈∅)
 
 %% Cell type:code id: tags:
 
 ``` prob
 REGEX_SEARCH("abca+bd",1,"a+")
 ```
 
 %% Output
 
     $\renewcommand{\emptyset}{\mathord\varnothing}\mathit{rec}(\mathit{length}\in 1,\mathit{position}\in 1,\mathit{string}\in\text{"a"},\mathit{submatches}\in\emptyset)$
     rec(length∈1,position∈1,string∈"a",submatches∈∅)
 
 %% Cell type:code id: tags:
 
 ``` prob
 REGEX_SEARCH("abca+bd",1,"a\+")
 ```
 
 %% Output
 
     $\renewcommand{\emptyset}{\mathord\varnothing}\mathit{rec}(\mathit{length}\in 2,\mathit{position}\in 4,\mathit{string}\in\text{"a+"},\mathit{submatches}\in\emptyset)$
     rec(length∈2,position∈4,string∈"a+",submatches∈∅)
 
 %% Cell type:markdown id: tags:
 
 Es gibt auch verschiedene besondere Zeichen:
 * ```\d``` für eine Ziffer
 * ```\D``` für ein Zeichen, dass keine Ziffer ist
 * ```\s``` für ein Leerzeichen
 * ```\S``` für ein Zeichen, dass kein Leerzeichen ist
 * ```\w``` für ein alpha-numerisches Zeichen oder den Underscore
 * ```\W``` für ein Zeichen, dass kein alpha-numerisches Zeichen und kein Underscore ist
 * ```.```  für alle Zeichen ausser Zeilenumbrüchen
 * ```\n``` für einen Zeilenumbruch
 * ```\t``` für ein Tabulatorzeichen
 
 %% Cell type:code id: tags:
 
 ``` prob
 REGEX_SEARCH_ALL("ab cd ef","\w+")
 ```
 
 %% Output
 
     $\{(1\mapsto\text{"ab"}),(2\mapsto\text{"cd"}),(3\mapsto\text{"ef"})\}$
     {(1↦"ab"),(2↦"cd"),(3↦"ef")}
 
 %% Cell type:code id: tags:
 
 ``` prob
 REGEX_SEARCH_ALL(txt,"\w+")
 ```
 
 %% Output
 
     $\{(1\mapsto\text{"FAUST"}),(2\mapsto\text{"Habe"}),(3\mapsto\text{"nun"}),(4\mapsto\text{"ach"}),(5\mapsto\text{"Philosophie"}),(6\mapsto\text{"Juristerei"}),(7\mapsto\text{"und"}),(8\mapsto\text{"Medizin"}),(9\mapsto\text{"Und"}),(10\mapsto\text{"leider"}),(11\mapsto\text{"auch"}),(12\mapsto\text{"Theologie"}),(13\mapsto\text{"Durchaus"}),(14\mapsto\text{"studiert"}),(15\mapsto\text{"mit"}),(16\mapsto\text{"heißem"}),(17\mapsto\text{"Bemühn"}),(18\mapsto\text{"Da"}),(19\mapsto\text{"steh"}),(20\mapsto\text{"ich"}),(21\mapsto\text{"nun"}),(22\mapsto\text{"ich"}),(23\mapsto\text{"armer"}),(24\mapsto\text{"Tor"}),(25\mapsto\text{"Und"}),(26\mapsto\text{"bin"}),(27\mapsto\text{"so"}),(28\mapsto\text{"klug"}),(29\mapsto\text{"als"}),(30\mapsto\text{"wie"}),(31\mapsto\text{"zuvor"}),(32\mapsto\text{"Heiße"}),(33\mapsto\text{"Magister"}),(34\mapsto\text{"heiße"}),(35\mapsto\text{"Doktor"}),(36\mapsto\text{"gar"}),(37\mapsto\text{"Und"}),(38\mapsto\text{"ziehe"}),(39\mapsto\text{"schon"}),(40\mapsto\text{"an"}),(41\mapsto\text{"die"}),(42\mapsto\text{"zehen"}),(43\mapsto\text{"Jahr"}),(44\mapsto\text{"Herauf"}),(45\mapsto\text{"herab"}),(46\mapsto\text{"und"}),(47\mapsto\text{"quer"}),(48\mapsto\text{"und"}),(49\mapsto\text{"krumm"}),(50\mapsto\text{"Meine"}),(51\mapsto\text{"Schüler"}),(52\mapsto\text{"an"}),(53\mapsto\text{"der"}),(54\mapsto\text{"Nase"}),(55\mapsto\text{"herum"}),(56\mapsto\text{"Und"}),(57\mapsto\text{"sehe"}),(58\mapsto\text{"daß"}),(59\mapsto\text{"wir"}),(60\mapsto\text{"nichts"}),(61\mapsto\text{"wissen"}),(62\mapsto\text{"können"}),(63\mapsto\text{"Das"}),(64\mapsto\text{"will"}),(65\mapsto\text{"mir"}),(66\mapsto\text{"schier"}),(67\mapsto\text{"das"}),(68\mapsto\text{"Herz"}),(69\mapsto\text{"verbrennen"}),(70\mapsto\text{"Zwar"}),(71\mapsto\text{"bin"}),(72\mapsto\text{"ich"}),(73\mapsto\text{"gescheiter"}),(74\mapsto\text{"als"}),(75\mapsto\text{"all"}),(76\mapsto\text{"die"}),(77\mapsto\text{"Laffen"}),(78\mapsto\text{"Doktoren"}),(79\mapsto\text{"Magister"}),(80\mapsto\text{"Schreiber"}),(81\mapsto\text{"und"}),(82\mapsto\text{"Pfaffen"}),(83\mapsto\text{"Mich"}),(84\mapsto\text{"plagen"}),(85\mapsto\text{"keine"}),(86\mapsto\text{"Skrupel"}),(87\mapsto\text{"noch"}),(88\mapsto\text{"Zweifel"}),(89\mapsto\text{"Fürchte"}),(90\mapsto\text{"mich"}),(91\mapsto\text{"weder"}),(92\mapsto\text{"vor"}),(93\mapsto\text{"Hölle"}),(94\mapsto\text{"noch"}),(95\mapsto\text{"Teufel"}),(96\mapsto\text{"Dafür"}),(97\mapsto\text{"ist"}),(98\mapsto\text{"mir"}),(99\mapsto\text{"auch"}),(100\mapsto\text{"alle"}),(101\mapsto\text{"Freud"}),(102\mapsto\text{"entrissen"}),(103\mapsto\text{"Bilde"}),(104\mapsto\text{"mir"}),(105\mapsto\text{"nicht"}),(106\mapsto\text{"ein"}),(107\mapsto\text{"was"}),(108\mapsto\text{"Rechts"}),(109\mapsto\text{"zu"}),(110\mapsto\text{"wissen"}),(111\mapsto\text{"Bilde"}),(112\mapsto\text{"mir"}),(113\mapsto\text{"nicht"}),(114\mapsto\text{"ein"}),(115\mapsto\text{"ich"}),(116\mapsto\text{"könnte"}),(117\mapsto\text{"was"}),(118\mapsto\text{"lehren"}),(119\mapsto\text{"Die"}),(120\mapsto\text{"Menschen"}),(121\mapsto\text{"zu"}),(122\mapsto\text{"bessern"}),(123\mapsto\text{"und"}),(124\mapsto\text{"zu"}),(125\mapsto\text{"bekehren"}),(126\mapsto\text{"Auch"}),(127\mapsto\text{"hab"}),(128\mapsto\text{"ich"}),(129\mapsto\text{"weder"}),(130\mapsto\text{"Gut"}),(131\mapsto\text{"noch"}),(132\mapsto\text{"Geld"}),(133\mapsto\text{"Noch"}),(134\mapsto\text{"Ehr"}),(135\mapsto\text{"und"}),(136\mapsto\text{"Herrlichkeit"}),(137\mapsto\text{"der"}),(138\mapsto\text{"Welt"}),(139\mapsto\text{"Es"}),(140\mapsto\text{"möchte"}),(141\mapsto\text{"kein"}),(142\mapsto\text{"Hund"}),(143\mapsto\text{"so"}),(144\mapsto\text{"länger"}),(145\mapsto\text{"leben"}),(146\mapsto\text{"Drum"}),(147\mapsto\text{"hab"}),(148\mapsto\text{"ich"}),(149\mapsto\text{"mich"}),(150\mapsto\text{"der"}),(151\mapsto\text{"Magie"}),(152\mapsto\text{"ergeben"}),(153\mapsto\text{"Ob"}),(154\mapsto\text{"mir"}),(155\mapsto\text{"durch"}),(156\mapsto\text{"Geistes"}),(157\mapsto\text{"Kraft"}),(158\mapsto\text{"und"}),(159\mapsto\text{"Mund"}),(160\mapsto\text{"Nicht"}),(161\mapsto\text{"manch"}),(162\mapsto\text{"Geheimnis"}),(163\mapsto\text{"würde"}),(164\mapsto\text{"kund"}),(165\mapsto\text{"Daß"}),(166\mapsto\text{"ich"}),(167\mapsto\text{"nicht"}),(168\mapsto\text{"mehr"}),(169\mapsto\text{"mit"}),(170\mapsto\text{"saurem"}),(171\mapsto\text{"Schweiß"}),(172\mapsto\text{"Zu"}),(173\mapsto\text{"sagen"}),(174\mapsto\text{"brauche"}),(175\mapsto\text{"was"}),(176\mapsto\text{"ich"}),(177\mapsto\text{"nicht"}),(178\mapsto\text{"weiß"}),(179\mapsto\text{"Daß"}),(180\mapsto\text{"ich"}),(181\mapsto\text{"erkenne"}),(182\mapsto\text{"was"}),(183\mapsto\text{"die"}),(184\mapsto\text{"Welt"}),(185\mapsto\text{"Im"}),(186\mapsto\text{"Innersten"}),(187\mapsto\text{"zusammenhält"}),(188\mapsto\text{"Schau"}),(189\mapsto\text{"alle"}),(190\mapsto\text{"Wirkenskraft"}),(191\mapsto\text{"und"}),(192\mapsto\text{"Samen"}),(193\mapsto\text{"Und"}),(194\mapsto\text{"tu"}),(195\mapsto\text{"nicht"}),(196\mapsto\text{"mehr"}),(197\mapsto\text{"in"}),(198\mapsto\text{"Worten"}),(199\mapsto\text{"kramen"})\}$
     {(1↦"FAUST"),(2↦"Habe"),(3↦"nun"),(4↦"ach"),(5↦"Philosophie"),(6↦"Juristerei"),(7↦"und"),(8↦"Medizin"),(9↦"Und"),(10↦"leider"),(11↦"auch"),(12↦"Theologie"),(13↦"Durchaus"),(14↦"studiert"),(15↦"mit"),(16↦"heißem"),(17↦"Bemühn"),(18↦"Da"),(19↦"steh"),(20↦"ich"),(21↦"nun"),(22↦"ich"),(23↦"armer"),(24↦"Tor"),(25↦"Und"),(26↦"bin"),(27↦"so"),(28↦"klug"),(29↦"als"),(30↦"wie"),(31↦"zuvor"),(32↦"Heiße"),(33↦"Magister"),(34↦"heiße"),(35↦"Doktor"),(36↦"gar"),(37↦"Und"),(38↦"ziehe"),(39↦"schon"),(40↦"an"),(41↦"die"),(42↦"zehen"),(43↦"Jahr"),(44↦"Herauf"),(45↦"herab"),(46↦"und"),(47↦"quer"),(48↦"und"),(49↦"krumm"),(50↦"Meine"),(51↦"Schüler"),(52↦"an"),(53↦"der"),(54↦"Nase"),(55↦"herum"),(56↦"Und"),(57↦"sehe"),(58↦"daß"),(59↦"wir"),(60↦"nichts"),(61↦"wissen"),(62↦"können"),(63↦"Das"),(64↦"will"),(65↦"mir"),(66↦"schier"),(67↦"das"),(68↦"Herz"),(69↦"verbrennen"),(70↦"Zwar"),(71↦"bin"),(72↦"ich"),(73↦"gescheiter"),(74↦"als"),(75↦"all"),(76↦"die"),(77↦"Laffen"),(78↦"Doktoren"),(79↦"Magister"),(80↦"Schreiber"),(81↦"und"),(82↦"Pfaffen"),(83↦"Mich"),(84↦"plagen"),(85↦"keine"),(86↦"Skrupel"),(87↦"noch"),(88↦"Zweifel"),(89↦"Fürchte"),(90↦"mich"),(91↦"weder"),(92↦"vor"),(93↦"Hölle"),(94↦"noch"),(95↦"Teufel"),(96↦"Dafür"),(97↦"ist"),(98↦"mir"),(99↦"auch"),(100↦"alle"),(101↦"Freud"),(102↦"entrissen"),(103↦"Bilde"),(104↦"mir"),(105↦"nicht"),(106↦"ein"),(107↦"was"),(108↦"Rechts"),(109↦"zu"),(110↦"wissen"),(111↦"Bilde"),(112↦"mir"),(113↦"nicht"),(114↦"ein"),(115↦"ich"),(116↦"könnte"),(117↦"was"),(118↦"lehren"),(119↦"Die"),(120↦"Menschen"),(121↦"zu"),(122↦"bessern"),(123↦"und"),(124↦"zu"),(125↦"bekehren"),(126↦"Auch"),(127↦"hab"),(128↦"ich"),(129↦"weder"),(130↦"Gut"),(131↦"noch"),(132↦"Geld"),(133↦"Noch"),(134↦"Ehr"),(135↦"und"),(136↦"Herrlichkeit"),(137↦"der"),(138↦"Welt"),(139↦"Es"),(140↦"möchte"),(141↦"kein"),(142↦"Hund"),(143↦"so"),(144↦"länger"),(145↦"leben"),(146↦"Drum"),(147↦"hab"),(148↦"ich"),(149↦"mich"),(150↦"der"),(151↦"Magie"),(152↦"ergeben"),(153↦"Ob"),(154↦"mir"),(155↦"durch"),(156↦"Geistes"),(157↦"Kraft"),(158↦"und"),(159↦"Mund"),(160↦"Nicht"),(161↦"manch"),(162↦"Geheimnis"),(163↦"würde"),(164↦"kund"),(165↦"Daß"),(166↦"ich"),(167↦"nicht"),(168↦"mehr"),(169↦"mit"),(170↦"saurem"),(171↦"Schweiß"),(172↦"Zu"),(173↦"sagen"),(174↦"brauche"),(175↦"was"),(176↦"ich"),(177↦"nicht"),(178↦"weiß"),(179↦"Daß"),(180↦"ich"),(181↦"erkenne"),(182↦"was"),(183↦"die"),(184↦"Welt"),(185↦"Im"),(186↦"Innersten"),(187↦"zusammenhält"),(188↦"Schau"),(189↦"alle"),(190↦"Wirkenskraft"),(191↦"und"),(192↦"Samen"),(193↦"Und"),(194↦"tu"),(195↦"nicht"),(196↦"mehr"),(197↦"in"),(198↦"Worten"),(199↦"kramen")}
 
 %% Cell type:code id: tags:
 
 ``` prob
 ran(REGEX_SEARCH_ALL(txt,"\w+"))
 ```
 
 %% Output
 
     $\{\text{"Auch"},\text{"Bemühn"},\text{"Bilde"},\text{"Da"},\text{"Dafür"},\text{"Das"},\text{"Daß"},\text{"Die"},\text{"Doktor"},\text{"Doktoren"},\text{"Drum"},\text{"Durchaus"},\text{"Ehr"},\text{"Es"},\text{"FAUST"},\text{"Freud"},\text{"Fürchte"},\text{"Geheimnis"},\text{"Geistes"},\text{"Geld"},\text{"Gut"},\text{"Habe"},\text{"Heiße"},\text{"Herauf"},\text{"Herrlichkeit"},\text{"Herz"},\text{"Hund"},\text{"Hölle"},\text{"Im"},\text{"Innersten"},\text{"Jahr"},\text{"Juristerei"},\text{"Kraft"},\text{"Laffen"},\text{"Magie"},\text{"Magister"},\text{"Medizin"},\text{"Meine"},\text{"Menschen"},\text{"Mich"},\text{"Mund"},\text{"Nase"},\text{"Nicht"},\text{"Noch"},\text{"Ob"},\text{"Pfaffen"},\text{"Philosophie"},\text{"Rechts"},\text{"Samen"},\text{"Schau"},\text{"Schreiber"},\text{"Schweiß"},\text{"Schüler"},\text{"Skrupel"},\text{"Teufel"},\text{"Theologie"},\text{"Tor"},\text{"Und"},\text{"Welt"},\text{"Wirkenskraft"},\text{"Worten"},\text{"Zu"},\text{"Zwar"},\text{"Zweifel"},\text{"ach"},\text{"all"},\text{"alle"},\text{"als"},\text{"an"},\text{"armer"},\text{"auch"},\text{"bekehren"},\text{"bessern"},\text{"bin"},\text{"brauche"},\text{"das"},\text{"daß"},\text{"der"},\text{"die"},\text{"durch"},\text{"ein"},\text{"entrissen"},\text{"ergeben"},\text{"erkenne"},\text{"gar"},\text{"gescheiter"},\text{"hab"},\text{"heiße"},\text{"heißem"},\text{"herab"},\text{"herum"},\text{"ich"},\text{"in"},\text{"ist"},\text{"kein"},\text{"keine"},\text{"klug"},\text{"kramen"},\text{"krumm"},\text{"kund"},\text{"können"},\text{"könnte"},\text{"leben"},\text{"lehren"},\text{"leider"},\text{"länger"},\text{"manch"},\text{"mehr"},\text{"mich"},\text{"mir"},\text{"mit"},\text{"möchte"},\text{"nicht"},\text{"nichts"},\text{"noch"},\text{"nun"},\text{"plagen"},\text{"quer"},\text{"sagen"},\text{"saurem"},\text{"schier"},\text{"schon"},\text{"sehe"},\text{"so"},\text{"steh"},\text{"studiert"},\text{"tu"},\text{"und"},\text{"verbrennen"},\text{"vor"},\text{"was"},\text{"weder"},\text{"weiß"},\text{"wie"},\text{"will"},\text{"wir"},\text{"wissen"},\text{"würde"},\text{"zehen"},\text{"ziehe"},\text{"zu"},\text{"zusammenhält"},\text{"zuvor"}\}$
     {"Auch","Bemühn","Bilde","Da","Dafür","Das","Daß","Die","Doktor","Doktoren","Drum","Durchaus","Ehr","Es","FAUST","Freud","Fürchte","Geheimnis","Geistes","Geld","Gut","Habe","Heiße","Herauf","Herrlichkeit","Herz","Hund","Hölle","Im","Innersten","Jahr","Juristerei","Kraft","Laffen","Magie","Magister","Medizin","Meine","Menschen","Mich","Mund","Nase","Nicht","Noch","Ob","Pfaffen","Philosophie","Rechts","Samen","Schau","Schreiber","Schweiß","Schüler","Skrupel","Teufel","Theologie","Tor","Und","Welt","Wirkenskraft","Worten","Zu","Zwar","Zweifel","ach","all","alle","als","an","armer","auch","bekehren","bessern","bin","brauche","das","daß","der","die","durch","ein","entrissen","ergeben","erkenne","gar","gescheiter","hab","heiße","heißem","herab","herum","ich","in","ist","kein","keine","klug","kramen","krumm","kund","können","könnte","leben","lehren","leider","länger","manch","mehr","mich","mir","mit","möchte","nicht","nichts","noch","nun","plagen","quer","sagen","saurem","schier","schon","sehe","so","steh","studiert","tu","und","verbrennen","vor","was","weder","weiß","wie","will","wir","wissen","würde","zehen","ziehe","zu","zusammenhält","zuvor"}
 
 %% Cell type:code id: tags:
 
 ``` prob
 REGEX_SEARCH_ALL(txt,"\n\w+")
 ```
 
 %% Output
 
     $\{(1\mapsto\text{"\nFAUST"})\}$
     {(1↦"\nFAUST")}
 
 %% Cell type:code id: tags:
 
 ``` prob
 REGEX_SEARCH_ALL(txt,"\n\s*\w+")
 ```
 
 %% Output
 
     $\{(1\mapsto\text{"\nFAUST"}),(2\mapsto\text{"\n  Habe"}),(3\mapsto\text{"\n  Juristerei"}),(4\mapsto\text{"\n  Und"}),(5\mapsto\text{"\n  Durchaus"}),(6\mapsto\text{"\n  Da"}),(7\mapsto\text{"\n  Und"}),(8\mapsto\text{"\n  Heiße"}),(9\mapsto\text{"\n  Und"}),(10\mapsto\text{"\n  Herauf"}),(11\mapsto\text{"\n  Meine"}),(12\mapsto\text{"\n  Und"}),(13\mapsto\text{"\n  Das"}),(14\mapsto\text{"\n  Zwar"}),(15\mapsto\text{"\n  Doktoren"}),(16\mapsto\text{"\n  Mich"}),(17\mapsto\text{"\n  Fürchte"}),(18\mapsto\text{"\n  Dafür"}),(19\mapsto\text{"\n  Bilde"}),(20\mapsto\text{"\n  Bilde"}),(21\mapsto\text{"\n  Die"}),(22\mapsto\text{"\n  Auch"}),(23\mapsto\text{"\n  Noch"}),(24\mapsto\text{"\n  Es"}),(25\mapsto\text{"\n  Drum"}),(26\mapsto\text{"\n  Ob"}),(27\mapsto\text{"\n  Nicht"}),(28\mapsto\text{"\n  Daß"}),(29\mapsto\text{"\n  Zu"}),(30\mapsto\text{"\n  Daß"}),(31\mapsto\text{"\n  Im"}),(32\mapsto\text{"\n  Schau"}),(33\mapsto\text{"\n  Und"})\}$
     {(1↦"\nFAUST"),(2↦"\n  Habe"),(3↦"\n  Juristerei"),(4↦"\n  Und"),(5↦"\n  Durchaus"),(6↦"\n  Da"),(7↦"\n  Und"),(8↦"\n  Heiße"),(9↦"\n  Und"),(10↦"\n  Herauf"),(11↦"\n  Meine"),(12↦"\n  Und"),(13↦"\n  Das"),(14↦"\n  Zwar"),(15↦"\n  Doktoren"),(16↦"\n  Mich"),(17↦"\n  Fürchte"),(18↦"\n  Dafür"),(19↦"\n  Bilde"),(20↦"\n  Bilde"),(21↦"\n  Die"),(22↦"\n  Auch"),(23↦"\n  Noch"),(24↦"\n  Es"),(25↦"\n  Drum"),(26↦"\n  Ob"),(27↦"\n  Nicht"),(28↦"\n  Daß"),(29↦"\n  Zu"),(30↦"\n  Daß"),(31↦"\n  Im"),(32↦"\n  Schau"),(33↦"\n  Und")}
 
 %% Cell type:code id: tags:
 
 ``` prob
 :let jt '''
 public class HelloWorld {
     public static void main(String[] args) {
         System.out.println("Hello, World");
         int res1 = 22*33;
         System.out.println(res);
     }
 }
 '''
 ```
 
 %% Output
 
     $\text{" \npublic class HelloWorld {\n    public static void main(String[] args) {\n        System.out.println(\"Hello, World\");\n        int res1 = 22*33;\n        System.out.println(res);\n    }\n}\n"}$
     " \npublic class HelloWorld {\n    public static void main(String[] args) {\n        System.out.println(\"Hello, World\");\n        int res1 = 22*33;\n        System.out.println(res);\n    }\n}\n"
 
 %% Cell type:code id: tags:
 
 ``` prob
 :let Bezeichner "\b[A-Za-z_][A-Za-z0-9_]*"
 ```
 
 %% Output
 
     $\text{"\b[A-Za-z_][A-Za-z0-9_]*"}$
     "\b[A-Za-z_][A-Za-z0-9_]*"
 
 %% Cell type:code id: tags:
 
 ``` prob
 :let Zahl "\b[0-9]+"
 ```
 
 %% Output
 
     $\text{"\b[0-9]+"}$
     "\b[0-9]+"
 
 %% Cell type:code id: tags:
 
 ``` prob
 REGEX_SEARCH_ALL(jt,Bezeichner)
 ```
 
 %% Output
 
     $\{(1\mapsto\text{"public"}),(2\mapsto\text{"class"}),(3\mapsto\text{"HelloWorld"}),(4\mapsto\text{"public"}),(5\mapsto\text{"static"}),(6\mapsto\text{"void"}),(7\mapsto\text{"main"}),(8\mapsto\text{"String"}),(9\mapsto\text{"args"}),(10\mapsto\text{"System"}),(11\mapsto\text{"out"}),(12\mapsto\text{"println"}),(13\mapsto\text{"Hello"}),(14\mapsto\text{"World"}),(15\mapsto\text{"int"}),(16\mapsto\text{"res1"}),(17\mapsto\text{"System"}),(18\mapsto\text{"out"}),(19\mapsto\text{"println"}),(20\mapsto\text{"res"})\}$
     {(1↦"public"),(2↦"class"),(3↦"HelloWorld"),(4↦"public"),(5↦"static"),(6↦"void"),(7↦"main"),(8↦"String"),(9↦"args"),(10↦"System"),(11↦"out"),(12↦"println"),(13↦"Hello"),(14↦"World"),(15↦"int"),(16↦"res1"),(17↦"System"),(18↦"out"),(19↦"println"),(20↦"res")}
 
 %% Cell type:code id: tags:
 
 ``` prob
 REGEX_SEARCH_ALL(jt,Zahl)
 ```
 
 %% Output
 
     $\{(1\mapsto\text{"22"}),(2\mapsto\text{"33"})\}$
     {(1↦"22"),(2↦"33")}
 
 %% Cell type:code id: tags:
 
 ``` prob
 :let ComposedID "\b([A-Za-z_][A-Za-z0-9_]*)(\.([A-Za-z_][A-Za-z0-9_]*))+"
 ```
 
 %% Output
 
     $\text{"\b([A-Za-z_][A-Za-z0-9_]*)(\.([A-Za-z_][A-Za-z0-9_]*))+"}$
     "\b([A-Za-z_][A-Za-z0-9_]*)(\.([A-Za-z_][A-Za-z0-9_]*))+"
 
 %% Cell type:code id: tags:
 
 ``` prob
 REGEX_SEARCH_ALL(jt,ComposedID)
 ```
 
 %% Output
 
     $\{(1\mapsto\text{"System.out.println"}),(2\mapsto\text{"System.out.println"})\}$
     {(1↦"System.out.println"),(2↦"System.out.println")}
 
 %% Cell type:markdown id: tags:
 
 ## Zusammenfassung
 
 Reguläre Ausdrücke können sehr nützlich sein.
 Sie sind sehr mächtig, aber wir werden sehen, dass sie auch Grenzen haben.
 
 Sie finden Verwendung
  * im Compilerbau (Tokenklassen zu definieren)
  * in Editoren und IDEs
   - Syntaxhighlighting, fortgeschrittene Suche (und Ersetzen)
  * auf der Kommandozeile (grep) und in Programmen
   - Verarbeiten von Log-Dateien, Einlesen oder Validierung von Daten, ...
 
 Es gibt viele Bibliotheken und Bücher über reguläre Ausdrücke, zum Beispiel:
 
 ![Oreilly](https://covers.oreillystatic.com/images/9780596528126/lrg.jpg)
 
 Es gibt auch diesen berühmten Comic von xkcd:
 
 ![Xkcd](https://imgs.xkcd.com/comics/regular_expressions.png)
 
 %% Cell type:code id: tags:
 
 ``` prob
 ```

info4/kapitel-3/CYK_Algorithmus.ipynb

 %% Cell type:markdown id: tags:
 
 # CYK Algorithmus
 
 %% Cell type:code id: tags:
 
 ``` prob
 ::load
 MACHINE CYK
 /* An encoding of the CYK Algorithm in B */
 SETS
  ΣN = {a,b,   S,A,B,C}
 DEFINITIONS
   ANIMATION_FUNCTION_DEFAULT == {r,c,i| r=-1 ∧ c↦i ∈ x};
   ANIMATION_FUNCTION == {r,c,i | c↦r ∈ dom(T) ∧ i=(T(c,r))}
 CONSTANTS Σ, N, P, x, n
 PROPERTIES
  Σ = {a,b} ∧ // Terminalsymbole
  Σ ∩ N = ∅ ∧
  Σ ∪ N = ΣN ∧
  /* eine kfG in Chomsky Normalform, Example 6.7 aus Hopcroft/Ullman */
  P = { // die Regeln
                   [S] ↦ [A,B], [S] ↦ [B,C],
                   [A] ↦ [B,A], [A] ↦ [a],
                   [B] ↦ [C,C], [B] ↦ [b],
                   [C] ↦ [A,B], [C] ↦ [a]
      } ∧
 x ∈ seq(ΣN) ∧ n = size(x) ∧
 x = [b,a,a,b,a]
 VARIABLES T, i,j
 INVARIANT T ∈ ((1..n)*(0..n)) ⇸ ℙ(N) ∧ j∈1..n ∧ i∈1..n-1
 INITIALISATION
   T := λ(i,j).(i∈1..n ∧ j=0 | {A| A∈N ∧ [A] ↦ [x(i)] ∈ P})
   // for(i =1,2,...,n){T(i,0)={A∈N | 􏰁􏰁A→x(i) ist Regel in P}; }
   ||
   j := 1
   ||
   i := 1
 OPERATIONS
   For_k_loop(ii,jj,Tij) = // führt eine Iteration der for(k=0,1,...j-1) Schleife aus
     PRE j<n ∧ ii=i ∧ jj=j ∧
         Tij = { A | A∈N ∧
                 ∃(B,C,k).( [A] ↦ [B,C] ∈ P ∧
                            k∈0..j-1 ∧
                            B∈T(i,k) ∧
                            C∈T(i+k+1,j-k-1)) }  THEN
     T(i,j) := Tij ||
     IF i<n-j THEN
        i := i+1
     ELSE
        i := 1 || j := j+1
     END
   END;
   r <-- Accept = PRE j=n THEN r := bool(S∈ T(1,n-1)) END
 END
 
 
 
 ```
 
 %% Output
 
     Loaded machine: CYK
 
 %% Cell type:code id: tags:
 
 ``` prob
 :constants
 ```
 
 %% Output
 
-    Machine constants set up using operation 0: $setup_constants()
+    Executed operation: SETUP_CONSTANTS()
 
 %% Cell type:code id: tags:
 
 ``` prob
 :init
 ```
 
 %% Output
 
-    Machine initialised using operation 1: $initialise_machine()
+    Executed operation: INITIALISATION()
+
+%% Cell type:code id: tags:
+
+``` prob
+:pref PP_SEQUENCES=TRUE
+```
+
+%% Output
+
+    Preference changed: PP_SEQUENCES = TRUE
 
 %% Cell type:markdown id: tags:
 
 Wir lassen den Algorithmus für folgendes Wort $x$ laufen (und wollen prüfen ob die Grammatik das Wort generieren kann):
 
 %% Cell type:code id: tags:
 
 ``` prob
 x
 ```
 
 %% Output
 
-    $\{(1\mapsto \mathit{b}),(2\mapsto \mathit{a}),(3\mapsto \mathit{a}),(4\mapsto \mathit{b}),(5\mapsto \mathit{a})\}$
-    {(1↦b),(2↦a),(3↦a),(4↦b),(5↦a)}
+    $[\mathit{b},\mathit{a},\mathit{a},\mathit{b},\mathit{a}]$
+    [b,a,a,b,a]
 
 %% Cell type:markdown id: tags:
 
 Am Anfang werden die Werte für T(i,0) in der INITIALISATION der Maschine berechnet:
 * for(i =1,2,...,n){T(i,0)={A∈N | A→x(i) ist Regel in P};}
 
 %% Cell type:code id: tags:
 
 ``` prob
 :show
 ```
 
 %% Output
 
     <table style="font-family:monospace"><tbody>
     <tr>
     <td style="padding:10px">b</td>
     <td style="padding:10px">a</td>
     <td style="padding:10px">a</td>
     <td style="padding:10px">b</td>
     <td style="padding:10px">a</td>
     </tr>
     <tr>
     <td style="padding:10px">{B}</td>
     <td style="padding:10px">{A,C}</td>
     <td style="padding:10px">{A,C}</td>
     <td style="padding:10px">{B}</td>
     <td style="padding:10px">{A,C}</td>
     </tr>
     </tbody></table>
     <Animation function visualisation>
 
 %% Cell type:code id: tags:
 
 ``` prob
 N
 ```
 
 %% Output
 
     $\{\mathit{S},\mathit{A},\mathit{B},\mathit{C}\}$
     {S,A,B,C}
 
 %% Cell type:code id: tags:
 
 ``` prob
 P
 ```
 
 %% Output
 
-    $\{(\{(1\mapsto \mathit{S})\}\mapsto\{(1\mapsto \mathit{A}),(2\mapsto \mathit{B})\}),(\{(1\mapsto \mathit{S})\}\mapsto\{(1\mapsto \mathit{B}),(2\mapsto \mathit{C})\}),(\{(1\mapsto \mathit{A})\}\mapsto\{(1\mapsto \mathit{a})\}),(\{(1\mapsto \mathit{A})\}\mapsto\{(1\mapsto \mathit{B}),(2\mapsto \mathit{A})\}),(\{(1\mapsto \mathit{B})\}\mapsto\{(1\mapsto \mathit{b})\}),(\{(1\mapsto \mathit{B})\}\mapsto\{(1\mapsto \mathit{C}),(2\mapsto \mathit{C})\}),(\{(1\mapsto \mathit{C})\}\mapsto\{(1\mapsto \mathit{a})\}),(\{(1\mapsto \mathit{C})\}\mapsto\{(1\mapsto \mathit{A}),(2\mapsto \mathit{B})\})\}$
-    {({(1↦S)}↦{(1↦A),(2↦B)}),({(1↦S)}↦{(1↦B),(2↦C)}),({(1↦A)}↦{(1↦a)}),({(1↦A)}↦{(1↦B),(2↦A)}),({(1↦B)}↦{(1↦b)}),({(1↦B)}↦{(1↦C),(2↦C)}),({(1↦C)}↦{(1↦a)}),({(1↦C)}↦{(1↦A),(2↦B)})}
+    $\{([\mathit{S}]\mapsto[\mathit{A},\mathit{B}]),([\mathit{S}]\mapsto[\mathit{B},\mathit{C}]),([\mathit{A}]\mapsto[\mathit{a}]),([\mathit{A}]\mapsto[\mathit{B},\mathit{A}]),([\mathit{B}]\mapsto[\mathit{b}]),([\mathit{B}]\mapsto[\mathit{C},\mathit{C}]),([\mathit{C}]\mapsto[\mathit{a}]),([\mathit{C}]\mapsto[\mathit{A},\mathit{B}])\}$
+    {([S]↦[A,B]),([S]↦[B,C]),([A]↦[a]),([A]↦[B,A]),([B]↦[b]),([B]↦[C,C]),([C]↦[a]),([C]↦[A,B])}
 
 %% Cell type:code id: tags:
 
 ``` prob
 (i,j)
 ```
 
 %% Output
 
     $(1\mapsto 1)$
     (1↦1)
 
 %% Cell type:code id: tags:
 
 ``` prob
 :exec For_k_loop
 ```
 
 %% Output
 
     Executed operation: For_k_loop(1,1,{S,A})
 
 %% Cell type:code id: tags:
 
 ``` prob
 (i,j)
 ```
 
 %% Output
 
     $(2\mapsto 1)$
     (2↦1)
 
 %% Cell type:code id: tags:
 
 ``` prob
 :show
 ```
 
 %% Output
 
     <table style="font-family:monospace"><tbody>
     <tr>
     <td style="padding:10px">b</td>
     <td style="padding:10px">a</td>
     <td style="padding:10px">a</td>
     <td style="padding:10px">b</td>
     <td style="padding:10px">a</td>
     </tr>
     <tr>
     <td style="padding:10px">{B}</td>
     <td style="padding:10px">{A,C}</td>
     <td style="padding:10px">{A,C}</td>
     <td style="padding:10px">{B}</td>
     <td style="padding:10px">{A,C}</td>
     </tr>
     <tr>
     <td style="padding:10px">{S,A}</td>
     <td style="padding:0px"></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
 :exec For_k_loop
 ```
 
 %% Output
 
     Executed operation: For_k_loop(2,1,{B})
 
 %% Cell type:code id: tags:
 
 ``` prob
 (i,j)
 ```
 
 %% Output
 
     $(3\mapsto 1)$
     (3↦1)
 
 %% Cell type:code id: tags:
 
 ``` prob
 :show
 ```
 
 %% Output
 
     <table style="font-family:monospace"><tbody>
     <tr>
     <td style="padding:10px">b</td>
     <td style="padding:10px">a</td>
     <td style="padding:10px">a</td>
     <td style="padding:10px">b</td>
     <td style="padding:10px">a</td>
     </tr>
     <tr>
     <td style="padding:10px">{B}</td>
     <td style="padding:10px">{A,C}</td>
     <td style="padding:10px">{A,C}</td>
     <td style="padding:10px">{B}</td>
     <td style="padding:10px">{A,C}</td>
     </tr>
     <tr>
     <td style="padding:10px">{S,A}</td>
     <td style="padding:10px">{B}</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
 T
 ```
 
 %% Output
 
     $\{(1\mapsto 0\mapsto\{\mathit{B}\}),(1\mapsto 1\mapsto\{\mathit{S},\mathit{A}\}),(2\mapsto 0\mapsto\{\mathit{A},\mathit{C}\}),(2\mapsto 1\mapsto\{\mathit{B}\}),(3\mapsto 0\mapsto\{\mathit{A},\mathit{C}\}),(4\mapsto 0\mapsto\{\mathit{B}\}),(5\mapsto 0\mapsto\{\mathit{A},\mathit{C}\})\}$
     {(1↦0↦{B}),(1↦1↦{S,A}),(2↦0↦{A,C}),(2↦1↦{B}),(3↦0↦{A,C}),(4↦0↦{B}),(5↦0↦{A,C})}
 
 %% Cell type:code id: tags:
 
 ``` prob
 :exec For_k_loop
 ```
 
 %% Output
 
     Executed operation: For_k_loop(3,1,{S,C})
 
 %% Cell type:code id: tags:
 
 ``` prob
 :exec For_k_loop
 ```
 
 %% Output
 
     Executed operation: For_k_loop(4,1,{S,A})
 
 %% Cell type:code id: tags:
 
 ``` prob
 :show
 ```
 
 %% Output
 
     <table style="font-family:monospace"><tbody>
     <tr>
     <td style="padding:10px">b</td>
     <td style="padding:10px">a</td>
     <td style="padding:10px">a</td>
     <td style="padding:10px">b</td>
     <td style="padding:10px">a</td>
     </tr>
     <tr>
     <td style="padding:10px">{B}</td>
     <td style="padding:10px">{A,C}</td>
     <td style="padding:10px">{A,C}</td>
     <td style="padding:10px">{B}</td>
     <td style="padding:10px">{A,C}</td>
     </tr>
     <tr>
     <td style="padding:10px">{S,A}</td>
     <td style="padding:10px">{B}</td>
     <td style="padding:10px">{S,C}</td>
     <td style="padding:10px">{S,A}</td>
     <td style="padding:0px"></td>
     </tr>
     </tbody></table>
     <Animation function visualisation>
 
 %% Cell type:code id: tags:
 
 ``` prob
 :exec For_k_loop
 ```
 
 %% Output
 
-    Executed operation: For_k_loop(1,2,{})
+    Executed operation: For_k_loop(1,2,[])
 
 %% Cell type:code id: tags:
 
 ``` prob
 (i,j)
 ```
 
 %% Output
 
     $(2\mapsto 2)$
     (2↦2)
 
 %% Cell type:code id: tags:
 
 ``` prob
 :show
 ```
 
 %% Output
 
     <table style="font-family:monospace"><tbody>
     <tr>
     <td style="padding:10px">b</td>
     <td style="padding:10px">a</td>
     <td style="padding:10px">a</td>
     <td style="padding:10px">b</td>
     <td style="padding:10px">a</td>
     </tr>
     <tr>
     <td style="padding:10px">{B}</td>
     <td style="padding:10px">{A,C}</td>
     <td style="padding:10px">{A,C}</td>
     <td style="padding:10px">{B}</td>
     <td style="padding:10px">{A,C}</td>
     </tr>
     <tr>
     <td style="padding:10px">{S,A}</td>
     <td style="padding:10px">{B}</td>
     <td style="padding:10px">{S,C}</td>
     <td style="padding:10px">{S,A}</td>
     <td style="padding:0px"></td>
     </tr>
     <tr>
-    <td style="padding:10px">{}</td>
+    <td style="padding:10px">[]</td>
     <td style="padding:0px"></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
 :exec For_k_loop
 ```
 
 %% Output
 
     Executed operation: For_k_loop(2,2,{B})
 
 %% Cell type:code id: tags:
 
 ``` prob
 :exec For_k_loop
 ```
 
 %% Output
 
     Executed operation: For_k_loop(3,2,{B})
 
 %% Cell type:code id: tags:
 
 ``` prob
 :show
 ```
 
 %% Output
 
     <table style="font-family:monospace"><tbody>
     <tr>
     <td style="padding:10px">b</td>
     <td style="padding:10px">a</td>
     <td style="padding:10px">a</td>
     <td style="padding:10px">b</td>
     <td style="padding:10px">a</td>
     </tr>
     <tr>
     <td style="padding:10px">{B}</td>
     <td style="padding:10px">{A,C}</td>
     <td style="padding:10px">{A,C}</td>
     <td style="padding:10px">{B}</td>
     <td style="padding:10px">{A,C}</td>
     </tr>
     <tr>
     <td style="padding:10px">{S,A}</td>
     <td style="padding:10px">{B}</td>
     <td style="padding:10px">{S,C}</td>
     <td style="padding:10px">{S,A}</td>
     <td style="padding:0px"></td>
     </tr>
     <tr>
-    <td style="padding:10px">{}</td>
+    <td style="padding:10px">[]</td>
     <td style="padding:10px">{B}</td>
     <td style="padding:10px">{B}</td>
     <td style="padding:0px"></td>
     <td style="padding:0px"></td>
     </tr>
     </tbody></table>
     <Animation function visualisation>
 
 %% Cell type:code id: tags:
 
 ``` prob
 :exec For_k_loop
 ```
 
 %% Output
 
-    Executed operation: For_k_loop(1,3,{})
+    Executed operation: For_k_loop(1,3,[])
 
 %% Cell type:code id: tags:
 
 ``` prob
 :show
 ```
 
 %% Output
 
     <table style="font-family:monospace"><tbody>
     <tr>
     <td style="padding:10px">b</td>
     <td style="padding:10px">a</td>
     <td style="padding:10px">a</td>
     <td style="padding:10px">b</td>
     <td style="padding:10px">a</td>
     </tr>
     <tr>
     <td style="padding:10px">{B}</td>
     <td style="padding:10px">{A,C}</td>
     <td style="padding:10px">{A,C}</td>
     <td style="padding:10px">{B}</td>
     <td style="padding:10px">{A,C}</td>
     </tr>
     <tr>
     <td style="padding:10px">{S,A}</td>
     <td style="padding:10px">{B}</td>
     <td style="padding:10px">{S,C}</td>
     <td style="padding:10px">{S,A}</td>
     <td style="padding:0px"></td>
     </tr>
     <tr>
-    <td style="padding:10px">{}</td>
+    <td style="padding:10px">[]</td>
     <td style="padding:10px">{B}</td>
     <td style="padding:10px">{B}</td>
     <td style="padding:0px"></td>
     <td style="padding:0px"></td>
     </tr>
     <tr>
-    <td style="padding:10px">{}</td>
+    <td style="padding:10px">[]</td>
     <td style="padding:0px"></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
 :exec For_k_loop
 ```
 
 %% Output
 
     Executed operation: For_k_loop(2,3,{S,A,C})
 
 %% Cell type:code id: tags:
 
 ``` prob
 :show
 ```
 
 %% Output
 
     <table style="font-family:monospace"><tbody>
     <tr>
     <td style="padding:10px">b</td>
     <td style="padding:10px">a</td>
     <td style="padding:10px">a</td>
     <td style="padding:10px">b</td>
     <td style="padding:10px">a</td>
     </tr>
     <tr>
     <td style="padding:10px">{B}</td>
     <td style="padding:10px">{A,C}</td>
     <td style="padding:10px">{A,C}</td>
     <td style="padding:10px">{B}</td>
     <td style="padding:10px">{A,C}</td>
     </tr>
     <tr>
     <td style="padding:10px">{S,A}</td>
     <td style="padding:10px">{B}</td>
     <td style="padding:10px">{S,C}</td>
     <td style="padding:10px">{S,A}</td>
     <td style="padding:0px"></td>
     </tr>
     <tr>
-    <td style="padding:10px">{}</td>
+    <td style="padding:10px">[]</td>
     <td style="padding:10px">{B}</td>
     <td style="padding:10px">{B}</td>
     <td style="padding:0px"></td>
     <td style="padding:0px"></td>
     </tr>
     <tr>
-    <td style="padding:10px">{}</td>
+    <td style="padding:10px">[]</td>
     <td style="padding:10px">{S,A,C}</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
 :exec For_k_loop
 ```
 
 %% Output
 
     Executed operation: For_k_loop(1,4,{S,A,C})
 
 %% Cell type:code id: tags:
 
 ``` prob
 :show
 ```
 
 %% Output
 
     <table style="font-family:monospace"><tbody>
     <tr>
     <td style="padding:10px">b</td>
     <td style="padding:10px">a</td>
     <td style="padding:10px">a</td>
     <td style="padding:10px">b</td>
     <td style="padding:10px">a</td>
     </tr>
     <tr>
     <td style="padding:10px">{B}</td>
     <td style="padding:10px">{A,C}</td>
     <td style="padding:10px">{A,C}</td>
     <td style="padding:10px">{B}</td>
     <td style="padding:10px">{A,C}</td>
     </tr>
     <tr>
     <td style="padding:10px">{S,A}</td>
     <td style="padding:10px">{B}</td>
     <td style="padding:10px">{S,C}</td>
     <td style="padding:10px">{S,A}</td>
     <td style="padding:0px"></td>
     </tr>
     <tr>
-    <td style="padding:10px">{}</td>
+    <td style="padding:10px">[]</td>
     <td style="padding:10px">{B}</td>
     <td style="padding:10px">{B}</td>
     <td style="padding:0px"></td>
     <td style="padding:0px"></td>
     </tr>
     <tr>
-    <td style="padding:10px">{}</td>
+    <td style="padding:10px">[]</td>
     <td style="padding:10px">{S,A,C}</td>
     <td style="padding:0px"></td>
     <td style="padding:0px"></td>
     <td style="padding:0px"></td>
     </tr>
     <tr>
     <td style="padding:10px">{S,A,C}</td>
     <td style="padding:0px"></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
 S : T(1,n-1)
 ```
 
 %% Output
 
     $\mathit{TRUE}$
     TRUE
 
 %% Cell type:code id: tags:
 
 ``` prob
 :exec Accept
 ```
 
 %% Output
 
     Executed operation: TRUE <-- Accept()
 
 %% Cell type:code id: tags:
 
 ``` prob
 (i,j,n)
 ```
 
 %% Output
 
     $(1\mapsto 5\mapsto 5)$
     (1↦5↦5)
 
 %% Cell type:code id: tags:
 
 ``` prob
 ```

info4/kapitel-3/PDA-Kellerautomaten-Unicode.ipynb

+%% 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 = # = Bottom-Symbol im Keller*/
+DEFINITIONS
+
+ 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 δ, Σ, Γ
+PROPERTIES
+ Σ = {a,b}    // das Eingabe-Alphabet
+ ∧
+ Γ = {A,`#`} // das Kelleralphabet
+ ∧
+ /* Der PDA für {a^m b^m| m>=1} ; Beispiel von Info 4 (Folie 95ff) */
+ δ = {     (z0,a,`#`)      ↦  (z0,[A,`#`]),
+           (z0,a,A)        ↦  (z0,[A,A]),
+           (z0,b,A)        ↦  (z1,[]),
+           (z1,`λ`,`#`) ↦  (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 ||
+  γ := [`#`] || // 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,`λ`,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
+
+    Executed operation: SETUP_CONSTANTS()
+
+%% Cell type:code id: tags:
+
+``` prob
+:init
+```
+
+%% Output
+
+    Executed operation: INITIALISATION()
+
+%% 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">`#`</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,`#`])
+
+%% Cell type:code id: tags:
+
+``` prob
+:exec Schritt
+```
+
+%% Output
+
+    Executed operation: Schritt(z0,[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">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">`#`</td>
+    <td style="padding:0px"></td>
+    </tr>
+    </tbody></table>
+    <Animation function visualisation>
+
+%% Cell type:code id: tags:
+
+``` prob
+(z,α,γ)
+```
+
+%% Output
+
+    $(\mathit{z0}\mapsto[\mathit{a},\mathit{b},\mathit{b}]\mapsto[\mathit{A},`\exists`])$
+    (z0↦[a,b,b]↦[A,`∃`])
+
+%% 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">`#`</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">`#`</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">`#`</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:code id: tags:
+
+``` prob
+:dot state_space
+```
+
+%% Output
+
+
+    <Dot visualization: state_space []>
+
+%% 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
+
+    Executed operation: SETUP_CONSTANTS()
+
+%% Cell type:code id: tags:
+
+``` prob
+:init
+```
+
+%% Output
+
+    Executed operation: INITIALISATION()
+
+%% Cell type:code id: tags:
+
+``` prob
+:table {z,x,X,z2,Xs| ((z,x,X)↦(z2,Xs)) : δ}
+```
+
+%% Output
+
+    |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|[]|
+    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
+```
+
+%% Cell type:code id: tags:
+
+``` prob
+```

info4/kapitel-3/PDA-Kellerautomaten.ipynb

 %% 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
 
  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 δ, Σ, Γ
 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()
+    Executed operation: SETUP_CONSTANTS()
 
 %% Cell type:code id: tags:
 
 ``` prob
 :init
 ```
 
 %% Output
 
-    Machine initialised using operation 1: $initialise_machine()
+    Executed operation: INITIALISATION()
 
 %% 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])$
+    $(\mathit{z0}\mapsto[\mathit{a},\mathit{b},\mathit{b}]\mapsto[\mathit{A},\mathit{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:code id: tags:
+
+``` prob
+```
+
 %% 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()
+    Executed operation: SETUP_CONSTANTS()
 
 %% Cell type:code id: tags:
 
 ``` prob
 :init
 ```
 
 %% Output
 
-    Machine initialised using operation 1: $initialise_machine()
+    Executed operation: INITIALISATION()
 
 %% 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}$|$[]$|
+    |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|[]|
     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
 ```
+
+%% Cell type:code id: tags:
+
+``` prob
+```

info4/kapitel-3/PDA_nach_kfG.ipynb

 %% Cell type:markdown id: tags:
 
 # PDA nach kfG
 
 Aus einem gegebenen PDA kann man auch eine kontextfreie Grammatik generieren, die die gleiche Sprache akzeptiert.
 
 %% Cell type:code id: tags:
 
 ``` prob
 ::load
 MACHINE PDA_to_CFG
 /* Translating a PDA to a CFG */
 SETS
- Z = {z0,z1,   symbol};
-   /* symbol: virtueller Zustand um S und andere Symbole in der Grammatik darzustellen */
- SYMBOLE={a,b, A, BOT, lambda,     S} /* BOT = # = Ende vom Keller */
+ Z = {z0,z1,   `-`};
+   /* `-`: virtueller Zustand um S und andere Symbole in der Grammatik darzustellen */
+ SYMBOLE={a,b, A, `#`, `λ`,     S} /* BOT = # = Ende vom Keller */
 DEFINITIONS
- kfG_Alphabet  == (Z*(SYMBOLE \ {lambda})*Z);
+ kfG_Alphabet  == (Z*(SYMBOLE \ {`λ`})*Z);
  Σ == {a,b};
- Γ == {A,BOT};
- PDA_Zustände == (Z-{symbol});
+ Γ == {A,`#`};
+ symbol == `-`; // virtueller Zustand für einfache Symbole
+ PDA_Zustände == (Z-{symbol}); // echte PDA Zustände
 
- SYMS(s) == IF (s=lambda) THEN [] ELSE [SYM(s)] END;
+ SYMS(s) == IF (s=`λ`) THEN [] ELSE [SYM(s)] END;
  SYM(s) == (symbol,s,symbol); // Darstellung eines Symbols als Tripel für die Grammatik
  kfG_TERMINALE == {x|∃t.(t∈Σ ∧ x=SYM(t))};
 
  "LibraryStrings.def";
  ANIMATION_FUNCTION1 == {r,c,i| r=1 ∧ c∈dom(cur) ∧
          i= IF ∃t.(t∈SYMBOLE ∧ cur(c) = (symbol |->t|-> symbol))
             THEN TO_STRING(prj2(Z,SYMBOLE)(prj1((Z*SYMBOLE),Z)(cur(c))))
             ELSE TO_STRING(cur(c)) END};
  ANIMATION_STR_JUSTIFY_LEFT == TRUE;
- SET_PREF_PP_SEQUENCES == TRUE
+ SET_PREF_PP_SEQUENCES == TRUE;
+ TOS == %(s1,s,s2).(s1:Z & s2:Z & s:SYMBOLE|
+           IF s1=symbol THEN TO_STRING(s)
+           ELSE conc(["(",TO_STRING(s1),",",
+                          TO_STRING(s),",",
+                          TO_STRING(s2),")"]) END);
+ CURS == conc((cur ; TOS)) // can be used for state space projection
 CONSTANTS δ, Regeln, RegelnP1, RegelnP2, RegelnP3, RegelnP4
 PROPERTIES
  /* Ein 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,[]) } ∧
+ δ = {     (z0, a, `#`) ↦ (z0,[A,`#`]),
+           (z0, a,  A)  ↦ (z0,[A,A]),
+           (z0, b,  A)  ↦ (z1,[]),
+           (z1,`λ`,`#`) ↦ (z1,[]),
+           (z1, b,  A)  ↦ (z1,[]) } ∧
 
   /*Die Regeln der kfG zum PDA*/
-  /* Punkt 1 Folie 109 */
-  RegelnP1 = { lhs,rhs | ∃z.(z∈PDA_Zustände ∧ lhs=SYM(S) ∧ rhs = [(z0,BOT,z)])} ∧
-  /* Punkt 2 Folie 109 */
+  /* Punkt 1 Folie 109: Regeln für das Startsymbol */
+  RegelnP1 = { lhs,rhs | #z.(z:PDA_Zustände & lhs=SYM(S) & rhs = [(z0,`#`,z)])} ∧
+  /* Punkt 2 Folie 109: Regeln für PDA Übergänge die "Poppen" */
   RegelnP2 = { lhs,rhs | ∃(z,a,A,z2).((z,a,A)↦(z2,[])∈δ ∧ lhs=(z,A,z2) ∧ rhs = SYMS(a)) } ∧
-  /* Punkt 3 Folie 110 */
+  /* Punkt 3 Folie 110: Regeln für PDA Übergänge die die Stapelgröße nicht verändern */
   RegelnP3 = { lhs,rhs | ∃(z,a,A,B,z1,z2).((z,a,A)↦(z1,[B])∈δ ∧ z2∈PDA_Zustände ∧
                    lhs=(z,A,z2) ∧ rhs = SYMS(a)^[(z1,B,z2)]) } ∧
-  /* Punkt 4 Folie 110 */
+  /* Punkt 4 Folie 110: Regeln für PDA Übergänge die auf den Stapel "Pushen" */
   RegelnP4 = { lhs,rhs | ∃(z,a,A,B,C,z1,z2,z3).((z,a,A)↦(z1,[B,C])∈δ ∧
                      z2∈PDA_Zustände ∧ z3∈PDA_Zustände ∧
                      lhs=(z,A,z3) ∧
                      rhs = SYMS(a)^[(z1,B,z2),(z2,C,z3)]) } ∧
 
   Regeln = RegelnP1 ∪ RegelnP2 ∪ RegelnP3 ∪ RegelnP4
 
 VARIABLES cur
 INVARIANT
  cur ∈ seq(kfG_Alphabet)
 INITIALISATION
   cur:=SYMS(S)
 OPERATIONS
   // Anwendung einer Grammatikregel
   ApplyRule(LHS,RHS,pre,post) = PRE LHS↦RHS ∈ Regeln ∧
                                     cur = pre^[LHS]^post ∧
                                     ran(pre) ⊆ kfG_TERMINALE /* Linksableitung */
   THEN
      cur := pre^RHS^post
   END
 END
 ```
 
 %% Output
 
     Loaded machine: PDA_to_CFG
 
 %% Cell type:code id: tags:
 
 ``` prob
 :constants
 ```
 
 %% Output
 
-    Machine constants set up using operation 0: $setup_constants()
+    Executed operation: SETUP_CONSTANTS()
 
 %% Cell type:code id: tags:
 
 ``` prob
 :init
 ```
 
 %% Output
 
-    Machine initialised using operation 1: $initialise_machine()
+    Executed operation: INITIALISATION()
 
 %% Cell type:code id: tags:
 
 ``` prob
-δ
+RegelnP1
 ```
 
 %% Output
 
-    $\{(\mathit{z0}\mapsto \mathit{a}\mapsto \mathit{A}\mapsto(\mathit{z0}\mapsto [A,A])),(\mathit{z0}\mapsto \mathit{a}\mapsto \mathit{BOT}\mapsto(\mathit{z0}\mapsto [A,BOT])),(\mathit{z0}\mapsto \mathit{b}\mapsto \mathit{A}\mapsto(\mathit{z1}\mapsto [])),(\mathit{z1}\mapsto \mathit{b}\mapsto \mathit{A}\mapsto(\mathit{z1}\mapsto [])),(\mathit{z1}\mapsto \mathit{lambda}\mapsto \mathit{BOT}\mapsto(\mathit{z1}\mapsto []))\}$
-    {(z0↦a↦A↦(z0↦[A,A])),(z0↦a↦BOT↦(z0↦[A,BOT])),(z0↦b↦A↦(z1↦[])),(z1↦b↦A↦(z1↦[])),(z1↦lambda↦BOT↦(z1↦[]))}
+    $\{(\mathit{\text{`}-\text{`}}\mapsto\mathit{S}\mapsto\mathit{\text{`}-\text{`}}\mapsto[(\mathit{z0}\mapsto\mathit{\text{`}\#\text{`}}\mapsto\mathit{z0})]),(\mathit{\text{`}-\text{`}}\mapsto\mathit{S}\mapsto\mathit{\text{`}-\text{`}}\mapsto[(\mathit{z0}\mapsto\mathit{\text{`}\#\text{`}}\mapsto\mathit{z1})])\}$
+    {(`-`↦S↦`-`↦[(z0↦`#`↦z0)]),(`-`↦S↦`-`↦[(z0↦`#`↦z1)])}
+
+%% Cell type:code id: tags:
+
+``` prob
+:table Regeln
+```
+
+%% Output
+
+    |prj111|prj112|prj12|prj2|
+    |---|---|---|---|
+    |z0|A|z0|[(`-`↦a↦`-`),(z0↦A↦z0),(z0↦A↦z0)]|
+    |z0|A|z0|[(`-`↦a↦`-`),(z0↦A↦z1),(z1↦A↦z0)]|
+    |z0|A|z1|[(`-`↦b↦`-`)]|
+    |z0|A|z1|[(`-`↦a↦`-`),(z0↦A↦z0),(z0↦A↦z1)]|
+    |z0|A|z1|[(`-`↦a↦`-`),(z0↦A↦z1),(z1↦A↦z1)]|
+    |z0|`#`|z0|[(`-`↦a↦`-`),(z0↦A↦z0),(z0↦`#`↦z0)]|
+    |z0|`#`|z0|[(`-`↦a↦`-`),(z0↦A↦z1),(z1↦`#`↦z0)]|
+    |z0|`#`|z1|[(`-`↦a↦`-`),(z0↦A↦z0),(z0↦`#`↦z1)]|
+    |z0|`#`|z1|[(`-`↦a↦`-`),(z0↦A↦z1),(z1↦`#`↦z1)]|
+    |z1|A|z1|[(`-`↦b↦`-`)]|
+    |z1|`#`|z1|[]|
+    |`-`|S|`-`|[(z0↦`#`↦z0)]|
+    |`-`|S|`-`|[(z0↦`#`↦z1)]|
+    prj111	prj112	prj12	prj2
+    z0	A	z0	[(`-`|->a|->`-`),(z0|->A|->z0),(z0|->A|->z0)]
+    z0	A	z0	[(`-`|->a|->`-`),(z0|->A|->z1),(z1|->A|->z0)]
+    z0	A	z1	[(`-`|->b|->`-`)]
+    z0	A	z1	[(`-`|->a|->`-`),(z0|->A|->z0),(z0|->A|->z1)]
+    z0	A	z1	[(`-`|->a|->`-`),(z0|->A|->z1),(z1|->A|->z1)]
+    z0	`#`	z0	[(`-`|->a|->`-`),(z0|->A|->z0),(z0|->`#`|->z0)]
+    z0	`#`	z0	[(`-`|->a|->`-`),(z0|->A|->z1),(z1|->`#`|->z0)]
+    z0	`#`	z1	[(`-`|->a|->`-`),(z0|->A|->z0),(z0|->`#`|->z1)]
+    z0	`#`	z1	[(`-`|->a|->`-`),(z0|->A|->z1),(z1|->`#`|->z1)]
+    z1	A	z1	[(`-`|->b|->`-`)]
+    z1	`#`	z1	[]
+    `-`	S	`-`	[(z0|->`#`|->z0)]
+    `-`	S	`-`	[(z0|->`#`|->z1)]
+
+%% Cell type:code id: tags:
+
+``` prob
+:table δ
+```
+
+%% Output
+
+    |prj111|prj112|prj12|prj21|prj22|
+    |---|---|---|---|---|
+    |z0|a|A|z0|[A,A]|
+    |z0|a|`#`|z0|[A,`#`]|
+    |z0|b|A|z1|[]|
+    |z1|b|A|z1|[]|
+    |z1|`λ`|`#`|z1|[]|
+    prj111	prj112	prj12	prj21	prj22
+    z0	a	A	z0	[A,A]
+    z0	a	`#`	z0	[A,`#`]
+    z0	b	A	z1	[]
+    z1	b	A	z1	[]
+    z1	`λ`	`#`	z1	[]
 
 %% Cell type:markdown id: tags:
 
 Die Grammatik startet mit dem Startsymbol und simuliert die Ausführung eines entsprechenden PDAs. Dabei gibt es teils mehrere Wege, aber das Wort $ab$ wird von mindestens einem erreicht.
 
 %% Cell type:code id: tags:
 
 ``` prob
 :show
 ```
 
 %% Output
 
     <table style="font-family:monospace"><tbody>
     <tr>
     <td style="padding:10px">S</td>
     </tr>
     </tbody></table>
     <Animation function visualisation>
 
 %% Cell type:code id: tags:
 
 ``` prob
 :browse
 ```
 
 %% Output
 
     Machine: PDA_to_CFG
     Sets: Z, SYMBOLE
     Constants: δ, Regeln, RegelnP1, RegelnP2, RegelnP3, RegelnP4
     Variables: cur
     Operations:
-    ApplyRule((symbol|->S|->symbol),[(z0|->BOT|->z0)],[],[])
-    ApplyRule((symbol|->S|->symbol),[(z0|->BOT|->z1)],[],[])
+    ApplyRule((`-`|->S|->`-`),[(z0|->`#`|->z0)],[],[])
+    ApplyRule((`-`|->S|->`-`),[(z0|->`#`|->z1)],[],[])
 
 %% Cell type:code id: tags:
 
 ``` prob
-:exec ApplyRule RHS = [(z0|->BOT|->z1)]
+:exec ApplyRule RHS = [(z0|->`#`|->z1)]
 ```
 
 %% Output
 
-    Executed operation: ApplyRule((symbol|->S|->symbol),[(z0|->BOT|->z1)],[],[])
+    Executed operation: ApplyRule((`-`|->S|->`-`),[(z0|->`#`|->z1)],[],[])
 
 %% Cell type:code id: tags:
 
 ``` prob
 :show
 ```
 
 %% Output
 
     <table style="font-family:monospace"><tbody>
     <tr>
-    <td style="padding:10px">(z0|->BOT|->z1)</td>
+    <td style="padding:10px">(z0|->`#`|->z1)</td>
     </tr>
     </tbody></table>
     <Animation function visualisation>
 
 %% Cell type:code id: tags:
 
 ``` prob
-:exec ApplyRule RHS = [(symbol|->a|->symbol),(z0|->A|->z1),(z1|->BOT|->z1)]
+:exec ApplyRule RHS = [(`-`|->a|->`-`),(z0|->A|->z1),(z1|->`#`|->z1)]
 ```
 
 %% Output
 
-    Executed operation: ApplyRule((z0|->BOT|->z1),[(symbol|->a|->symbol),(z0|->A|->z1),(z1|->BOT|->z1)],[],[])
+    Executed operation: ApplyRule((z0|->`#`|->z1),[(`-`|->a|->`-`),(z0|->A|->z1),(z1|->`#`|->z1)],[],[])
 
 %% Cell type:code id: tags:
 
 ``` prob
 :show
 ```
 
 %% Output
 
     <table style="font-family:monospace"><tbody>
     <tr>
     <td style="padding:10px">a</td>
     <td style="padding:10px">(z0|->A|->z1)</td>
-    <td style="padding:10px">(z1|->BOT|->z1)</td>
+    <td style="padding:10px">(z1|->`#`|->z1)</td>
     </tr>
     </tbody></table>
     <Animation function visualisation>
 
 %% Cell type:code id: tags:
 
 ``` prob
-:exec ApplyRule RHS=[(symbol|->b|->symbol)]
+:exec ApplyRule RHS=[(`-`|->b|->`-`)]
 ```
 
 %% Output
 
-    Executed operation: ApplyRule((z0|->A|->z1),[(symbol|->b|->symbol)],[(symbol|->a|->symbol)],[(z1|->BOT|->z1)])
+    Executed operation: ApplyRule((z0|->A|->z1),[(`-`|->b|->`-`)],[(`-`|->a|->`-`)],[(z1|->`#`|->z1)])
 
 %% Cell type:code id: tags:
 
 ``` prob
 :show
 ```
 
 %% Output
 
     <table style="font-family:monospace"><tbody>
     <tr>
     <td style="padding:10px">a</td>
     <td style="padding:10px">b</td>
-    <td style="padding:10px">(z1|->BOT|->z1)</td>
+    <td style="padding:10px">(z1|->`#`|->z1)</td>
     </tr>
     </tbody></table>
     <Animation function visualisation>
 
 %% Cell type:code id: tags:
 
 ``` prob
 :exec ApplyRule
 ```
 
 %% Output
 
-    Executed operation: ApplyRule((z1|->BOT|->z1),[],[(symbol|->a|->symbol),(symbol|->b|->symbol)],[])
+    Executed operation: ApplyRule((z1|->`#`|->z1),[],[(`-`|->a|->`-`),(`-`|->b|->`-`)],[])
 
 %% Cell type:code id: tags:
 
 ``` prob
 :show
 ```
 
 %% Output
 
     <table style="font-family:monospace"><tbody>
     <tr>
     <td style="padding:10px">a</td>
     <td style="padding:10px">b</td>
     </tr>
     </tbody></table>
     <Animation function visualisation>
 
 %% Cell type:code id: tags:
 
 ``` prob
 :browse
 ```
 
 %% Output
 
     Machine: PDA_to_CFG
     Sets: Z, SYMBOLE
     Constants: δ, Regeln, RegelnP1, RegelnP2, RegelnP3, RegelnP4
     Variables: cur
     Operations:
 
 %% Cell type:markdown id: tags:
 
 Da das Wort fertig abgeleitet wurde ist keine Regel mehr ausführbar.
 
 %% Cell type:code id: tags:
 
 ``` prob
+:dot transition_diagram CURS
+```
+
+%% Output
+
+
+    <Dot visualization: transition_diagram [CURS]>
+
+%% Cell type:code id: tags:
+
+``` prob
 ```

info4/kapitel-4/DPDA.ipynb

 %% Cell type:markdown id: tags:
 
 # DPDA
 
 Ein __deterministischer Kellerautomat__
 (kurz DPDA für __deterministic push-down automaton__) ist ein $7$-Tupel
   $M = (\Sigma, \Gamma, Z, \delta , z_0, \#,F)$, 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,
 * $F \subseteq Z$ sind die Endzustände
 
 wo gilt:
 * $(\forall a \in \Sigma)\, (\forall A \in \Gamma)\, (\forall z \in
   Z)\, [ \|\delta(z, a, A)\| + \|\delta(z, \lambda , A)\| \leq 1]$
 
 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 DPDA
 /* B Modell eines PDA */
 SETS
  Z = {z0,z1,ze}; // die Zustände des Automaten, z0 ist der Startzustand
- SYMBOLE={a,b, A, BOT, lambda} /* BOT = # = Bottom-Symbol im Keller*/
+ SYMBOLE={a,b, A, `#`, `λ`} /* BOT = # = Bottom-Symbol im Keller*/
 DEFINITIONS
  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
+ SET_PREF_PP_SEQUENCES == TRUE;
+   "LibraryStrings.def";
+  dot_fields(seqval) == IF seqval=[] THEN "λ" ELSE
+               conc( %i.(i:1..size(seqval)-1| TO_STRING(seqval(i)) ^ "|") ) ^ TO_STRING(last(seqval))
+            END;
+  CUSTOM_GRAPH_NODES1 == rec(label:"{Eingabe α|{"^dot_fields(α)^"}}",
+                             shape:"record", style:"filled", fillcolor:"gray");
+  CUSTOM_GRAPH_NODES2 == rec(label:"{Keller γ|"^dot_fields(γ)^"}",
+                             shape:"record", style:"filled", fillcolor:"gray");
+  CUSTOM_GRAPH_NODES == {s•s:Z|rec(label:s,
+                                       shape: IF s:F THEN "doublecircle" ELSE "circle" END,
+                                       style:"filled",
+                                       fillcolor: IF s=z THEN "gray" ELSE "white" END)};
+  CUSTOM_GRAPH_EDGES == {z1,aa,bb,z2,G2•(z1,aa,bb)|->(z2,G2):δ| rec(from:z1,to:z2,label:aa)};
 CONSTANTS δ, F, Σ, Γ
 PROPERTIES
  Σ = {a,b}    // das Eingabe-Alphabet
  ∧
- Γ = {A,BOT} // das Kelleralphabet
+ Γ = {A,`#`} // 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,`#`)      ↦  (z0,[A,`#`]),
            (z0,a,A)        ↦  (z0,[A,A]),
            (z0,b,A)        ↦  (z1,[]),
-           (z1,lambda,BOT) ↦  (ze,[]),
+           (z1,`λ`,`#`)    ↦  (ze,[]),
            (z1,b,A)        ↦  (z1,[]) } ∧
  F = {ze} // die Endzustände
  // 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
 ASSERTIONS
   !(a,A,z).(a∈Σ ∧ A∈Γ ∧ z∈Z => card(δ[{(z,a,A)}]) + card(δ[{(z,a,A)}]) ≤ 1)
   /*@desc Die Überführungsfunktion ist deterministisch */
 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
+  γ := [`#`] || // 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‘↦s ∈ δ[{(z,`λ`,first(γ))}] THEN
      z := z‘ ||  // in den neuen Zustand wechseln
      γ := s^tail(γ) // s auf den Stapel packen
   END;
   Akzeptieren = PRE γ = ∅ ∧ z∈F THEN
         /* Wir akzeptieren wenn Eingabe leer und wir in einem Endzustand sind */
    skip END;
   AkzeptierenMitLeeremKeller = PRE γ = ∅ ∧ α = ∅ THEN
               /* Wir akzeptieren wenn Eingabe und Stapel leer sind */
    skip END
 END
 
 
 ```
 
 %% Output
 
     Loaded machine: DPDA
 
 %% Cell type:code id: tags:
 
 ``` prob
 :constants
 ```
 
 %% Output
 
-    Machine constants set up using operation 0: $setup_constants()
+    Executed operation: SETUP_CONSTANTS()
 
 %% Cell type:code id: tags:
 
 ``` prob
 :init
 ```
 
 %% Output
 
-    Machine initialised using operation 1: $initialise_machine()
+    Executed operation: INITIALISATION()
 
 %% Cell type:markdown id: tags:
 
 Wir prüfen nun ob der PDA auch wirklich deterministisch ist:
 
 %% Cell type:code id: tags:
 
 ``` prob
-!(a,A,z).(a∈Σ ∧ A∈Γ ∧ z∈Z => card(δ[{(z,a,A)}]) + card(δ[{(z,lambda,A)}]) ≤ 1)
+!(a,A,z).(a∈Σ ∧ A∈Γ ∧ z∈Z => card(δ[{(z,a,A)}]) + card(δ[{(z,`λ`,A)}]) ≤ 1)
 ```
 
 %% Output
 
     $\mathit{TRUE}$
     TRUE
 
 %% Cell type:markdown id: tags:
 
 Wir können uns auch tabellarisch für jede Kombination an Symbolen und Zuständen die Kardinalität der möglichen Übergange ausgeben:
 
 %% Cell type:code id: tags:
 
 ``` prob
-:table {a,A,z,ca,cl| a∈Σ ∧ A∈Γ ∧ z∈Z ∧ ca=card(δ[{(z,a,A)}]) & cl = card(δ[{(z,lambda,A)}])}
+:table {a,A,z,ca,cl| a∈Σ ∧ A∈Γ ∧ z∈Z ∧ ca=card(δ[{(z,a,A)}]) & cl = card(δ[{(z,`λ`,A)}])}
 ```
 
 %% Output
 
     |a|A|z|ca|cl|
     |---|---|---|---|---|
-    |$\mathit{a}$|$\mathit{A}$|$\mathit{z0}$|$1$|$0$|
-    |$\mathit{a}$|$\mathit{A}$|$\mathit{z1}$|$0$|$0$|
-    |$\mathit{a}$|$\mathit{A}$|$\mathit{ze}$|$0$|$0$|
-    |$\mathit{a}$|$\mathit{BOT}$|$\mathit{z0}$|$1$|$0$|
-    |$\mathit{a}$|$\mathit{BOT}$|$\mathit{z1}$|$0$|$1$|
-    |$\mathit{a}$|$\mathit{BOT}$|$\mathit{ze}$|$0$|$0$|
-    |$\mathit{b}$|$\mathit{A}$|$\mathit{z0}$|$1$|$0$|
-    |$\mathit{b}$|$\mathit{A}$|$\mathit{z1}$|$1$|$0$|
-    |$\mathit{b}$|$\mathit{A}$|$\mathit{ze}$|$0$|$0$|
-    |$\mathit{b}$|$\mathit{BOT}$|$\mathit{z0}$|$0$|$0$|
-    |$\mathit{b}$|$\mathit{BOT}$|$\mathit{z1}$|$0$|$1$|
-    |$\mathit{b}$|$\mathit{BOT}$|$\mathit{ze}$|$0$|$0$|
+    |a|A|z0|1|0|
+    |a|A|z1|0|0|
+    |a|A|ze|0|0|
+    |a|`#`|z0|1|0|
+    |a|`#`|z1|0|1|
+    |a|`#`|ze|0|0|
+    |b|A|z0|1|0|
+    |b|A|z1|1|0|
+    |b|A|ze|0|0|
+    |b|`#`|z0|0|0|
+    |b|`#`|z1|0|1|
+    |b|`#`|ze|0|0|
     a	A	z	ca	cl
     a	A	z0	1	0
     a	A	z1	0	0
     a	A	ze	0	0
-    a	BOT	z0	1	0
-    a	BOT	z1	0	1
-    a	BOT	ze	0	0
+    a	`#`	z0	1	0
+    a	`#`	z1	0	1
+    a	`#`	ze	0	0
     b	A	z0	1	0
     b	A	z1	1	0
     b	A	ze	0	0
-    b	BOT	z0	0	0
-    b	BOT	z1	0	1
-    b	BOT	ze	0	0
+    b	`#`	z0	0	0
+    b	`#`	z1	0	1
+    b	`#`	ze	0	0
 
 %% Cell type:code id: tags:
 
 ``` prob
 :browse
 ```
 
 %% Output
 
     Machine: DPDA
     Sets: Z, SYMBOLE
     Constants: δ, F, Σ, Γ
     Variables: z, α, γ
     Operations:
-    Schritt(z0,[A,BOT])
+    Schritt(z0,[A,`#`])
 
 %% Cell type:code id: tags:
 
 ``` prob
 :exec Schritt
 ```
 
 %% Output
 
-    Executed operation: Schritt(z0,[A,BOT])
+    Executed operation: Schritt(z0,[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">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:10px">`#`</td>
     <td style="padding:0px"></td>
     </tr>
     </tbody></table>
     <Animation function visualisation>
 
 %% Cell type:code id: tags:
 
 ``` prob
+:dot custom_graph
+```
+
+%% Output
+
+
+    <Dot visualization: custom_graph []>
+
+%% 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>
+    <td style="padding:10px">`#`</td>
     </tr>
     </tbody></table>
     <Animation function visualisation>
 
 %% 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>
+    <td style="padding:10px">`#`</td>
     </tr>
     </tbody></table>
     <Animation function visualisation>
 
 %% 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>
+    <td style="padding:10px">`#`</td>
     </tr>
     </tbody></table>
     <Animation function visualisation>
 
 %% Cell type:code id: tags:
 
 ``` prob
 :browse
 ```
 
 %% Output
 
     Machine: DPDA
     Sets: Z, SYMBOLE
     Constants: δ, F, Σ, Γ
     Variables: z, α, γ
     Operations:
     LambdaSchritt(ze,[])
 
 %% Cell type:code id: tags:
 
 ``` prob
 :exec LambdaSchritt
 ```
 
 %% Output
 
     Executed operation: LambdaSchritt(ze,[])
 
 %% 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">ze</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: DPDA
     Sets: Z, SYMBOLE
     Constants: δ, F, Σ, Γ
     Variables: z, α, γ
     Operations:
     Akzeptieren()
     AkzeptierenMitLeeremKeller()
 
 %% Cell type:code id: tags:
 
 ``` prob
 :exec Akzeptieren
 ```
 
 %% Output
 
     Executed operation: Akzeptieren()
 
 %% Cell type:code id: tags:
 
 ``` prob
 ```

info4/kapitel-5/TuringMaschine.ipynb

 %% Cell type:markdown id: tags:
 
 ## Turing Maschine
 
 
 %% Cell type:code id: tags:
 
 ``` prob
 ::load
 MACHINE TuringMachine_2
 /* B Modell einer 1-band Turing Maschine */
 /* by Michael Leuschel, 2012 */
 /* Akzeptiert die Sprache a^n b^n c^n (siehe Folien 14ff von folien-kapitel-5 */
 SETS
- Alphabet={a,b,c,X,Blank};
+ Alphabet={a,b,c,X,`◻︎`};
  States = {z0,z1,z2,z3,z4,z5,z6};
  Direction = {L,R,N}
 DEFINITIONS
   Σ == {a,b,c};
   Γ == Σ \/ {X};
-  CurSymbol == (Right<-Blank)(1);
+  CurSymbol == (Right<-`◻︎`)(1);
   ANIMATION_FUNCTION_DEFAULT == {(1,0,cur)};
  /* ANIMATION_FUNCTION__xx == {(1,1,Left), (1,3,Right)}; */
-  ANIMATION_FUNCTION1 == {1} *( (%i.(i:-size(Left)..-1|i+size(Left)+1) ; Left) \/ Right)
+  ANIMATION_FUNCTION1 == {1} *( (%i.(i:-size(Left)..-1|i+size(Left)+1) ; Left) \/ Right);
+
+  "LibraryStrings.def";
+  dot_fields(seqval) == IF seqval=[] THEN "λ" ELSE
+               conc( %i.(i:1..size(seqval)-1| TO_STRING(seqval(i)) ^ "|") ) ^ TO_STRING(last(seqval))
+            END;
+  CUSTOM_GRAPH_NODES1 == rec(label:"{left|{"^dot_fields(Left)^"}}",
+                             shape:"record", style:"filled", fillcolor:"gray90");
+  CUSTOM_GRAPH_NODES2 == rec(label:"{right|{"^dot_fields(Right)^"}}",
+                             shape:"record", style:"filled", fillcolor:"gray90");
+  CUSTOM_GRAPH_NODES == {s•s:States|rec(label:s,
+                                       shape: IF s:Final THEN "doublecircle" ELSE "circle" END,
+                                       style:"filled",
+                                       fillcolor: IF s=cur THEN "gray" ELSE "white" END)};
+  CUSTOM_GRAPH_EDGES == {z,a,z2,b,DIR•(z,a)|->(z2,b,DIR):δ| rec(from:z,to:z2,label:a)};
 CONSTANTS Final, δ
 PROPERTIES
  Final <: States &
  δ : (States * Alphabet) <-> (States * Alphabet * Direction) &
 
  δ = {  /* Neuer Zyklus */
             (z0,a) ↦ (z1,X,R),
             (z0,X) ↦ (z0,X,R),
 
             /* ein a getilgt (X), nächstes b suchen */
             (z1,a) ↦ (z1,a,R),
             (z1,b) ↦ (z2,X,R),
             (z1,X) ↦ (z1,X,R),
 
             /* ein a,b getilgt (X), nächstes c suchen */
             (z2,b) ↦ (z2,b,R),
             (z2,c) ↦ (z3,X,R),
             (z2,X) ↦ (z2,X,R),
 
             /* ein a,b,c getilgt (X), rechten Rand suchen */
             (z3,c) ↦ (z3,c,R),
-            (z3,Blank) ↦ (z4,Blank,L),
+            (z3,`◻︎`) ↦ (z4,`◻︎`,L),
 
             /* Zurücklaufen und testen ob alle a,b,c getilgt */
             (z4,X) ↦ (z4,X,L),
-            (z4,Blank) ↦ (z6,Blank,R),  /* Erfolg ! */
+            (z4,`◻︎`) ↦ (z6,`◻︎`,R),  /* Erfolg ! */
             (z4,c) ↦ (z5,c,L),
 
             /* Test nicht erfolgreich; zum linken Rand zurücklaufen und neuer Zyklus */
             (z5,X) ↦ (z5,X,L),
-            (z5,Blank) ↦ (z0,Blank,R),
+            (z5,`◻︎`) ↦ (z0,`◻︎`,R),
             (z5,a) ↦ (z5,a,L),
             (z5,b) ↦ (z5,b,L),
             (z5,c) ↦ (z5,c,L)
          } &
  Final = {z6}
 VARIABLES Left,cur,Right
 INVARIANT
   cur : States &
   Left : seq(Alphabet) & Right : seq(Alphabet)
 INITIALISATION Left,cur,Right := [],z0,[a,a,b,b,c,c]
 OPERATIONS
   Accept = PRE cur : Final THEN skip END;
   GoTo(z,S,znew,NewSymbol,Dir) =
    PRE z=cur & S=CurSymbol &
        (z, S) ↦ (znew,NewSymbol,Dir) : δ THEN
      ANY tail_Right
       WHERE (Right=[] ⇒ tail_Right=[]) & (Right/=[] ⇒ tail_Right = tail(Right)) THEN
       cur := znew ||
       IF Dir = N THEN
          Right := NewSymbol -> tail_Right
       ELSIF Dir = R THEN
          Left,Right := Left <- NewSymbol, tail_Right
       ELSIF Left=[] THEN
-         Left,Right := [], Blank -> (NewSymbol -> tail_Right)
+         Left,Right := [], `◻︎` -> (NewSymbol -> tail_Right)
       ELSE
          Left,Right := front(Left), last(Left) -> (NewSymbol -> tail_Right)
       END
      END
   END
 END
 ```
 
 %% Output
 
     Loaded machine: TuringMachine_2
 
 %% Cell type:code id: tags:
 
 ``` prob
 :constants
 ```
 
 %% Output
 
-    Machine constants set up using operation 0: $setup_constants()
+    Executed operation: SETUP_CONSTANTS()
 
 %% Cell type:code id: tags:
 
 ``` prob
 :init
 ```
 
 %% Output
 
-    Machine initialised using operation 1: $initialise_machine()
+    Executed operation: INITIALISATION()
 
 %% Cell type:code id: tags:
 
 ``` prob
 δ
 ```
 
 %% Output
 
-    $\{(\mathit{z0}\mapsto \mathit{a}\mapsto(\mathit{z1}\mapsto \mathit{X}\mapsto \mathit{R})),(\mathit{z0}\mapsto \mathit{X}\mapsto(\mathit{z0}\mapsto \mathit{X}\mapsto \mathit{R})),(\mathit{z1}\mapsto \mathit{a}\mapsto(\mathit{z1}\mapsto \mathit{a}\mapsto \mathit{R})),(\mathit{z1}\mapsto \mathit{b}\mapsto(\mathit{z2}\mapsto \mathit{X}\mapsto \mathit{R})),(\mathit{z1}\mapsto \mathit{X}\mapsto(\mathit{z1}\mapsto \mathit{X}\mapsto \mathit{R})),(\mathit{z2}\mapsto \mathit{b}\mapsto(\mathit{z2}\mapsto \mathit{b}\mapsto \mathit{R})),(\mathit{z2}\mapsto \mathit{c}\mapsto(\mathit{z3}\mapsto \mathit{X}\mapsto \mathit{R})),(\mathit{z2}\mapsto \mathit{X}\mapsto(\mathit{z2}\mapsto \mathit{X}\mapsto \mathit{R})),(\mathit{z3}\mapsto \mathit{c}\mapsto(\mathit{z3}\mapsto \mathit{c}\mapsto \mathit{R})),(\mathit{z3}\mapsto \mathit{Blank}\mapsto(\mathit{z4}\mapsto \mathit{Blank}\mapsto \mathit{L})),(\mathit{z4}\mapsto \mathit{c}\mapsto(\mathit{z5}\mapsto \mathit{c}\mapsto \mathit{L})),(\mathit{z4}\mapsto \mathit{X}\mapsto(\mathit{z4}\mapsto \mathit{X}\mapsto \mathit{L})),(\mathit{z4}\mapsto \mathit{Blank}\mapsto(\mathit{z6}\mapsto \mathit{Blank}\mapsto \mathit{R})),(\mathit{z5}\mapsto \mathit{a}\mapsto(\mathit{z5}\mapsto \mathit{a}\mapsto \mathit{L})),(\mathit{z5}\mapsto \mathit{b}\mapsto(\mathit{z5}\mapsto \mathit{b}\mapsto \mathit{L})),(\mathit{z5}\mapsto \mathit{c}\mapsto(\mathit{z5}\mapsto \mathit{c}\mapsto \mathit{L})),(\mathit{z5}\mapsto \mathit{X}\mapsto(\mathit{z5}\mapsto \mathit{X}\mapsto \mathit{L})),(\mathit{z5}\mapsto \mathit{Blank}\mapsto(\mathit{z0}\mapsto \mathit{Blank}\mapsto \mathit{R}))\}$
-    {(z0↦a↦(z1↦X↦R)),(z0↦X↦(z0↦X↦R)),(z1↦a↦(z1↦a↦R)),(z1↦b↦(z2↦X↦R)),(z1↦X↦(z1↦X↦R)),(z2↦b↦(z2↦b↦R)),(z2↦c↦(z3↦X↦R)),(z2↦X↦(z2↦X↦R)),(z3↦c↦(z3↦c↦R)),(z3↦Blank↦(z4↦Blank↦L)),(z4↦c↦(z5↦c↦L)),(z4↦X↦(z4↦X↦L)),(z4↦Blank↦(z6↦Blank↦R)),(z5↦a↦(z5↦a↦L)),(z5↦b↦(z5↦b↦L)),(z5↦c↦(z5↦c↦L)),(z5↦X↦(z5↦X↦L)),(z5↦Blank↦(z0↦Blank↦R))}
+    $\{(\mathit{z0}\mapsto\mathit{a}\mapsto(\mathit{z1}\mapsto\mathit{X}\mapsto\mathit{R})),(\mathit{z0}\mapsto\mathit{X}\mapsto(\mathit{z0}\mapsto\mathit{X}\mapsto\mathit{R})),(\mathit{z1}\mapsto\mathit{a}\mapsto(\mathit{z1}\mapsto\mathit{a}\mapsto\mathit{R})),(\mathit{z1}\mapsto\mathit{b}\mapsto(\mathit{z2}\mapsto\mathit{X}\mapsto\mathit{R})),(\mathit{z1}\mapsto\mathit{X}\mapsto(\mathit{z1}\mapsto\mathit{X}\mapsto\mathit{R})),(\mathit{z2}\mapsto\mathit{b}\mapsto(\mathit{z2}\mapsto\mathit{b}\mapsto\mathit{R})),(\mathit{z2}\mapsto\mathit{c}\mapsto(\mathit{z3}\mapsto\mathit{X}\mapsto\mathit{R})),(\mathit{z2}\mapsto\mathit{X}\mapsto(\mathit{z2}\mapsto\mathit{X}\mapsto\mathit{R})),(\mathit{z3}\mapsto\mathit{c}\mapsto(\mathit{z3}\mapsto\mathit{c}\mapsto\mathit{R})),(\mathit{z3}\mapsto\mathit{\text{`}◻︎\text{`}}\mapsto(\mathit{z4}\mapsto\mathit{\text{`}◻︎\text{`}}\mapsto\mathit{L})),(\mathit{z4}\mapsto\mathit{c}\mapsto(\mathit{z5}\mapsto\mathit{c}\mapsto\mathit{L})),(\mathit{z4}\mapsto\mathit{X}\mapsto(\mathit{z4}\mapsto\mathit{X}\mapsto\mathit{L})),(\mathit{z4}\mapsto\mathit{\text{`}◻︎\text{`}}\mapsto(\mathit{z6}\mapsto\mathit{\text{`}◻︎\text{`}}\mapsto\mathit{R})),(\mathit{z5}\mapsto\mathit{a}\mapsto(\mathit{z5}\mapsto\mathit{a}\mapsto\mathit{L})),(\mathit{z5}\mapsto\mathit{b}\mapsto(\mathit{z5}\mapsto\mathit{b}\mapsto\mathit{L})),(\mathit{z5}\mapsto\mathit{c}\mapsto(\mathit{z5}\mapsto\mathit{c}\mapsto\mathit{L})),(\mathit{z5}\mapsto\mathit{X}\mapsto(\mathit{z5}\mapsto\mathit{X}\mapsto\mathit{L})),(\mathit{z5}\mapsto\mathit{\text{`}◻︎\text{`}}\mapsto(\mathit{z0}\mapsto\mathit{\text{`}◻︎\text{`}}\mapsto\mathit{R}))\}$
+    {(z0↦a↦(z1↦X↦R)),(z0↦X↦(z0↦X↦R)),(z1↦a↦(z1↦a↦R)),(z1↦b↦(z2↦X↦R)),(z1↦X↦(z1↦X↦R)),(z2↦b↦(z2↦b↦R)),(z2↦c↦(z3↦X↦R)),(z2↦X↦(z2↦X↦R)),(z3↦c↦(z3↦c↦R)),(z3↦`◻︎`↦(z4↦`◻︎`↦L)),(z4↦c↦(z5↦c↦L)),(z4↦X↦(z4↦X↦L)),(z4↦`◻︎`↦(z6↦`◻︎`↦R)),(z5↦a↦(z5↦a↦L)),(z5↦b↦(z5↦b↦L)),(z5↦c↦(z5↦c↦L)),(z5↦X↦(z5↦X↦L)),(z5↦`◻︎`↦(z0↦`◻︎`↦R))}
 
 %% Cell type:code id: tags:
 
 ``` prob
 :show
 ```
 
 %% Output
 
     <table style="font-family:monospace"><tbody>
     <tr>
     <td style="padding:10px">z0</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>
     <td style="padding:10px">c</td>
     <td style="padding:10px">c</td>
     </tr>
     </tbody></table>
     <Animation function visualisation>
 
 %% Cell type:code id: tags:
 
 ``` prob
 :browse
 ```
 
 %% Output
 
     Machine: TuringMachine_2
     Sets: Alphabet, States, Direction
     Constants: Final, δ
-    Variables: Left, cur, Right
+    Variables: Left, Right, cur
     Operations:
     GoTo(z0,a,z1,X,R)
 
 %% Cell type:code id: tags:
 
 ``` prob
+:dot custom_graph
+```
+
+%% Output
+
+
+    <Dot visualization: custom_graph []>
+
+%% Cell type:code id: tags:
+
+``` prob
 :exec GoTo
 ```
 
 %% Output
 
     Executed operation: GoTo(z0,a,z1,X,R)
 
 %% Cell type:code id: tags:
 
 ``` prob
 :show
 ```
 
 %% Output
 
     <table style="font-family:monospace"><tbody>
     <tr>
     <td style="padding:10px">X</td>
     <td style="padding:10px">z1</td>
     <td style="padding:10px">a</td>
     <td style="padding:10px">b</td>
     <td style="padding:10px">b</td>
     <td style="padding:10px">c</td>
     <td style="padding:10px">c</td>
     </tr>
     </tbody></table>
     <Animation function visualisation>
 
 %% Cell type:code id: tags:
 
 ``` prob
+:dot custom_graph
+```
+
+%% Output
+
+
+    <Dot visualization: custom_graph []>
+
+%% Cell type:code id: tags:
+
+``` prob
 :exec GoTo
 ```
 
 %% Output
 
     Executed operation: GoTo(z1,a,z1,a,R)
 
 %% Cell type:code id: tags:
 
 ``` prob
 :show
 ```
 
 %% Output
 
     <table style="font-family:monospace"><tbody>
     <tr>
     <td style="padding:10px">X</td>
     <td style="padding:10px">a</td>
     <td style="padding:10px">z1</td>
     <td style="padding:10px">b</td>
     <td style="padding:10px">b</td>
     <td style="padding:10px">c</td>
     <td style="padding:10px">c</td>
     </tr>
     </tbody></table>
     <Animation function visualisation>
 
 %% Cell type:code id: tags:
 
 ``` prob
 :exec GoTo
 ```
 
 %% Output
 
     Executed operation: GoTo(z1,b,z2,X,R)
 
 %% Cell type:code id: tags:
 
 ``` prob
 :show
 ```
 
 %% Output
 
     <table style="font-family:monospace"><tbody>
     <tr>
     <td style="padding:10px">X</td>
     <td style="padding:10px">a</td>
     <td style="padding:10px">X</td>
     <td style="padding:10px">z2</td>
     <td style="padding:10px">b</td>
     <td style="padding:10px">c</td>
     <td style="padding:10px">c</td>
     </tr>
     </tbody></table>
     <Animation function visualisation>
 
 %% Cell type:code id: tags:
 
 ``` prob
 :exec GoTo
 ```
 
 %% Output
 
     Executed operation: GoTo(z2,b,z2,b,R)
 
 %% Cell type:code id: tags:
 
 ``` prob
 :show
 ```
 
 %% Output
 
     <table style="font-family:monospace"><tbody>
     <tr>
     <td style="padding:10px">X</td>
     <td style="padding:10px">a</td>
     <td style="padding:10px">X</td>
     <td style="padding:10px">b</td>
     <td style="padding:10px">z2</td>
     <td style="padding:10px">c</td>
     <td style="padding:10px">c</td>
     </tr>
     </tbody></table>
     <Animation function visualisation>
 
 %% Cell type:code id: tags:
 
 ``` prob
 :exec GoTo
 ```
 
 %% Output
 
     Executed operation: GoTo(z2,c,z3,X,R)
 
 %% Cell type:code id: tags:
 
 ``` prob
 :show
 ```
 
 %% Output
 
     <table style="font-family:monospace"><tbody>
     <tr>
     <td style="padding:10px">X</td>
     <td style="padding:10px">a</td>
     <td style="padding:10px">X</td>
     <td style="padding:10px">b</td>
     <td style="padding:10px">X</td>
     <td style="padding:10px">z3</td>
     <td style="padding:10px">c</td>
     </tr>
     </tbody></table>
     <Animation function visualisation>
 
 %% Cell type:code id: tags:
 
 ``` prob
 :exec GoTo
 ```
 
 %% Output
 
     Executed operation: GoTo(z3,c,z3,c,R)
 
 %% Cell type:code id: tags:
 
 ``` prob
 :show
 ```
 
 %% Output
 
     <table style="font-family:monospace"><tbody>
     <tr>
     <td style="padding:10px">X</td>
     <td style="padding:10px">a</td>
     <td style="padding:10px">X</td>
     <td style="padding:10px">b</td>
     <td style="padding:10px">X</td>
     <td style="padding:10px">c</td>
     <td style="padding:10px">z3</td>
     </tr>
     </tbody></table>
     <Animation function visualisation>
 
 %% Cell type:code id: tags:
 
 ``` prob
 :exec GoTo
 ```
 
 %% Output
 
-    Executed operation: GoTo(z3,Blank,z4,Blank,L)
+    Executed operation: GoTo(z3,`◻︎`,z4,`◻︎`,L)
 
 %% Cell type:code id: tags:
 
 ``` prob
 :show
 ```
 
 %% Output
 
     <table style="font-family:monospace"><tbody>
     <tr>
     <td style="padding:10px">X</td>
     <td style="padding:10px">a</td>
     <td style="padding:10px">X</td>
     <td style="padding:10px">b</td>
     <td style="padding:10px">X</td>
     <td style="padding:10px">z4</td>
     <td style="padding:10px">c</td>
-    <td style="padding:10px">Blank</td>
+    <td style="padding:10px">`◻︎`</td>
     </tr>
     </tbody></table>
     <Animation function visualisation>
 
 %% Cell type:code id: tags:
 
 ``` prob
 :exec GoTo
 ```
 
 %% Output
 
     Executed operation: GoTo(z4,c,z5,c,L)
 
 %% Cell type:code id: tags:
 
 ``` prob
 :show
 ```
 
 %% Output
 
     <table style="font-family:monospace"><tbody>
     <tr>
     <td style="padding:10px">X</td>
     <td style="padding:10px">a</td>
     <td style="padding:10px">X</td>
     <td style="padding:10px">b</td>
     <td style="padding:10px">z5</td>
     <td style="padding:10px">X</td>
     <td style="padding:10px">c</td>
-    <td style="padding:10px">Blank</td>
+    <td style="padding:10px">`◻︎`</td>
     </tr>
     </tbody></table>
     <Animation function visualisation>
 
 %% Cell type:code id: tags:
 
 ``` prob
 :exec GoTo
 ```
 
 %% Output
 
     Executed operation: GoTo(z5,X,z5,X,L)
 
 %% Cell type:code id: tags:
 
 ``` prob
 :show
 ```
 
 %% Output
 
     <table style="font-family:monospace"><tbody>
     <tr>
     <td style="padding:10px">X</td>
     <td style="padding:10px">a</td>
     <td style="padding:10px">X</td>
     <td style="padding:10px">z5</td>
     <td style="padding:10px">b</td>
     <td style="padding:10px">X</td>
     <td style="padding:10px">c</td>
-    <td style="padding:10px">Blank</td>
+    <td style="padding:10px">`◻︎`</td>
     </tr>
     </tbody></table>
     <Animation function visualisation>
 
 %% Cell type:code id: tags:
 
 ``` prob
 :exec GoTo
 ```
 
 %% Output
 
     Executed operation: GoTo(z5,b,z5,b,L)
 
 %% Cell type:code id: tags:
 
 ``` prob
 :show
 ```
 
 %% Output
 
     <table style="font-family:monospace"><tbody>
     <tr>
     <td style="padding:10px">X</td>
     <td style="padding:10px">a</td>
     <td style="padding:10px">z5</td>
     <td style="padding:10px">X</td>
     <td style="padding:10px">b</td>
     <td style="padding:10px">X</td>
     <td style="padding:10px">c</td>
-    <td style="padding:10px">Blank</td>
+    <td style="padding:10px">`◻︎`</td>
     </tr>
     </tbody></table>
     <Animation function visualisation>
 
 %% Cell type:code id: tags:
 
 ``` prob
 :exec GoTo
 ```
 
 %% Output
 
     Executed operation: GoTo(z5,X,z5,X,L)
 
 %% Cell type:code id: tags:
 
 ``` prob
 :show
 ```
 
 %% Output
 
     <table style="font-family:monospace"><tbody>
     <tr>
     <td style="padding:10px">X</td>
     <td style="padding:10px">z5</td>
     <td style="padding:10px">a</td>
     <td style="padding:10px">X</td>
     <td style="padding:10px">b</td>
     <td style="padding:10px">X</td>
     <td style="padding:10px">c</td>
-    <td style="padding:10px">Blank</td>
+    <td style="padding:10px">`◻︎`</td>
     </tr>
     </tbody></table>
     <Animation function visualisation>
 
 %% Cell type:code id: tags:
 
 ``` prob
 :exec GoTo
 ```
 
 %% Output
 
     Executed operation: GoTo(z5,a,z5,a,L)
 
 %% Cell type:code id: tags:
 
 ``` prob
 :show
 ```
 
 %% Output
 
     <table style="font-family:monospace"><tbody>
     <tr>
     <td style="padding:10px">z5</td>
     <td style="padding:10px">X</td>
     <td style="padding:10px">a</td>
     <td style="padding:10px">X</td>
     <td style="padding:10px">b</td>
     <td style="padding:10px">X</td>
     <td style="padding:10px">c</td>
-    <td style="padding:10px">Blank</td>
+    <td style="padding:10px">`◻︎`</td>
     </tr>
     </tbody></table>
     <Animation function visualisation>
 
 %% Cell type:code id: tags:
 
 ``` prob
 :exec GoTo
 ```
 
 %% Output
 
     Executed operation: GoTo(z5,X,z5,X,L)
 
 %% Cell type:code id: tags:
 
 ``` prob
 :show
 ```
 
 %% Output
 
     <table style="font-family:monospace"><tbody>
     <tr>
     <td style="padding:10px">z5</td>
-    <td style="padding:10px">Blank</td>
+    <td style="padding:10px">`◻︎`</td>
     <td style="padding:10px">X</td>
     <td style="padding:10px">a</td>
     <td style="padding:10px">X</td>
     <td style="padding:10px">b</td>
     <td style="padding:10px">X</td>
     <td style="padding:10px">c</td>
-    <td style="padding:10px">Blank</td>
+    <td style="padding:10px">`◻︎`</td>
     </tr>
     </tbody></table>
     <Animation function visualisation>
 
 %% Cell type:code id: tags:
 
 ``` prob
 :exec GoTo
 ```
 
 %% Output
 
-    Executed operation: GoTo(z5,Blank,z0,Blank,R)
+    Executed operation: GoTo(z5,`◻︎`,z0,`◻︎`,R)
 
 %% Cell type:code id: tags:
 
 ``` prob
 :show
 ```
 
 %% Output
 
     <table style="font-family:monospace"><tbody>
     <tr>
-    <td style="padding:10px">Blank</td>
+    <td style="padding:10px">`◻︎`</td>
     <td style="padding:10px">z0</td>
     <td style="padding:10px">X</td>
     <td style="padding:10px">a</td>
     <td style="padding:10px">X</td>
     <td style="padding:10px">b</td>
     <td style="padding:10px">X</td>
     <td style="padding:10px">c</td>
-    <td style="padding:10px">Blank</td>
+    <td style="padding:10px">`◻︎`</td>
     </tr>
     </tbody></table>
     <Animation function visualisation>
 
 %% Cell type:code id: tags:
 
 ``` prob
 :exec GoTo
 ```
 
 %% Output
 
     Executed operation: GoTo(z0,X,z0,X,R)
 
 %% Cell type:code id: tags:
 
 ``` prob
 :show
 ```
 
 %% Output
 
     <table style="font-family:monospace"><tbody>
     <tr>
-    <td style="padding:10px">Blank</td>
+    <td style="padding:10px">`◻︎`</td>
     <td style="padding:10px">X</td>
     <td style="padding:10px">z0</td>
     <td style="padding:10px">a</td>
     <td style="padding:10px">X</td>
     <td style="padding:10px">b</td>
     <td style="padding:10px">X</td>
     <td style="padding:10px">c</td>
-    <td style="padding:10px">Blank</td>
+    <td style="padding:10px">`◻︎`</td>
     </tr>
     </tbody></table>
     <Animation function visualisation>
 
 %% Cell type:code id: tags:
 
 ``` prob
 :exec GoTo
 ```
 
 %% Output
 
     Executed operation: GoTo(z0,a,z1,X,R)
 
 %% Cell type:code id: tags:
 
 ``` prob
 :show
 ```
 
 %% Output
 
     <table style="font-family:monospace"><tbody>
     <tr>
-    <td style="padding:10px">Blank</td>
+    <td style="padding:10px">`◻︎`</td>
     <td style="padding:10px">X</td>
     <td style="padding:10px">X</td>
     <td style="padding:10px">z1</td>
     <td style="padding:10px">X</td>
     <td style="padding:10px">b</td>
     <td style="padding:10px">X</td>
     <td style="padding:10px">c</td>
-    <td style="padding:10px">Blank</td>
+    <td style="padding:10px">`◻︎`</td>
     </tr>
     </tbody></table>
     <Animation function visualisation>
 
 %% Cell type:code id: tags:
 
 ``` prob
 :exec GoTo
 ```
 
 %% Output
 
     Executed operation: GoTo(z1,X,z1,X,R)
 
 %% Cell type:code id: tags:
 
 ``` prob
 :show
 ```
 
 %% Output
 
     <table style="font-family:monospace"><tbody>
     <tr>
-    <td style="padding:10px">Blank</td>
+    <td style="padding:10px">`◻︎`</td>
     <td style="padding:10px">X</td>
     <td style="padding:10px">X</td>
     <td style="padding:10px">X</td>
     <td style="padding:10px">z1</td>
     <td style="padding:10px">b</td>
     <td style="padding:10px">X</td>
     <td style="padding:10px">c</td>
-    <td style="padding:10px">Blank</td>
+    <td style="padding:10px">`◻︎`</td>
     </tr>
     </tbody></table>
     <Animation function visualisation>
 
 %% Cell type:code id: tags:
 
 ``` prob
 :exec GoTo
 ```
 
 %% Output
 
     Executed operation: GoTo(z1,b,z2,X,R)
 
 %% Cell type:code id: tags:
 
 ``` prob
 :show
 ```
 
 %% Output
 
     <table style="font-family:monospace"><tbody>
     <tr>
-    <td style="padding:10px">Blank</td>
+    <td style="padding:10px">`◻︎`</td>
     <td style="padding:10px">X</td>
     <td style="padding:10px">X</td>
     <td style="padding:10px">X</td>
     <td style="padding:10px">X</td>
     <td style="padding:10px">z2</td>
     <td style="padding:10px">X</td>
     <td style="padding:10px">c</td>
-    <td style="padding:10px">Blank</td>
+    <td style="padding:10px">`◻︎`</td>
     </tr>
     </tbody></table>
     <Animation function visualisation>
 
 %% Cell type:code id: tags:
 
 ``` prob
 :exec GoTo
 ```
 
 %% Output
 
     Executed operation: GoTo(z2,X,z2,X,R)
 
 %% Cell type:code id: tags:
 
 ``` prob
 :show
 ```
 
 %% Output
 
     <table style="font-family:monospace"><tbody>
     <tr>
-    <td style="padding:10px">Blank</td>
+    <td style="padding:10px">`◻︎`</td>
     <td style="padding:10px">X</td>
     <td style="padding:10px">X</td>
     <td style="padding:10px">X</td>
     <td style="padding:10px">X</td>
     <td style="padding:10px">X</td>
     <td style="padding:10px">z2</td>
     <td style="padding:10px">c</td>
-    <td style="padding:10px">Blank</td>
+    <td style="padding:10px">`◻︎`</td>
     </tr>
     </tbody></table>
     <Animation function visualisation>
 
 %% Cell type:code id: tags:
 
 ``` prob
 :exec GoTo
 ```
 
 %% Output
 
     Executed operation: GoTo(z2,c,z3,X,R)
 
 %% Cell type:code id: tags:
 
 ``` prob
 :show
 ```
 
 %% Output
 
     <table style="font-family:monospace"><tbody>
     <tr>
-    <td style="padding:10px">Blank</td>
+    <td style="padding:10px">`◻︎`</td>
     <td style="padding:10px">X</td>
     <td style="padding:10px">X</td>
     <td style="padding:10px">X</td>
     <td style="padding:10px">X</td>
     <td style="padding:10px">X</td>
     <td style="padding:10px">X</td>
     <td style="padding:10px">z3</td>
-    <td style="padding:10px">Blank</td>
+    <td style="padding:10px">`◻︎`</td>
     </tr>
     </tbody></table>
     <Animation function visualisation>
 
 %% Cell type:code id: tags:
 
 ``` prob
 :exec GoTo
 ```
 
 %% Output
 
-    Executed operation: GoTo(z3,Blank,z4,Blank,L)
+    Executed operation: GoTo(z3,`◻︎`,z4,`◻︎`,L)
 
 %% Cell type:code id: tags:
 
 ``` prob
 :show
 ```
 
 %% Output
 
     <table style="font-family:monospace"><tbody>
     <tr>
-    <td style="padding:10px">Blank</td>
+    <td style="padding:10px">`◻︎`</td>
     <td style="padding:10px">X</td>
     <td style="padding:10px">X</td>
     <td style="padding:10px">X</td>
     <td style="padding:10px">X</td>
     <td style="padding:10px">X</td>
     <td style="padding:10px">z4</td>
     <td style="padding:10px">X</td>
-    <td style="padding:10px">Blank</td>
+    <td style="padding:10px">`◻︎`</td>
     </tr>
     </tbody></table>
     <Animation function visualisation>
 
 %% Cell type:code id: tags:
 
 ``` prob
 :exec GoTo
 ```
 
 %% Output
 
     Executed operation: GoTo(z4,X,z4,X,L)
 
 %% Cell type:code id: tags:
 
 ``` prob
 :exec GoTo
 ```
 
 %% Output
 
     Executed operation: GoTo(z4,X,z4,X,L)
 
 %% Cell type:code id: tags:
 
 ``` prob
 :show
 ```
 
 %% Output
 
     <table style="font-family:monospace"><tbody>
     <tr>
-    <td style="padding:10px">Blank</td>
+    <td style="padding:10px">`◻︎`</td>
     <td style="padding:10px">X</td>
     <td style="padding:10px">X</td>
     <td style="padding:10px">X</td>
     <td style="padding:10px">z4</td>
     <td style="padding:10px">X</td>
     <td style="padding:10px">X</td>
     <td style="padding:10px">X</td>
-    <td style="padding:10px">Blank</td>
+    <td style="padding:10px">`◻︎`</td>
     </tr>
     </tbody></table>
     <Animation function visualisation>
 
 %% Cell type:code id: tags:
 
 ``` prob
 :exec GoTo
 ```
 
 %% Output
 
     Executed operation: GoTo(z4,X,z4,X,L)
 
 %% Cell type:code id: tags:
 
 ``` prob
 :exec GoTo
 ```
 
 %% Output
 
     Executed operation: GoTo(z4,X,z4,X,L)
 
 %% Cell type:code id: tags:
 
 ``` prob
 :show
 ```
 
 %% Output
 
     <table style="font-family:monospace"><tbody>
     <tr>
-    <td style="padding:10px">Blank</td>
+    <td style="padding:10px">`◻︎`</td>
     <td style="padding:10px">X</td>
     <td style="padding:10px">z4</td>
     <td style="padding:10px">X</td>
     <td style="padding:10px">X</td>
     <td style="padding:10px">X</td>
     <td style="padding:10px">X</td>
     <td style="padding:10px">X</td>
-    <td style="padding:10px">Blank</td>
+    <td style="padding:10px">`◻︎`</td>
     </tr>
     </tbody></table>
     <Animation function visualisation>
 
 %% Cell type:code id: tags:
 
 ``` prob
 :exec GoTo
 ```
 
 %% Output
 
     Executed operation: GoTo(z4,X,z4,X,L)
 
 %% Cell type:code id: tags:
 
 ``` prob
 :show
 ```
 
 %% Output
 
     <table style="font-family:monospace"><tbody>
     <tr>
-    <td style="padding:10px">Blank</td>
+    <td style="padding:10px">`◻︎`</td>
     <td style="padding:10px">z4</td>
     <td style="padding:10px">X</td>
     <td style="padding:10px">X</td>
     <td style="padding:10px">X</td>
     <td style="padding:10px">X</td>
     <td style="padding:10px">X</td>
     <td style="padding:10px">X</td>
-    <td style="padding:10px">Blank</td>
+    <td style="padding:10px">`◻︎`</td>
     </tr>
     </tbody></table>
     <Animation function visualisation>
 
 %% Cell type:code id: tags:
 
 ``` prob
 :exec GoTo
 ```
 
 %% Output
 
     Executed operation: GoTo(z4,X,z4,X,L)
 
 %% Cell type:code id: tags:
 
 ``` prob
 :show
 ```
 
 %% Output
 
     <table style="font-family:monospace"><tbody>
     <tr>
     <td style="padding:10px">z4</td>
-    <td style="padding:10px">Blank</td>
+    <td style="padding:10px">`◻︎`</td>
     <td style="padding:10px">X</td>
     <td style="padding:10px">X</td>
     <td style="padding:10px">X</td>
     <td style="padding:10px">X</td>
     <td style="padding:10px">X</td>
     <td style="padding:10px">X</td>
-    <td style="padding:10px">Blank</td>
+    <td style="padding:10px">`◻︎`</td>
     </tr>
     </tbody></table>
     <Animation function visualisation>
 
 %% Cell type:code id: tags:
 
 ``` prob
 :exec GoTo
 ```
 
 %% Output
 
-    Executed operation: GoTo(z4,Blank,z6,Blank,R)
+    Executed operation: GoTo(z4,`◻︎`,z6,`◻︎`,R)
 
 %% Cell type:code id: tags:
 
 ``` prob
 :show
 ```
 
 %% Output
 
     <table style="font-family:monospace"><tbody>
     <tr>
-    <td style="padding:10px">Blank</td>
+    <td style="padding:10px">`◻︎`</td>
     <td style="padding:10px">z6</td>
     <td style="padding:10px">X</td>
     <td style="padding:10px">X</td>
     <td style="padding:10px">X</td>
     <td style="padding:10px">X</td>
     <td style="padding:10px">X</td>
     <td style="padding:10px">X</td>
-    <td style="padding:10px">Blank</td>
+    <td style="padding:10px">`◻︎`</td>
     </tr>
     </tbody></table>
     <Animation function visualisation>
 
 %% Cell type:code id: tags:
 
 ``` prob
 :browse
 ```
 
 %% Output
 
     Machine: TuringMachine_2
     Sets: Alphabet, States, Direction
     Constants: Final, δ
-    Variables: Left, cur, Right
+    Variables: Left, Right, cur
     Operations:
     Accept()
 
 %% Cell type:code id: tags:
 
 ``` prob
 :exec Accept
 ```
 
 %% Output
 
     Executed operation: Accept()
 
 %% Cell type:code id: tags:
 
 ``` prob
 ```