{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Grammatiken und Chomsky-Hierarchie\n",
    "\n",
    "Dieses Notebook begleitet Teil 2 der Vorlesung 3 und führt am Ende die Chomsky-Hierarchie ein."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Eine __Grammatik__ ist ein Quadrupel \n",
    "$G = (\\Sigma , N, S, P)$, wobei\n",
    "* $\\Sigma$ ein Alphabet (von so genannten __Terminalsymbolen__) ist,\n",
    "* $N$ eine endliche Menge (von so genannten __Nichtterminalen__) mit\n",
    "  $\\Sigma \\cap N = \\emptyset$,\n",
    "* $S \\in N$ das __Startsymbol__ und\n",
    "* $P \\subseteq (N \\cup \\Sigma)^+ \\times (N \\cup \\Sigma)^{\\ast}$ die\n",
    "  endliche Menge der __Produktionen__ (Regeln).\n",
    "  \n",
    "Diese mathematische Definition setzen wir im Notebook folgendermaßen um.\n",
    "Wir verwenden eine B Maschine um eine neue Basismenge an Symbolen (ΣN) einführen zu können.\n",
    "Hier steht ```seq1(T)``` für die nicht leeren Folgen über T, also $T^+$ in der Notation des Skripts."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Loaded machine: Grammatik"
      ]
     },
     "execution_count": 1,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "::load\n",
    "MACHINE Grammatik\n",
    "SETS ΣN = {a,b,c, S}\n",
    "CONSTANTS Σ, N, P\n",
    "PROPERTIES\n",
    "   Σ = {a,b,c} ∧\n",
    "   Σ ∩ N = {} ∧\n",
    "   Σ ∪ N = ΣN ∧\n",
    "   S ∈ N ∧\n",
    "   P ⊆ seq1(ΣN) × seq(ΣN) ∧\n",
    "   \n",
    "   // Die Beispiel Grammatik G1 von den Folien\n",
    "   P = { [S] ↦ [],\n",
    "         [S] ↦ [a,S,b]\n",
    "       }\n",
    "DEFINITIONS SET_PREF_PP_SEQUENCES == TRUE\n",
    "END"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Machine constants set up using operation 0: $setup_constants()"
      ]
     },
     "execution_count": 2,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":constants"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "$\\mathit{TRUE}$\n",
       "\n",
       "**Solution:**\n",
       "* $\\mathit{RHS} = []$"
      ],
      "text/plain": [
       "TRUE\n",
       "\n",
       "Solution:\n",
       "\tRHS = []"
      ]
     },
     "execution_count": 3,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "[S] ↦ RHS ∈ P"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Mit dem relationalen Bild können wir alle Regeln mit der Folge S auf der rechten Seite finden:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "$\\{[],[a,\\mathit{S},b]\\}$"
      ],
      "text/plain": [
       "{[],[a,S,b]}"
      ]
     },
     "execution_count": 4,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "P[{ [S] }]"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Definiere die __unmittelbare Ableitungsrelation__ bzgl. $G$ so\n",
    "\n",
    "* $u \\vdash_{G} v \\Longleftrightarrow u = xpz, v = xqz$,\n",
    "\n",
    "wobei $x,z \\in (N \\cup \\Sigma)^{\\ast}$ und $p \\rightarrow q$ eine Regel in $P$\n",
    "ist.\n",
    "\n",
    "Im Notebook können wir dies so umsetzen, können aber leider nicht das Symbol $\\vdash_G$ verwenden.\n",
    "Aus $u \\vdash_{G} v$ wird $u \\mapsto v \\in abl$."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Loaded machine: Grammatik"
      ]
     },
     "execution_count": 5,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "::load\n",
    "MACHINE Grammatik\n",
    "SETS ΣN = {a,b,c, S}\n",
    "CONSTANTS Σ, N, P\n",
    "ABSTRACT_CONSTANTS abl\n",
    "PROPERTIES\n",
    "   Σ = {a,b,c} ∧\n",
    "   Σ ∩ N = {} ∧\n",
    "   Σ ∪ N = ΣN ∧\n",
    "   S ∈ N ∧\n",
    "   P ⊆ seq1(ΣN) × seq(ΣN) ∧\n",
    "   \n",
    "   // Die Beispiel Grammatik G1 von den Folien\n",
    "   P = { [S] ↦ [],\n",
    "         [S] ↦ [a,S,b]\n",
    "       }\n",
    "       \n",
    "   ∧ \n",
    "   abl = {u,v | ∃(x,z,p,q).( p↦q ∈ P ∧ u = x^p^z ∧ v = x^q^z )}\n",
    "DEFINITIONS SET_PREF_PP_SEQUENCES == TRUE\n",
    "END"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Machine constants set up using operation 0: $setup_constants()"
      ]
     },
     "execution_count": 6,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":constants"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Da diese Relation ```abl``` unendlich ist wird diese im Notebook symbolisch gehalten. Wir können aber prüfen ob Paare an Folgen in der Relation sind:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "$\\newcommand{\\qdot}{\\mathord{\\mkern1mu\\cdot\\mkern1mu}}/*@symbolic*/ \\{\\mathit{u},\\mathit{v}\\mid\\exists(\\mathit{x},\\mathit{z},\\mathit{p},\\mathit{q})\\qdot(\\mathit{p} \\mapsto \\mathit{q} \\in \\{([S]\\mapsto []),([S]\\mapsto [a,\\mathit{S},b])\\} \\land \\mathit{u} = \\mathit{x} ⌒ \\mathit{p} ⌒ \\mathit{z} \\land \\mathit{v} = \\mathit{x} ⌒ \\mathit{q} ⌒ \\mathit{z})\\}$"
      ],
      "text/plain": [
       "/*@symbolic*/ {u,v∣∃(x,z,p,q)·(p ↦ q ∈ {([S]↦[]),([S]↦[a,S,b])} ∧ u = x ⌒ p ⌒ z ∧ v = x ⌒ q ⌒ z)}"
      ]
     },
     "execution_count": 7,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "abl"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "$\\mathit{TRUE}$"
      ],
      "text/plain": [
       "TRUE"
      ]
     },
     "execution_count": 8,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "[a,S,b,S] ↦ [a,S,b,a,S,b] ∈ abl"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "$\\mathit{FALSE}$"
      ],
      "text/plain": [
       "FALSE"
      ]
     },
     "execution_count": 9,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "[S] ↦ [a,b] ∈ abl"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 10,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "$\\mathit{TRUE}$\n",
       "\n",
       "**Solution:**\n",
       "* $\\mathit{x} = []$"
      ],
      "text/plain": [
       "TRUE\n",
       "\n",
       "Solution:\n",
       "\tx = []"
      ]
     },
     "execution_count": 10,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "[S] ↦ x ∈ abl"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Mit dem relationalen Abbild können wir die Menge aller Umschreibungen berrechnen:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 11,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "$\\{[],[a,\\mathit{S},b]\\}$"
      ],
      "text/plain": [
       "{[],[a,S,b]}"
      ]
     },
     "execution_count": 11,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "abl[ { [S] } ]"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 12,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "$\\{[a,\\mathit{b},S],[a,\\mathit{S},b],[a,\\mathit{S},\\mathit{b},\\mathit{a},\\mathit{S},b],[a,\\mathit{a},\\mathit{S},\\mathit{b},\\mathit{b},S]\\}$"
      ],
      "text/plain": [
       "{[a,b,S],[a,S,b],[a,S,b,a,S,b],[a,a,S,b,b,S]}"
      ]
     },
     "execution_count": 12,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "abl[ {[a,S,b,S]} ]"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Durch mehrfache Anwendung bekommen wir die Ergebnisse von immer längeren Ableitungen:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 13,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "$\\{[a,b],[a,\\mathit{a},\\mathit{S},\\mathit{b},b]\\}$"
      ],
      "text/plain": [
       "{[a,b],[a,a,S,b,b]}"
      ]
     },
     "execution_count": 13,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "abl[ abl[ {[S]} ] ]"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 14,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "$\\{[a,\\mathit{a},\\mathit{b},b],[a,\\mathit{a},\\mathit{a},\\mathit{S},\\mathit{b},\\mathit{b},b]\\}$"
      ],
      "text/plain": [
       "{[a,a,b,b],[a,a,a,S,b,b,b]}"
      ]
     },
     "execution_count": 14,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "abl[ abl[ abl[ {[S]} ] ] ]"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Durch $n$-malige Anwendung von $\\vdash_{G}$ erhalten wir\n",
    "  $\\vdash_{G}^{n}$.  Das heiß t:\n",
    " \n",
    "* $u \\vdash_{G}^{n} v \\Longleftrightarrow u = x_0 \\vdash_{G} x_1\n",
    "\\vdash_{G} \\cdots \\vdash_{G} x_n = v$\n",
    "\n",
    "Im Notebook kann man für die n-malige Anwendung einer binären Relation den Operator ```iterate``` verwenden:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 15,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "$\\mathit{TRUE}$"
      ],
      "text/plain": [
       "TRUE"
      ]
     },
     "execution_count": 15,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "[S] ↦ [a,b] ∈ iterate(abl,2)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Die Menge $\\{w \\mid S \\vdash_{G}^{n} w\\}$ kann direkt mit dem relationalen Bild berechnet werden. Zum Beispiel für n = 0,1,2,3,4:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 16,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "$\\{[S]\\}$"
      ],
      "text/plain": [
       "{[S]}"
      ]
     },
     "execution_count": 16,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    " iterate(abl,0)[ {[S]} ]"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 17,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "$\\{[],[a,\\mathit{S},b]\\}$"
      ],
      "text/plain": [
       "{[],[a,S,b]}"
      ]
     },
     "execution_count": 17,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    " iterate(abl,1)[ {[S]} ]"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 18,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "$\\{[a,b],[a,\\mathit{a},\\mathit{S},\\mathit{b},b]\\}$"
      ],
      "text/plain": [
       "{[a,b],[a,a,S,b,b]}"
      ]
     },
     "execution_count": 18,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    " iterate(abl,2)[ {[S]} ]"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 19,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "$\\{[a,\\mathit{a},\\mathit{b},b],[a,\\mathit{a},\\mathit{a},\\mathit{S},\\mathit{b},\\mathit{b},b]\\}$"
      ],
      "text/plain": [
       "{[a,a,b,b],[a,a,a,S,b,b,b]}"
      ]
     },
     "execution_count": 19,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    " iterate(abl,3)[ {[S]} ]"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 20,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "$\\{[a,\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{b},b],[a,\\mathit{a},\\mathit{a},\\mathit{a},\\mathit{S},\\mathit{b},\\mathit{b},\\mathit{b},b]\\}$"
      ],
      "text/plain": [
       "{[a,a,a,b,b,b],[a,a,a,a,S,b,b,b,b]}"
      ]
     },
     "execution_count": 20,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    " iterate(abl,4)[ {[S]} ]"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Die von der Grammatik $G$ erzeugte Sprache ist\n",
    "  definiert als\n",
    "$L(G) = \\{w \\in \\Sigma^* \\mid S \\vdash_{G}^{\\ast} w\\}.$\n",
    "\n",
    "Bis zur Länge 4 gibt es folgende abgeleitenen Wörter über $\\Sigma \\cup N$\n",
    "(auch Satzformen genannt):"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 21,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "$\\{[],[a,b],[S],[a,\\mathit{a},\\mathit{b},b],[a,\\mathit{S},b],[a,\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{b},b],[a,\\mathit{a},\\mathit{S},\\mathit{b},b],[a,\\mathit{a},\\mathit{a},\\mathit{S},\\mathit{b},\\mathit{b},b],[a,\\mathit{a},\\mathit{a},\\mathit{a},\\mathit{S},\\mathit{b},\\mathit{b},\\mathit{b},b]\\}$"
      ],
      "text/plain": [
       "{[],[a,b],[S],[a,a,b,b],[a,S,b],[a,a,a,b,b,b],[a,a,S,b,b],[a,a,a,S,b,b,b],[a,a,a,a,S,b,b,b,b]}"
      ]
     },
     "execution_count": 21,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "UNION(i).(i:0..4|iterate(abl,i)[ {[S]} ])"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Wenn wir mit $\\Sigma^*$ schneiden, bekommen wir Wörter der von der Grammatik generierten Sprache:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 22,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "$\\{[],[a,b],[a,\\mathit{a},\\mathit{b},b],[a,\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{b},b]\\}$"
      ],
      "text/plain": [
       "{[],[a,b],[a,a,b,b],[a,a,a,b,b,b]}"
      ]
     },
     "execution_count": 22,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "UNION(i).(i:0..4|iterate(abl,i)[ {[S]} ]) ∩ seq(Σ)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Wir können die Ableitungsrelationen für alle Satzformen bis zu einer gegebenen Tiefe auch grafisch darstellen."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 23,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "$\\{[],[a,b],[S],[a,\\mathit{a},\\mathit{b},b],[a,\\mathit{S},b],[a,\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{b},b],[a,\\mathit{a},\\mathit{S},\\mathit{b},b],[a,\\mathit{a},\\mathit{a},\\mathit{S},\\mathit{b},\\mathit{b},b],[a,\\mathit{a},\\mathit{a},\\mathit{a},\\mathit{S},\\mathit{b},\\mathit{b},\\mathit{b},b]\\}$"
      ],
      "text/plain": [
       "{[],[a,b],[S],[a,a,b,b],[a,S,b],[a,a,a,b,b,b],[a,a,S,b,b],[a,a,a,S,b,b,b],[a,a,a,a,S,b,b,b,b]}"
      ]
     },
     "execution_count": 23,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":let SF UNION(i).(i:0..4|iterate(abl,i)[ {[S]} ])"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 24,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Preference changed: DOT_DECOMPOSE_NODES = FALSE\n"
      ]
     },
     "execution_count": 24,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":pref DOT_DECOMPOSE_NODES=FALSE"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 25,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "image/svg+xml": [
       "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
       "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
       " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
       "<!-- Generated by graphviz version 2.44.1 (0)\n",
       " -->\n",
       "<!-- Title: state Pages: 1 -->\n",
       "<svg width=\"352pt\" height=\"392pt\"\n",
       " viewBox=\"0.00 0.00 351.50 392.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
       "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 388)\">\n",
       "<title>state</title>\n",
       "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-388 347.5,-388 347.5,4 -4,4\"/>\n",
       "<!-- [a,a,a,S,b,b,b] -->\n",
       "<g id=\"node1\" class=\"node\">\n",
       "<title>[a,a,a,S,b,b,b]</title>\n",
       "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"197,-123 82,-123 82,-87 197,-87 197,-123\"/>\n",
       "<text text-anchor=\"middle\" x=\"139.5\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\">[a,a,a,S,b,b,b]</text>\n",
       "</g>\n",
       "<!-- [a,a,a,a,S,b,b,b,b] -->\n",
       "<g id=\"node2\" class=\"node\">\n",
       "<title>[a,a,a,a,S,b,b,b,b]</title>\n",
       "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"141,-36 0,-36 0,0 141,0 141,-36\"/>\n",
       "<text text-anchor=\"middle\" x=\"70.5\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\">[a,a,a,a,S,b,b,b,b]</text>\n",
       "</g>\n",
       "<!-- [a,a,a,S,b,b,b]&#45;&gt;[a,a,a,a,S,b,b,b,b] -->\n",
       "<g id=\"edge1\" class=\"edge\">\n",
       "<title>[a,a,a,S,b,b,b]&#45;&gt;[a,a,a,a,S,b,b,b,b]</title>\n",
       "<path fill=\"none\" stroke=\"firebrick\" d=\"M125.54,-86.8C115.62,-74.59 102.15,-57.99 91.02,-44.28\"/>\n",
       "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"93.46,-41.73 84.44,-36.18 88.03,-46.15 93.46,-41.73\"/>\n",
       "<text text-anchor=\"middle\" x=\"120.5\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\">abl</text>\n",
       "</g>\n",
       "<!-- [a,a,a,b,b,b] -->\n",
       "<g id=\"node3\" class=\"node\">\n",
       "<title>[a,a,a,b,b,b]</title>\n",
       "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"260,-36 159,-36 159,0 260,0 260,-36\"/>\n",
       "<text text-anchor=\"middle\" x=\"209.5\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\">[a,a,a,b,b,b]</text>\n",
       "</g>\n",
       "<!-- [a,a,a,S,b,b,b]&#45;&gt;[a,a,a,b,b,b] -->\n",
       "<g id=\"edge2\" class=\"edge\">\n",
       "<title>[a,a,a,S,b,b,b]&#45;&gt;[a,a,a,b,b,b]</title>\n",
       "<path fill=\"none\" stroke=\"firebrick\" d=\"M153.67,-86.8C163.72,-74.59 177.39,-57.99 188.68,-44.28\"/>\n",
       "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"191.7,-46.12 195.36,-36.18 186.3,-41.67 191.7,-46.12\"/>\n",
       "<text text-anchor=\"middle\" x=\"190.5\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\">abl</text>\n",
       "</g>\n",
       "<!-- [a,a,S,b,b] -->\n",
       "<g id=\"node4\" class=\"node\">\n",
       "<title>[a,a,S,b,b]</title>\n",
       "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"240,-210 151,-210 151,-174 240,-174 240,-210\"/>\n",
       "<text text-anchor=\"middle\" x=\"195.5\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\">[a,a,S,b,b]</text>\n",
       "</g>\n",
       "<!-- [a,a,S,b,b]&#45;&gt;[a,a,a,S,b,b,b] -->\n",
       "<g id=\"edge3\" class=\"edge\">\n",
       "<title>[a,a,S,b,b]&#45;&gt;[a,a,a,S,b,b,b]</title>\n",
       "<path fill=\"none\" stroke=\"firebrick\" d=\"M184.17,-173.8C176.2,-161.7 165.39,-145.3 156.41,-131.67\"/>\n",
       "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"159.24,-129.6 150.82,-123.18 153.39,-133.45 159.24,-129.6\"/>\n",
       "<text text-anchor=\"middle\" x=\"182.5\" y=\"-144.8\" font-family=\"Times,serif\" font-size=\"14.00\">abl</text>\n",
       "</g>\n",
       "<!-- [a,a,b,b] -->\n",
       "<g id=\"node5\" class=\"node\">\n",
       "<title>[a,a,b,b]</title>\n",
       "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"290,-123 215,-123 215,-87 290,-87 290,-123\"/>\n",
       "<text text-anchor=\"middle\" x=\"252.5\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\">[a,a,b,b]</text>\n",
       "</g>\n",
       "<!-- [a,a,S,b,b]&#45;&gt;[a,a,b,b] -->\n",
       "<g id=\"edge4\" class=\"edge\">\n",
       "<title>[a,a,S,b,b]&#45;&gt;[a,a,b,b]</title>\n",
       "<path fill=\"none\" stroke=\"firebrick\" d=\"M207.03,-173.8C215.15,-161.7 226.14,-145.3 235.29,-131.67\"/>\n",
       "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"238.32,-133.43 240.98,-123.18 232.51,-129.53 238.32,-133.43\"/>\n",
       "<text text-anchor=\"middle\" x=\"238.5\" y=\"-144.8\" font-family=\"Times,serif\" font-size=\"14.00\">abl</text>\n",
       "</g>\n",
       "<!-- [a,S,b] -->\n",
       "<g id=\"node6\" class=\"node\">\n",
       "<title>[a,S,b]</title>\n",
       "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"271.5,-297 209.5,-297 209.5,-261 271.5,-261 271.5,-297\"/>\n",
       "<text text-anchor=\"middle\" x=\"240.5\" y=\"-275.3\" font-family=\"Times,serif\" font-size=\"14.00\">[a,S,b]</text>\n",
       "</g>\n",
       "<!-- [a,S,b]&#45;&gt;[a,a,S,b,b] -->\n",
       "<g id=\"edge5\" class=\"edge\">\n",
       "<title>[a,S,b]&#45;&gt;[a,a,S,b,b]</title>\n",
       "<path fill=\"none\" stroke=\"firebrick\" d=\"M231.39,-260.8C225.05,-248.82 216.47,-232.62 209.29,-219.06\"/>\n",
       "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"212.37,-217.38 204.59,-210.18 206.18,-220.65 212.37,-217.38\"/>\n",
       "<text text-anchor=\"middle\" x=\"232.5\" y=\"-231.8\" font-family=\"Times,serif\" font-size=\"14.00\">abl</text>\n",
       "</g>\n",
       "<!-- [a,b] -->\n",
       "<g id=\"node7\" class=\"node\">\n",
       "<title>[a,b]</title>\n",
       "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"312.5,-210 258.5,-210 258.5,-174 312.5,-174 312.5,-210\"/>\n",
       "<text text-anchor=\"middle\" x=\"285.5\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\">[a,b]</text>\n",
       "</g>\n",
       "<!-- [a,S,b]&#45;&gt;[a,b] -->\n",
       "<g id=\"edge6\" class=\"edge\">\n",
       "<title>[a,S,b]&#45;&gt;[a,b]</title>\n",
       "<path fill=\"none\" stroke=\"firebrick\" d=\"M249.61,-260.8C255.95,-248.82 264.53,-232.62 271.71,-219.06\"/>\n",
       "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"274.82,-220.65 276.41,-210.18 268.63,-217.38 274.82,-220.65\"/>\n",
       "<text text-anchor=\"middle\" x=\"277.5\" y=\"-231.8\" font-family=\"Times,serif\" font-size=\"14.00\">abl</text>\n",
       "</g>\n",
       "<!-- [S] -->\n",
       "<g id=\"node8\" class=\"node\">\n",
       "<title>[S]</title>\n",
       "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"305.5,-384 251.5,-384 251.5,-348 305.5,-348 305.5,-384\"/>\n",
       "<text text-anchor=\"middle\" x=\"278.5\" y=\"-362.3\" font-family=\"Times,serif\" font-size=\"14.00\">[S]</text>\n",
       "</g>\n",
       "<!-- [S]&#45;&gt;[a,S,b] -->\n",
       "<g id=\"edge7\" class=\"edge\">\n",
       "<title>[S]&#45;&gt;[a,S,b]</title>\n",
       "<path fill=\"none\" stroke=\"firebrick\" d=\"M270.81,-347.8C265.5,-335.93 258.35,-319.93 252.32,-306.45\"/>\n",
       "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"255.46,-304.88 248.18,-297.18 249.06,-307.73 255.46,-304.88\"/>\n",
       "<text text-anchor=\"middle\" x=\"273.5\" y=\"-318.8\" font-family=\"Times,serif\" font-size=\"14.00\">abl</text>\n",
       "</g>\n",
       "<!-- [] -->\n",
       "<g id=\"node9\" class=\"node\">\n",
       "<title>[]</title>\n",
       "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"343.5,-297 289.5,-297 289.5,-261 343.5,-261 343.5,-297\"/>\n",
       "<text text-anchor=\"middle\" x=\"316.5\" y=\"-275.3\" font-family=\"Times,serif\" font-size=\"14.00\">[]</text>\n",
       "</g>\n",
       "<!-- [S]&#45;&gt;[] -->\n",
       "<g id=\"edge8\" class=\"edge\">\n",
       "<title>[S]&#45;&gt;[]</title>\n",
       "<path fill=\"none\" stroke=\"firebrick\" d=\"M286.19,-347.8C291.5,-335.93 298.65,-319.93 304.68,-306.45\"/>\n",
       "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"307.94,-307.73 308.82,-297.18 301.54,-304.88 307.94,-307.73\"/>\n",
       "<text text-anchor=\"middle\" x=\"310.5\" y=\"-318.8\" font-family=\"Times,serif\" font-size=\"14.00\">abl</text>\n",
       "</g>\n",
       "</g>\n",
       "</svg>"
      ],
      "text/plain": [
       "<Dot visualization: expr_as_graph [SFSF={[],[a,b],[S],[a,a,b,b],[a,S,b],[a,a,a,b,b,b],[a,a,S,b,b],[a,a,a,S,b,b,b],[a,a,a,a,S,b,b,b,b]}(\"abl\",SF<|abl|>SF)]>"
      ]
     },
     "execution_count": 25,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":dot expr_as_graph (\"abl\",SF <| abl |> SF)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Die Grammatik G2 können wir wie folgt umsetzen:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 26,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Loaded machine: Grammatik2"
      ]
     },
     "execution_count": 26,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "::load\n",
    "MACHINE Grammatik2\n",
    "SETS ΣN = {a,b,c, S, B,C}\n",
    "CONSTANTS Σ, N, P\n",
    "ABSTRACT_CONSTANTS abl\n",
    "PROPERTIES\n",
    "   Σ = {a,b,c} ∧\n",
    "   Σ ∩ N = {} ∧\n",
    "   Σ ∪ N = ΣN ∧\n",
    "   S ∈ N ∧\n",
    "   P ⊆ seq1(ΣN) × seq(ΣN) ∧\n",
    "   \n",
    "   // Die Beispiel Grammatik G2 von den Folien\n",
    "   P = { [S] ↦ [a,B,C],\n",
    "         [S] ↦ [a,S,B,C],\n",
    "         [C,B] ↦ [B,C],\n",
    "         [a,B] ↦ [a,b],\n",
    "         [b,B] ↦ [b,b],\n",
    "         [b,C] ↦ [b,c],\n",
    "         [c,C] ↦ [c,c]\n",
    "       }\n",
    "       \n",
    "   ∧ \n",
    "   abl = {u,v | ∃(x,z,p,q).( p↦q ∈ P ∧ u = x^p^z ∧ v = x^q^z )}\n",
    "DEFINITIONS SET_PREF_PP_SEQUENCES == TRUE\n",
    "END"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 27,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Machine constants set up using operation 0: $setup_constants()"
      ]
     },
     "execution_count": 27,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":constants"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 28,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "$\\{[S],[a,\\mathit{b},c],[a,\\mathit{b},C],[a,\\mathit{S},\\mathit{B},C],[a,\\mathit{B},C],[a,\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{B},C],[a,\\mathit{a},\\mathit{b},\\mathit{C},\\mathit{B},C],[a,\\mathit{a},\\mathit{b},\\mathit{B},\\mathit{C},C],[a,\\mathit{a},\\mathit{B},\\mathit{C},\\mathit{B},C],[a,\\mathit{a},\\mathit{B},\\mathit{B},\\mathit{C},C],[a,\\mathit{a},\\mathit{S},\\mathit{B},\\mathit{C},\\mathit{B},C],[a,\\mathit{a},\\mathit{S},\\mathit{B},\\mathit{B},\\mathit{C},C],[a,\\mathit{a},\\mathit{a},\\mathit{S},\\mathit{B},\\mathit{C},\\mathit{B},\\mathit{B},\\mathit{C},C],[a,\\mathit{a},\\mathit{a},\\mathit{S},\\mathit{B},\\mathit{B},\\mathit{C},\\mathit{C},\\mathit{B},C],[a,\\mathit{a},\\mathit{a},\\mathit{S},\\mathit{B},\\mathit{C},\\mathit{B},\\mathit{C},\\mathit{B},C],[a,\\mathit{a},\\mathit{a},\\mathit{B},\\mathit{B},\\mathit{C},\\mathit{C},\\mathit{B},C],[a,\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{C},\\mathit{B},\\mathit{C},\\mathit{B},C],[a,\\mathit{a},\\mathit{a},\\mathit{B},\\mathit{C},\\mathit{B},\\mathit{B},\\mathit{C},C],[a,\\mathit{a},\\mathit{a},\\mathit{B},\\mathit{C},\\mathit{B},\\mathit{C},\\mathit{B},C],[a,\\mathit{a},\\mathit{a},\\mathit{a},\\mathit{B},\\mathit{C},\\mathit{B},\\mathit{C},\\mathit{B},\\mathit{C},\\mathit{B},C],[a,\\mathit{a},\\mathit{a},\\mathit{a},\\mathit{S},\\mathit{B},\\mathit{C},\\mathit{B},\\mathit{C},\\mathit{B},\\mathit{C},\\mathit{B},C]\\}$"
      ],
      "text/plain": [
       "{[S],[a,b,c],[a,b,C],[a,S,B,C],[a,B,C],[a,a,b,c,B,C],[a,a,b,C,B,C],[a,a,b,B,C,C],[a,a,B,C,B,C],[a,a,B,B,C,C],[a,a,S,B,C,B,C],[a,a,S,B,B,C,C],[a,a,a,S,B,C,B,B,C,C],[a,a,a,S,B,B,C,C,B,C],[a,a,a,S,B,C,B,C,B,C],[a,a,a,B,B,C,C,B,C],[a,a,a,b,C,B,C,B,C],[a,a,a,B,C,B,B,C,C],[a,a,a,B,C,B,C,B,C],[a,a,a,a,B,C,B,C,B,C,B,C],[a,a,a,a,S,B,C,B,C,B,C,B,C]}"
      ]
     },
     "execution_count": 28,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":let SF UNION(i).(i:0..4|iterate(abl,i)[ {[S]} ])"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 29,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "$\\{[a,\\mathit{b},c]\\}$"
      ],
      "text/plain": [
       "{[a,b,c]}"
      ]
     },
     "execution_count": 29,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "SF ∩ seq(Σ)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 30,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Preference changed: DOT_DECOMPOSE_NODES = FALSE\n"
      ]
     },
     "execution_count": 30,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":pref DOT_DECOMPOSE_NODES=FALSE"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 31,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "image/svg+xml": [
       "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
       "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
       " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
       "<!-- Generated by graphviz version 2.44.1 (0)\n",
       " -->\n",
       "<!-- Title: state Pages: 1 -->\n",
       "<svg width=\"1547pt\" height=\"392pt\"\n",
       " viewBox=\"0.00 0.00 1546.50 392.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
       "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 388)\">\n",
       "<title>state</title>\n",
       "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-388 1542.5,-388 1542.5,4 -4,4\"/>\n",
       "<!-- [a,a,a,B,C,B,C,B,C] -->\n",
       "<g id=\"node1\" class=\"node\">\n",
       "<title>[a,a,a,B,C,B,C,B,C]</title>\n",
       "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"1202.5,-123 1051.5,-123 1051.5,-87 1202.5,-87 1202.5,-123\"/>\n",
       "<text text-anchor=\"middle\" x=\"1127\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\">[a,a,a,B,C,B,C,B,C]</text>\n",
       "</g>\n",
       "<!-- [a,a,a,B,C,B,B,C,C] -->\n",
       "<g id=\"node2\" class=\"node\">\n",
       "<title>[a,a,a,B,C,B,B,C,C]</title>\n",
       "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"1202.5,-36 1051.5,-36 1051.5,0 1202.5,0 1202.5,-36\"/>\n",
       "<text text-anchor=\"middle\" x=\"1127\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\">[a,a,a,B,C,B,B,C,C]</text>\n",
       "</g>\n",
       "<!-- [a,a,a,B,C,B,C,B,C]&#45;&gt;[a,a,a,B,C,B,B,C,C] -->\n",
       "<g id=\"edge1\" class=\"edge\">\n",
       "<title>[a,a,a,B,C,B,C,B,C]&#45;&gt;[a,a,a,B,C,B,B,C,C]</title>\n",
       "<path fill=\"none\" stroke=\"firebrick\" d=\"M1127,-86.8C1127,-75.16 1127,-59.55 1127,-46.24\"/>\n",
       "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"1130.5,-46.18 1127,-36.18 1123.5,-46.18 1130.5,-46.18\"/>\n",
       "<text text-anchor=\"middle\" x=\"1138\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\">abl</text>\n",
       "</g>\n",
       "<!-- [a,a,a,b,C,B,C,B,C] -->\n",
       "<g id=\"node3\" class=\"node\">\n",
       "<title>[a,a,a,b,C,B,C,B,C]</title>\n",
       "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"1369.5,-36 1220.5,-36 1220.5,0 1369.5,0 1369.5,-36\"/>\n",
       "<text text-anchor=\"middle\" x=\"1295\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\">[a,a,a,b,C,B,C,B,C]</text>\n",
       "</g>\n",
       "<!-- [a,a,a,B,C,B,C,B,C]&#45;&gt;[a,a,a,b,C,B,C,B,C] -->\n",
       "<g id=\"edge2\" class=\"edge\">\n",
       "<title>[a,a,a,B,C,B,C,B,C]&#45;&gt;[a,a,a,b,C,B,C,B,C]</title>\n",
       "<path fill=\"none\" stroke=\"firebrick\" d=\"M1161,-86.8C1187.27,-73.51 1223.8,-55.02 1252.09,-40.71\"/>\n",
       "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"1254,-43.67 1261.34,-36.03 1250.84,-37.42 1254,-43.67\"/>\n",
       "<text text-anchor=\"middle\" x=\"1233\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\">abl</text>\n",
       "</g>\n",
       "<!-- [a,a,a,B,B,C,C,B,C] -->\n",
       "<g id=\"node4\" class=\"node\">\n",
       "<title>[a,a,a,B,B,C,C,B,C]</title>\n",
       "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"1538.5,-36 1387.5,-36 1387.5,0 1538.5,0 1538.5,-36\"/>\n",
       "<text text-anchor=\"middle\" x=\"1463\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\">[a,a,a,B,B,C,C,B,C]</text>\n",
       "</g>\n",
       "<!-- [a,a,a,B,C,B,C,B,C]&#45;&gt;[a,a,a,B,B,C,C,B,C] -->\n",
       "<g id=\"edge3\" class=\"edge\">\n",
       "<title>[a,a,a,B,C,B,C,B,C]&#45;&gt;[a,a,a,B,B,C,C,B,C]</title>\n",
       "<path fill=\"none\" stroke=\"firebrick\" d=\"M1194.59,-86.9C1249.84,-72.92 1327.98,-53.16 1385.71,-38.55\"/>\n",
       "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"1386.68,-41.92 1395.52,-36.07 1384.96,-35.13 1386.68,-41.92\"/>\n",
       "<text text-anchor=\"middle\" x=\"1327\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\">abl</text>\n",
       "</g>\n",
       "<!-- [a,a,a,S,B,C,B,C,B,C] -->\n",
       "<g id=\"node5\" class=\"node\">\n",
       "<title>[a,a,a,S,B,C,B,C,B,C]</title>\n",
       "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"836,-123 672,-123 672,-87 836,-87 836,-123\"/>\n",
       "<text text-anchor=\"middle\" x=\"754\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\">[a,a,a,S,B,C,B,C,B,C]</text>\n",
       "</g>\n",
       "<!-- [a,a,a,a,S,B,C,B,C,B,C,B,C] -->\n",
       "<g id=\"node6\" class=\"node\">\n",
       "<title>[a,a,a,a,S,B,C,B,C,B,C,B,C]</title>\n",
       "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"638.5,-36 431.5,-36 431.5,0 638.5,0 638.5,-36\"/>\n",
       "<text text-anchor=\"middle\" x=\"535\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\">[a,a,a,a,S,B,C,B,C,B,C,B,C]</text>\n",
       "</g>\n",
       "<!-- [a,a,a,S,B,C,B,C,B,C]&#45;&gt;[a,a,a,a,S,B,C,B,C,B,C,B,C] -->\n",
       "<g id=\"edge4\" class=\"edge\">\n",
       "<title>[a,a,a,S,B,C,B,C,B,C]&#45;&gt;[a,a,a,a,S,B,C,B,C,B,C,B,C]</title>\n",
       "<path fill=\"none\" stroke=\"firebrick\" d=\"M709.95,-86.9C674.97,-73.33 625.94,-54.29 588.67,-39.83\"/>\n",
       "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"589.57,-36.43 578.98,-36.07 587.04,-42.95 589.57,-36.43\"/>\n",
       "<text text-anchor=\"middle\" x=\"669\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\">abl</text>\n",
       "</g>\n",
       "<!-- [a,a,a,a,B,C,B,C,B,C,B,C] -->\n",
       "<g id=\"node7\" class=\"node\">\n",
       "<title>[a,a,a,a,B,C,B,C,B,C,B,C]</title>\n",
       "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"851,-36 657,-36 657,0 851,0 851,-36\"/>\n",
       "<text text-anchor=\"middle\" x=\"754\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\">[a,a,a,a,B,C,B,C,B,C,B,C]</text>\n",
       "</g>\n",
       "<!-- [a,a,a,S,B,C,B,C,B,C]&#45;&gt;[a,a,a,a,B,C,B,C,B,C,B,C] -->\n",
       "<g id=\"edge5\" class=\"edge\">\n",
       "<title>[a,a,a,S,B,C,B,C,B,C]&#45;&gt;[a,a,a,a,B,C,B,C,B,C,B,C]</title>\n",
       "<path fill=\"none\" stroke=\"firebrick\" d=\"M754,-86.8C754,-75.16 754,-59.55 754,-46.24\"/>\n",
       "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"757.5,-46.18 754,-36.18 750.5,-46.18 757.5,-46.18\"/>\n",
       "<text text-anchor=\"middle\" x=\"765\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\">abl</text>\n",
       "</g>\n",
       "<!-- [a,a,a,S,B,B,C,C,B,C] -->\n",
       "<g id=\"node8\" class=\"node\">\n",
       "<title>[a,a,a,S,B,B,C,C,B,C]</title>\n",
       "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"413,-36 249,-36 249,0 413,0 413,-36\"/>\n",
       "<text text-anchor=\"middle\" x=\"331\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\">[a,a,a,S,B,B,C,C,B,C]</text>\n",
       "</g>\n",
       "<!-- [a,a,a,S,B,C,B,C,B,C]&#45;&gt;[a,a,a,S,B,B,C,C,B,C] -->\n",
       "<g id=\"edge6\" class=\"edge\">\n",
       "<title>[a,a,a,S,B,C,B,C,B,C]&#45;&gt;[a,a,a,S,B,B,C,C,B,C]</title>\n",
       "<path fill=\"none\" stroke=\"firebrick\" d=\"M671.94,-87.51C600.55,-73.16 497.18,-52.39 423,-37.49\"/>\n",
       "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"423.69,-34.05 413.19,-35.52 422.31,-40.92 423.69,-34.05\"/>\n",
       "<text text-anchor=\"middle\" x=\"579\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\">abl</text>\n",
       "</g>\n",
       "<!-- [a,a,a,S,B,C,B,B,C,C] -->\n",
       "<g id=\"node9\" class=\"node\">\n",
       "<title>[a,a,a,S,B,C,B,B,C,C]</title>\n",
       "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"1033,-36 869,-36 869,0 1033,0 1033,-36\"/>\n",
       "<text text-anchor=\"middle\" x=\"951\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\">[a,a,a,S,B,C,B,B,C,C]</text>\n",
       "</g>\n",
       "<!-- [a,a,a,S,B,C,B,C,B,C]&#45;&gt;[a,a,a,S,B,C,B,B,C,C] -->\n",
       "<g id=\"edge7\" class=\"edge\">\n",
       "<title>[a,a,a,S,B,C,B,C,B,C]&#45;&gt;[a,a,a,S,B,C,B,B,C,C]</title>\n",
       "<path fill=\"none\" stroke=\"firebrick\" d=\"M793.87,-86.8C825.08,-73.33 868.63,-54.54 901.98,-40.15\"/>\n",
       "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"903.73,-43.21 911.53,-36.03 900.96,-36.78 903.73,-43.21\"/>\n",
       "<text text-anchor=\"middle\" x=\"876\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\">abl</text>\n",
       "</g>\n",
       "<!-- [a,a,S,B,B,C,C] -->\n",
       "<g id=\"node10\" class=\"node\">\n",
       "<title>[a,a,S,B,B,C,C]</title>\n",
       "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"1027,-123 905,-123 905,-87 1027,-87 1027,-123\"/>\n",
       "<text text-anchor=\"middle\" x=\"966\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\">[a,a,S,B,B,C,C]</text>\n",
       "</g>\n",
       "<!-- [a,a,S,B,B,C,C]&#45;&gt;[a,a,a,B,C,B,B,C,C] -->\n",
       "<g id=\"edge8\" class=\"edge\">\n",
       "<title>[a,a,S,B,B,C,C]&#45;&gt;[a,a,a,B,C,B,B,C,C]</title>\n",
       "<path fill=\"none\" stroke=\"firebrick\" d=\"M998.58,-86.8C1023.76,-73.51 1058.77,-55.02 1085.88,-40.71\"/>\n",
       "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"1087.53,-43.79 1094.74,-36.03 1084.27,-37.6 1087.53,-43.79\"/>\n",
       "<text text-anchor=\"middle\" x=\"1068\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\">abl</text>\n",
       "</g>\n",
       "<!-- [a,a,S,B,B,C,C]&#45;&gt;[a,a,a,S,B,C,B,B,C,C] -->\n",
       "<g id=\"edge9\" class=\"edge\">\n",
       "<title>[a,a,S,B,B,C,C]&#45;&gt;[a,a,a,S,B,C,B,B,C,C]</title>\n",
       "<path fill=\"none\" stroke=\"firebrick\" d=\"M962.96,-86.8C960.91,-75.16 958.16,-59.55 955.81,-46.24\"/>\n",
       "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"959.22,-45.41 954.03,-36.18 952.32,-46.63 959.22,-45.41\"/>\n",
       "<text text-anchor=\"middle\" x=\"971\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\">abl</text>\n",
       "</g>\n",
       "<!-- [a,a,S,B,C,B,C] -->\n",
       "<g id=\"node11\" class=\"node\">\n",
       "<title>[a,a,S,B,C,B,C]</title>\n",
       "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"1027,-210 905,-210 905,-174 1027,-174 1027,-210\"/>\n",
       "<text text-anchor=\"middle\" x=\"966\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\">[a,a,S,B,C,B,C]</text>\n",
       "</g>\n",
       "<!-- [a,a,S,B,C,B,C]&#45;&gt;[a,a,a,B,C,B,C,B,C] -->\n",
       "<g id=\"edge10\" class=\"edge\">\n",
       "<title>[a,a,S,B,C,B,C]&#45;&gt;[a,a,a,B,C,B,C,B,C]</title>\n",
       "<path fill=\"none\" stroke=\"firebrick\" d=\"M998.58,-173.8C1023.76,-160.51 1058.77,-142.02 1085.88,-127.71\"/>\n",
       "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"1087.53,-130.79 1094.74,-123.03 1084.27,-124.6 1087.53,-130.79\"/>\n",
       "<text text-anchor=\"middle\" x=\"1068\" y=\"-144.8\" font-family=\"Times,serif\" font-size=\"14.00\">abl</text>\n",
       "</g>\n",
       "<!-- [a,a,S,B,C,B,C]&#45;&gt;[a,a,a,S,B,C,B,C,B,C] -->\n",
       "<g id=\"edge11\" class=\"edge\">\n",
       "<title>[a,a,S,B,C,B,C]&#45;&gt;[a,a,a,S,B,C,B,C,B,C]</title>\n",
       "<path fill=\"none\" stroke=\"firebrick\" d=\"M923.35,-173.9C889.5,-160.33 842.03,-141.29 805.96,-126.83\"/>\n",
       "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"807.16,-123.54 796.58,-123.07 804.56,-130.04 807.16,-123.54\"/>\n",
       "<text text-anchor=\"middle\" x=\"884\" y=\"-144.8\" font-family=\"Times,serif\" font-size=\"14.00\">abl</text>\n",
       "</g>\n",
       "<!-- [a,a,S,B,C,B,C]&#45;&gt;[a,a,S,B,B,C,C] -->\n",
       "<g id=\"edge12\" class=\"edge\">\n",
       "<title>[a,a,S,B,C,B,C]&#45;&gt;[a,a,S,B,B,C,C]</title>\n",
       "<path fill=\"none\" stroke=\"firebrick\" d=\"M966,-173.8C966,-162.16 966,-146.55 966,-133.24\"/>\n",
       "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"969.5,-133.18 966,-123.18 962.5,-133.18 969.5,-133.18\"/>\n",
       "<text text-anchor=\"middle\" x=\"977\" y=\"-144.8\" font-family=\"Times,serif\" font-size=\"14.00\">abl</text>\n",
       "</g>\n",
       "<!-- [a,a,B,B,C,C] -->\n",
       "<g id=\"node12\" class=\"node\">\n",
       "<title>[a,a,B,B,C,C]</title>\n",
       "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"108,-123 0,-123 0,-87 108,-87 108,-123\"/>\n",
       "<text text-anchor=\"middle\" x=\"54\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\">[a,a,B,B,C,C]</text>\n",
       "</g>\n",
       "<!-- [a,a,b,B,C,C] -->\n",
       "<g id=\"node13\" class=\"node\">\n",
       "<title>[a,a,b,B,C,C]</title>\n",
       "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"108.5,-36 1.5,-36 1.5,0 108.5,0 108.5,-36\"/>\n",
       "<text text-anchor=\"middle\" x=\"55\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\">[a,a,b,B,C,C]</text>\n",
       "</g>\n",
       "<!-- [a,a,B,B,C,C]&#45;&gt;[a,a,b,B,C,C] -->\n",
       "<g id=\"edge13\" class=\"edge\">\n",
       "<title>[a,a,B,B,C,C]&#45;&gt;[a,a,b,B,C,C]</title>\n",
       "<path fill=\"none\" stroke=\"firebrick\" d=\"M54.2,-86.8C54.34,-75.16 54.52,-59.55 54.68,-46.24\"/>\n",
       "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"58.18,-46.22 54.8,-36.18 51.18,-46.13 58.18,-46.22\"/>\n",
       "<text text-anchor=\"middle\" x=\"66\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\">abl</text>\n",
       "</g>\n",
       "<!-- [a,a,B,C,B,C] -->\n",
       "<g id=\"node14\" class=\"node\">\n",
       "<title>[a,a,B,C,B,C]</title>\n",
       "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"234,-210 126,-210 126,-174 234,-174 234,-210\"/>\n",
       "<text text-anchor=\"middle\" x=\"180\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\">[a,a,B,C,B,C]</text>\n",
       "</g>\n",
       "<!-- [a,a,B,C,B,C]&#45;&gt;[a,a,B,B,C,C] -->\n",
       "<g id=\"edge14\" class=\"edge\">\n",
       "<title>[a,a,B,C,B,C]&#45;&gt;[a,a,B,B,C,C]</title>\n",
       "<path fill=\"none\" stroke=\"firebrick\" d=\"M154.5,-173.8C135.29,-160.84 108.76,-142.94 87.78,-128.79\"/>\n",
       "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"89.71,-125.87 79.46,-123.18 85.79,-131.67 89.71,-125.87\"/>\n",
       "<text text-anchor=\"middle\" x=\"136\" y=\"-144.8\" font-family=\"Times,serif\" font-size=\"14.00\">abl</text>\n",
       "</g>\n",
       "<!-- [a,a,b,C,B,C] -->\n",
       "<g id=\"node15\" class=\"node\">\n",
       "<title>[a,a,b,C,B,C]</title>\n",
       "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"233.5,-123 126.5,-123 126.5,-87 233.5,-87 233.5,-123\"/>\n",
       "<text text-anchor=\"middle\" x=\"180\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\">[a,a,b,C,B,C]</text>\n",
       "</g>\n",
       "<!-- [a,a,B,C,B,C]&#45;&gt;[a,a,b,C,B,C] -->\n",
       "<g id=\"edge15\" class=\"edge\">\n",
       "<title>[a,a,B,C,B,C]&#45;&gt;[a,a,b,C,B,C]</title>\n",
       "<path fill=\"none\" stroke=\"firebrick\" d=\"M180,-173.8C180,-162.16 180,-146.55 180,-133.24\"/>\n",
       "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"183.5,-133.18 180,-123.18 176.5,-133.18 183.5,-133.18\"/>\n",
       "<text text-anchor=\"middle\" x=\"191\" y=\"-144.8\" font-family=\"Times,serif\" font-size=\"14.00\">abl</text>\n",
       "</g>\n",
       "<!-- [a,a,b,C,B,C]&#45;&gt;[a,a,b,B,C,C] -->\n",
       "<g id=\"edge16\" class=\"edge\">\n",
       "<title>[a,a,b,C,B,C]&#45;&gt;[a,a,b,B,C,C]</title>\n",
       "<path fill=\"none\" stroke=\"firebrick\" d=\"M154.7,-86.8C135.73,-73.9 109.56,-56.1 88.79,-41.98\"/>\n",
       "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"90.5,-38.9 80.26,-36.18 86.56,-44.69 90.5,-38.9\"/>\n",
       "<text text-anchor=\"middle\" x=\"136\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\">abl</text>\n",
       "</g>\n",
       "<!-- [a,a,b,c,B,C] -->\n",
       "<g id=\"node16\" class=\"node\">\n",
       "<title>[a,a,b,c,B,C]</title>\n",
       "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"231,-36 127,-36 127,0 231,0 231,-36\"/>\n",
       "<text text-anchor=\"middle\" x=\"179\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\">[a,a,b,c,B,C]</text>\n",
       "</g>\n",
       "<!-- [a,a,b,C,B,C]&#45;&gt;[a,a,b,c,B,C] -->\n",
       "<g id=\"edge17\" class=\"edge\">\n",
       "<title>[a,a,b,C,B,C]&#45;&gt;[a,a,b,c,B,C]</title>\n",
       "<path fill=\"none\" stroke=\"firebrick\" d=\"M179.8,-86.8C179.66,-75.16 179.48,-59.55 179.32,-46.24\"/>\n",
       "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"182.82,-46.13 179.2,-36.18 175.82,-46.22 182.82,-46.13\"/>\n",
       "<text text-anchor=\"middle\" x=\"191\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\">abl</text>\n",
       "</g>\n",
       "<!-- [a,B,C] -->\n",
       "<g id=\"node17\" class=\"node\">\n",
       "<title>[a,B,C]</title>\n",
       "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"1140.5,-297 1075.5,-297 1075.5,-261 1140.5,-261 1140.5,-297\"/>\n",
       "<text text-anchor=\"middle\" x=\"1108\" y=\"-275.3\" font-family=\"Times,serif\" font-size=\"14.00\">[a,B,C]</text>\n",
       "</g>\n",
       "<!-- [a,b,C] -->\n",
       "<g id=\"node18\" class=\"node\">\n",
       "<title>[a,b,C]</title>\n",
       "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"1264,-210 1200,-210 1200,-174 1264,-174 1264,-210\"/>\n",
       "<text text-anchor=\"middle\" x=\"1232\" y=\"-188.3\" font-family=\"Times,serif\" font-size=\"14.00\">[a,b,C]</text>\n",
       "</g>\n",
       "<!-- [a,B,C]&#45;&gt;[a,b,C] -->\n",
       "<g id=\"edge18\" class=\"edge\">\n",
       "<title>[a,B,C]&#45;&gt;[a,b,C]</title>\n",
       "<path fill=\"none\" stroke=\"firebrick\" d=\"M1133.09,-260.8C1151.92,-247.9 1177.88,-230.1 1198.48,-215.98\"/>\n",
       "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"1200.67,-218.72 1206.94,-210.18 1196.72,-212.94 1200.67,-218.72\"/>\n",
       "<text text-anchor=\"middle\" x=\"1189\" y=\"-231.8\" font-family=\"Times,serif\" font-size=\"14.00\">abl</text>\n",
       "</g>\n",
       "<!-- [a,b,c] -->\n",
       "<g id=\"node20\" class=\"node\">\n",
       "<title>[a,b,c]</title>\n",
       "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"1281.5,-123 1220.5,-123 1220.5,-87 1281.5,-87 1281.5,-123\"/>\n",
       "<text text-anchor=\"middle\" x=\"1251\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\">[a,b,c]</text>\n",
       "</g>\n",
       "<!-- [a,b,C]&#45;&gt;[a,b,c] -->\n",
       "<g id=\"edge21\" class=\"edge\">\n",
       "<title>[a,b,C]&#45;&gt;[a,b,c]</title>\n",
       "<path fill=\"none\" stroke=\"firebrick\" d=\"M1235.84,-173.8C1238.45,-162.16 1241.94,-146.55 1244.91,-133.24\"/>\n",
       "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"1248.39,-133.7 1247.16,-123.18 1241.56,-132.17 1248.39,-133.7\"/>\n",
       "<text text-anchor=\"middle\" x=\"1254\" y=\"-144.8\" font-family=\"Times,serif\" font-size=\"14.00\">abl</text>\n",
       "</g>\n",
       "<!-- [a,S,B,C] -->\n",
       "<g id=\"node19\" class=\"node\">\n",
       "<title>[a,S,B,C]</title>\n",
       "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"1005.5,-297 926.5,-297 926.5,-261 1005.5,-261 1005.5,-297\"/>\n",
       "<text text-anchor=\"middle\" x=\"966\" y=\"-275.3\" font-family=\"Times,serif\" font-size=\"14.00\">[a,S,B,C]</text>\n",
       "</g>\n",
       "<!-- [a,S,B,C]&#45;&gt;[a,a,S,B,C,B,C] -->\n",
       "<g id=\"edge19\" class=\"edge\">\n",
       "<title>[a,S,B,C]&#45;&gt;[a,a,S,B,C,B,C]</title>\n",
       "<path fill=\"none\" stroke=\"firebrick\" d=\"M966,-260.8C966,-249.16 966,-233.55 966,-220.24\"/>\n",
       "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"969.5,-220.18 966,-210.18 962.5,-220.18 969.5,-220.18\"/>\n",
       "<text text-anchor=\"middle\" x=\"977\" y=\"-231.8\" font-family=\"Times,serif\" font-size=\"14.00\">abl</text>\n",
       "</g>\n",
       "<!-- [a,S,B,C]&#45;&gt;[a,a,B,C,B,C] -->\n",
       "<g id=\"edge20\" class=\"edge\">\n",
       "<title>[a,S,B,C]&#45;&gt;[a,a,B,C,B,C]</title>\n",
       "<path fill=\"none\" stroke=\"firebrick\" d=\"M926.48,-273.73C799.46,-259.99 400.78,-216.88 244.12,-199.93\"/>\n",
       "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"244.47,-196.45 234.15,-198.86 243.72,-203.41 244.47,-196.45\"/>\n",
       "<text text-anchor=\"middle\" x=\"632\" y=\"-231.8\" font-family=\"Times,serif\" font-size=\"14.00\">abl</text>\n",
       "</g>\n",
       "<!-- [S] -->\n",
       "<g id=\"node21\" class=\"node\">\n",
       "<title>[S]</title>\n",
       "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"1037,-384 983,-384 983,-348 1037,-348 1037,-384\"/>\n",
       "<text text-anchor=\"middle\" x=\"1010\" y=\"-362.3\" font-family=\"Times,serif\" font-size=\"14.00\">[S]</text>\n",
       "</g>\n",
       "<!-- [S]&#45;&gt;[a,B,C] -->\n",
       "<g id=\"edge22\" class=\"edge\">\n",
       "<title>[S]&#45;&gt;[a,B,C]</title>\n",
       "<path fill=\"none\" stroke=\"firebrick\" d=\"M1029.83,-347.8C1044.44,-335.13 1064.5,-317.73 1080.63,-303.74\"/>\n",
       "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"1082.94,-306.37 1088.2,-297.18 1078.35,-301.08 1082.94,-306.37\"/>\n",
       "<text text-anchor=\"middle\" x=\"1076\" y=\"-318.8\" font-family=\"Times,serif\" font-size=\"14.00\">abl</text>\n",
       "</g>\n",
       "<!-- [S]&#45;&gt;[a,S,B,C] -->\n",
       "<g id=\"edge23\" class=\"edge\">\n",
       "<title>[S]&#45;&gt;[a,S,B,C]</title>\n",
       "<path fill=\"none\" stroke=\"firebrick\" d=\"M1001.1,-347.8C994.89,-335.82 986.51,-319.62 979.49,-306.06\"/>\n",
       "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"982.6,-304.45 974.89,-297.18 976.38,-307.67 982.6,-304.45\"/>\n",
       "<text text-anchor=\"middle\" x=\"1002\" y=\"-318.8\" font-family=\"Times,serif\" font-size=\"14.00\">abl</text>\n",
       "</g>\n",
       "</g>\n",
       "</svg>"
      ],
      "text/plain": [
       "<Dot visualization: expr_as_graph [SFSF={[S],[a,b,c],[a,b,C],[a,S,B,C],[a,B,C],[a,a,b,c,B,C],[a,a,b,C,B,C],[a,a,b,B,C,C],[a,a,B,C,B,C],[a,a,B,B,C,C],[a,a,S,B,C,B,C],[a,a,S,B,B,C,C],[a,a,a,S,B,C,B,B,C,C],[a,a,a,S,B,B,C,C,B,C],[a,a,a,S,B,C,B,C,B,C],[a,a,a,B,B,C,C,B,C],[a,a,a,b,C,B,C,B,C],[a,a,a,B,C,B,B,C,C],[a,a,a,B,C,B,C,B,C],[a,a,a,a,B,C,B,C,B,C,B,C],[a,a,a,a,S,B,C,B,C,B,C,B,C]}(\"abl\",SF<|abl|>SF)]>"
      ]
     },
     "execution_count": 31,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":dot expr_as_graph (\"abl\",SF <| abl |> SF)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 32,
   "metadata": {},
   "outputs": [],
   "source": [
    ":unlet SF"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Bis zur Ebene 8 sieht der Graph der Ableitungsrelation so aus:\n",
    "\n",
    "<img src=\"img/GrammatikUnicode2.svg\" width=\"700\">"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Chomsky-Hierarchie\n",
    "\n",
    "Die Chomsky-Hierarchie klassifiziert Grammatiken nach folgenden Kriterien:\n",
    "\n",
    "Sei $G = (\\Sigma , N, S, P)$ eine Grammatik.\n",
    "* $G$ ist eine __Typ-0-Grammatik__, falls $P$ keinerlei\n",
    "  Einschränkungen unterliegt.\n",
    "  \n",
    "* $G$ ist eine __Typ-1-Grammatik__ (bzw. __kontextsensitiv__ bzw. _nichtverkürzend_ oder __monoton__), falls für alle Regeln $p \\rightarrow q$ in\n",
    "  $P$ gilt: $|p| \\leq |q|$.\n",
    "  \n",
    "* Eine Typ-1-Grammatik $G$ ist __vom Typ 2__ (bzw. __kontextfrei__), falls für alle Regeln $p \\rightarrow q$ in $P$ gilt: $p \\in N$.\n",
    "  \n",
    "* Eine Typ-2-Grammatik $G$ ist __vom Typ 3__ (bzw. __regulär__ bzw. __rechtslinear__), falls für\n",
    "  alle Regeln $p \\rightarrow q$ in $P$ gilt: $p \\in N$ und $q \\in \\Sigma \\cup \\Sigma N$.\n",
    "\n",
    "Eine Sprache $A \\subseteq \\Sigma^*$ ist genau dann vom Typ $i \\in\n",
    "  \\{0,1,2,3\\}$, wenn es eine Typ-$i$-Grammatik $G$ gibt mit $L(G) = A$."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 33,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "$\\{([a,B]\\mapsto [a,b]),([b,B]\\mapsto [b,b]),([b,C]\\mapsto [b,c]),([c,C]\\mapsto [c,c]),([S]\\mapsto [a,\\mathit{S},\\mathit{B},C]),([S]\\mapsto [a,\\mathit{B},C]),([C,B]\\mapsto [B,C])\\}$"
      ],
      "text/plain": [
       "{([a,B]↦[a,b]),([b,B]↦[b,b]),([b,C]↦[b,c]),([c,C]↦[c,c]),([S]↦[a,S,B,C]),([S]↦[a,B,C]),([C,B]↦[B,C])}"
      ]
     },
     "execution_count": 33,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "P"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Jede Grammatik ist vom Typ-0.\n",
    "Die Grammatik $G_2$ ist nicht-verkürzend, also vom Typ 1:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 34,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "$\\mathit{TRUE}$"
      ],
      "text/plain": [
       "TRUE"
      ]
     },
     "execution_count": 34,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "∀(p,q).( p↦q ∈ P ⇒ size(p) ≤ size(q))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 35,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "$\\{([a,B]\\mapsto [a,b]),([b,B]\\mapsto [b,b]),([b,C]\\mapsto [b,c]),([c,C]\\mapsto [c,c]),([S]\\mapsto [a,\\mathit{S},\\mathit{B},C]),([S]\\mapsto [a,\\mathit{B},C]),([C,B]\\mapsto [B,C])\\}$"
      ],
      "text/plain": [
       "{([a,B]↦[a,b]),([b,B]↦[b,b]),([b,C]↦[b,c]),([c,C]↦[c,c]),([S]↦[a,S,B,C]),([S]↦[a,B,C]),([C,B]↦[B,C])}"
      ]
     },
     "execution_count": 35,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "P"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Die Grammatik $G_2$ ist aber nicht vom Typ 2:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 36,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "$\\mathit{FALSE}$"
      ],
      "text/plain": [
       "FALSE"
      ]
     },
     "execution_count": 36,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "∀(p,q).( p↦q ∈ P ⇒ size(p)=1 & p∈seq(N))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Anmerkung: im Skript wird nicht zwischen einem Nicht-Terminal Symbol und einer Folge der Länge 1 bestehend aus einem Nicht-Terminal unterschieden.\n",
    "Deshalb steht im Skript $p\\in N$. Im Notebook sind $p$ und die Folge bestehend aus einem $p$ (geschrieben als [p]) von einem unterschiedlichen Typ. Die wortwörtliche Übersetzung von $p\\in N$ führt zu einem Typfehler."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 37,
   "metadata": {},
   "outputs": [
    {
     "ename": "CommandExecutionException",
     "evalue": ":eval: Computation not completed: Type mismatch: Expected POW(seq(ΣN)), but was POW(ΣN) in 'N'",
     "output_type": "error",
     "traceback": [
      "\u001b[1m\u001b[31m:eval: Computation not completed: Type mismatch: Expected POW(seq(ΣN)), but was POW(ΣN) in 'N'\u001b[0m"
     ]
    }
   ],
   "source": [
    "∀(p,q).( p↦q ∈ P ⇒ p ∈ N)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Die Grammatik $G_2$ ist also vom Typ 1 aber nicht vom Typ 2 oder 3.\n",
    "Wie sieht es mit der Grammatik $G_1$ aus?\n",
    "Diese erfüllt die Typ-2 Bedingung:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 38,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "$\\{([S]\\mapsto []),([S]\\mapsto [a,\\mathit{S},b])\\}$"
      ],
      "text/plain": [
       "{([S]↦[]),([S]↦[a,S,b])}"
      ]
     },
     "execution_count": 38,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":let P1 { [S] ↦ [], [S] ↦ [a,S,b] }"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 39,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "$\\mathit{TRUE}$\n",
       "\n",
       "**Solution:**\n",
       "* $\\mathit{P1} = \\{([S]\\mapsto []),([S]\\mapsto [a,\\mathit{S},b])\\}$"
      ],
      "text/plain": [
       "TRUE\n",
       "\n",
       "Solution:\n",
       "\tP1 = {([S]↦[]),([S]↦[a,S,b])}"
      ]
     },
     "execution_count": 39,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "∀(p,q).( p↦q ∈ P1 ⇒ size(p)=1 & p∈seq(N))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Die Grammatik $G_1$ erfüllt aber nicht die Typ 1 Bedingung, da die erste Regel verkürzend ist:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 40,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "$\\mathit{FALSE}$"
      ],
      "text/plain": [
       "FALSE"
      ]
     },
     "execution_count": 40,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "∀(p,q).( p↦q ∈ P1 ⇒ size(p) ≤ size(q))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 41,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "$\\mathit{TRUE}$\n",
       "\n",
       "**Solution:**\n",
       "* $\\mathit{p} = [S]$\n",
       "* $\\mathit{q} = []$\n",
       "* $\\mathit{P1} = \\{([S]\\mapsto []),([S]\\mapsto [a,\\mathit{S},b])\\}$"
      ],
      "text/plain": [
       "TRUE\n",
       "\n",
       "Solution:\n",
       "\tp = [S]\n",
       "\tq = []\n",
       "\tP1 = {([S]↦[]),([S]↦[a,S,b])}"
      ]
     },
     "execution_count": 41,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "p↦q ∈ P1 ∧ size(p) > size(q)  /* Gegenbeispiel */"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Die Grammatik $G_1$ ist also vom Typ-0.\n",
    "Wir werden aber in der nächsten Woche eine Sonderregelung für das leere Wort erlauben, damit auch Grammatiken vom Typ 1,2 oder 3 das leere Wort in ihrer Sprache generieren können."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Chomsky-Hierarchie\n",
    "\n",
    "Die __Chomsky-Hierarchie__ besteht aus den vier Sprachklassen:\n",
    "* $\\mathfrak{L}_i = \\{L(G) \\Longleftrightarrow \\mbox{$G$ ist Typ-$i$-Grammatik} \\}$,\n",
    "wobei $i \\in \\{0,1,2,3\\}$.\n",
    "\n",
    "\n",
    "Übliche Bezeichnungen:\n",
    "* $\\mathfrak{L}_0$ ist die Klasse aller Sprachen, die durch eine\n",
    "  Grammatik erzeugt werden können;\n",
    "* $\\mathfrak{L}_1 = CS$ ist die __Klasse der kontextsensitiven Sprachen__;\n",
    "* $\\mathfrak{L}_2 = CF$ ist die __Klasse der kontextfreien Sprachen__;\n",
    "* $\\mathfrak{L}_3 = REG$ ist die __Klasse der regulären Sprachen__.\n",
    " \n",
    "\n",
    "* $REG \\subseteq CF \\subseteq CS \\subseteq \\mathfrak{L}_0.$"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 42,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Loaded machine: Chomsky"
      ]
     },
     "execution_count": 42,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "::load\n",
    "MACHINE Chomsky\n",
    "SETS ΣN = {a, b, c, S, A, B, C}\n",
    "CONSTANTS Σ, N, P0, P1, P2, P3, P4, Grammatiken\n",
    "PROPERTIES\n",
    "   Σ = {a, b, c} ∧\n",
    "   N = {S, A, B, C} ∧\n",
    "   Σ ∩ N = {} ∧\n",
    "   Σ ∪ N = ΣN ∧\n",
    "   //L0 = {x∈{a, b}^* | x enthält gleich viele as und bs}\n",
    "   //Ohne Sonderrregelung für lambda ist L0 von Typ 0.\n",
    "   P0 = {([S] ↦ [a, b]), ([S] ↦ [S, S]), ([S] ↦ []), ([a, b] ↦ [b, a]), ([b, a] ↦ [a, b])} ∧\n",
    "   //L1 = {a^mb^mc^m | m≥1}\n",
    "   P1 = {([S] ↦ [S, S]), ([S] ↦ [A, B, C]), ([B, A] ↦ [A, B]), ([C, A] ↦ [A, C]), ([C, B] ↦ [B, C]),\n",
    "           ([A] ↦ [a]), ([a, B] ↦ [a, b]), ([b, B] ↦ [b, b]), ([b, C] ↦ [b, c]), ([c, C] ↦ [c, c])} ∧\n",
    "   //L2 = {x∈{a, b}^+ | x enthält gleich viele as und bs}\n",
    "   P2 = {([S] ↦ [A, B]), ([S] ↦ [B, A]),\n",
    "           ([A] ↦ [A, A, B]), ([A] ↦ [A, B, A]), ([A] ↦ [B, A, A]), ([A] ↦ [a]),\n",
    "           ([B] ↦ [B, B, A]), ([B] ↦ [B, A, B]), ([B] ↦ [A, B, B]), ([B] ↦ [b])} ∧\n",
    "   //L3 = L4 = {a, b, c}\n",
    "   P3 = {([S] ↦ [a]), ([S] ↦ [b]), ([S] ↦ [c])} ∧\n",
    "   P4 = {([S] ↦ [A, A]), ([A, A] ↦ [a]), ([S] ↦ [b]), ([S] ↦ [c])} ∧\n",
    "   Grammatiken = [P0, P1, P2, P3, P4]\n",
    "   \n",
    "DEFINITIONS\n",
    " SET_PREF_PP_SEQUENCES == TRUE;\n",
    " L0(R) == TRUE; //Jede Grammatik ist vom Typ 0\n",
    " L1(R) == IF ∀(p,q).( p↦q ∈ R ⇒ size(p) ≤ size(q)) THEN L0(R) ELSE FALSE END;\n",
    " L2(R) == IF ∀(p,q).( p↦q ∈ R ⇒ size(p)=1 & p∈seq(N)) THEN L1(R) ELSE FALSE END;\n",
    " L3(R) == IF ∀(p,q).( p↦q ∈ R ⇒ size(q)>0 & size(q) ≤ 2 & first(q)∈Σ & (size(q)≤1 or first(tail(q))∈N)) THEN L2(R) ELSE FALSE END;\n",
    " \n",
    " \"LibraryStrings.def\";\n",
    " ANIMATION_FUNCTION_DEFAULT == {(0,0,\"P\"), (1,0,\"P0\"), (2,0,\"P1\"), (3,0,\"P2\"), (4,0,\"P3\"), (5,0,\"P4\")};\n",
    " ANIMATION_FUNCTION1 == {c,r,i| r=1 ∧ c∈dom(Grammatiken) ∧ i=TO_STRING(L0(Grammatiken(c)))} ∪ {(0,1,\"L0(P)\")};\n",
    " ANIMATION_FUNCTION2 == {c,r,i| r=2 ∧ c∈dom(Grammatiken) ∧ i=TO_STRING(L1(Grammatiken(c)))} ∪ {(0,2,\"L1(P)\")};\n",
    " ANIMATION_FUNCTION3 == {c,r,i| r=3 ∧ c∈dom(Grammatiken) ∧ i=TO_STRING(L2(Grammatiken(c)))} ∪ {(0,3,\"L2(P)\")};\n",
    " ANIMATION_FUNCTION4 == {c,r,i| r=4 ∧ c∈dom(Grammatiken) ∧ i=TO_STRING(L3(Grammatiken(c)))} ∪ {(0,4,\"L3(P)\")};\n",
    "END"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 43,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Machine constants set up using operation 0: $setup_constants()"
      ]
     },
     "execution_count": 43,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":constants"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 44,
   "metadata": {
    "scrolled": true
   },
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Machine initialised using operation 1: $initialise_machine()"
      ]
     },
     "execution_count": 44,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":init"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 45,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "<table style=\"font-family:monospace\"><tbody>\n",
       "<tr>\n",
       "<td style=\"padding:10px\">P</td>\n",
       "<td style=\"padding:10px\">L0(P)</td>\n",
       "<td style=\"padding:10px\">L1(P)</td>\n",
       "<td style=\"padding:10px\">L2(P)</td>\n",
       "<td style=\"padding:10px\">L3(P)</td>\n",
       "</tr>\n",
       "<tr>\n",
       "<td style=\"padding:10px\">P0</td>\n",
       "<td style=\"padding:10px\">TRUE</td>\n",
       "<td style=\"padding:10px\">FALSE</td>\n",
       "<td style=\"padding:10px\">FALSE</td>\n",
       "<td style=\"padding:10px\">FALSE</td>\n",
       "</tr>\n",
       "<tr>\n",
       "<td style=\"padding:10px\">P1</td>\n",
       "<td style=\"padding:10px\">TRUE</td>\n",
       "<td style=\"padding:10px\">TRUE</td>\n",
       "<td style=\"padding:10px\">FALSE</td>\n",
       "<td style=\"padding:10px\">FALSE</td>\n",
       "</tr>\n",
       "<tr>\n",
       "<td style=\"padding:10px\">P2</td>\n",
       "<td style=\"padding:10px\">TRUE</td>\n",
       "<td style=\"padding:10px\">TRUE</td>\n",
       "<td style=\"padding:10px\">TRUE</td>\n",
       "<td style=\"padding:10px\">FALSE</td>\n",
       "</tr>\n",
       "<tr>\n",
       "<td style=\"padding:10px\">P3</td>\n",
       "<td style=\"padding:10px\">TRUE</td>\n",
       "<td style=\"padding:10px\">TRUE</td>\n",
       "<td style=\"padding:10px\">TRUE</td>\n",
       "<td style=\"padding:10px\">TRUE</td>\n",
       "</tr>\n",
       "<tr>\n",
       "<td style=\"padding:10px\">P4</td>\n",
       "<td style=\"padding:10px\">TRUE</td>\n",
       "<td style=\"padding:10px\">FALSE</td>\n",
       "<td style=\"padding:10px\">FALSE</td>\n",
       "<td style=\"padding:10px\">FALSE</td>\n",
       "</tr>\n",
       "</tbody></table>"
      ],
      "text/plain": [
       "<Animation function visualisation>"
      ]
     },
     "execution_count": 45,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":show"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Die obige Tabelle zeigt, in welche Sprachklasse die entsprechenden Grammatiken fallen. Dabei ist zu beachten, dass L3 = L4 ist, aber P3 und P4 unterschiedliche Typen haben. Die Sprache fällt allerdings immer in die größte Spracheklasse zu der es eine Grammatik gibt, die diese Sprache erzeugt. Also gilt $L4 ∈ \\mathfrak{L}_3 = REG$. Daher reicht die Angabe einer Grammatik nicht aus, um zu zeigen, dass eine Sprache höchstens in einer der Klassen liegt. Um dies zu zeigen, gibt es verschiedene Methoden, wie z.B. das Pumping-Lemma oder die Myhill-Nerode Relation."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": []
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "ProB 2",
   "language": "prob",
   "name": "prob2"
  },
  "language_info": {
   "codemirror_mode": "prob2_jupyter_repl",
   "file_extension": ".prob",
   "mimetype": "text/x-prob2-jupyter-repl",
   "name": "prob"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 2
}