diff --git a/info4/kapitel-2/Minimalautomat.ipynb b/info4/kapitel-2/Minimalautomat.ipynb index 0ad874e6a896220ff76f517533c56c651912ae52..0f0f11921b6cbf4244b52fd581f7a3546bdd4fb1 100644 --- a/info4/kapitel-2/Minimalautomat.ipynb +++ b/info4/kapitel-2/Minimalautomat.ipynb @@ -6,6 +6,7 @@ "source": [ "## Algorithmus Minimalautomat\n", "\n", + "Dieses Notebook begleitet die Vorlesung zur Myhill-Nerode Äquivalenzrelation und dem Minimalautomaten.\n", "\n", "Hier ist der Beispiel DFA aus den Folien zur Illustration der Konstruktion des Minimalautomaten.\n" ] @@ -1246,9 +1247,228 @@ "Anmerkung: wenn man oben zum Beispiel $F = \\{z2\\}$ setzt kommt ein anderes Ergebnis heraus." ] }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Das sind die Zustände die fusioniert werden können:" + ] + }, + { + "cell_type": "code", + "execution_count": 16, + "metadata": {}, + "outputs": [ + { + "data": { + "text/markdown": [ + "$\\{(\\mathit{z1}\\mapsto \\mathit{z2}),(\\mathit{z2}\\mapsto \\mathit{z1}),(\\mathit{z3}\\mapsto \\mathit{z4}),(\\mathit{z4}\\mapsto \\mathit{z3})\\}$" + ], + "text/plain": [ + "{(z1↦z2),(z2↦z1),(z3↦z4),(z4↦z3)}" + ] + }, + "execution_count": 16, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "fusioniert" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Wir berechnen jetzt die neue Menge ```ZF``` an fusionierten Zuständen (mit der reflexiven und transitiven Hülle ```closure``` von ```fusioniert```):" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + ":let ZF {zs| #x.(x:Z & closure(fusioniert)[{x}] = zs)}" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Man kann jetzt die Übergangsfunktion für ZF so ausrechnen:" + ] + }, + { + "cell_type": "code", + "execution_count": 32, + "metadata": {}, + "outputs": [ + { + "data": { + "text/markdown": [ + "$\\{(\\{\\mathit{z0}\\}\\mapsto 0\\mapsto\\{\\mathit{z1},\\mathit{z2}\\}),(\\{\\mathit{z0}\\}\\mapsto 1\\mapsto\\{\\mathit{z1},\\mathit{z2}\\}),(\\{\\mathit{z1},\\mathit{z2}\\}\\mapsto 0\\mapsto\\{\\mathit{z3},\\mathit{z4}\\}),(\\{\\mathit{z1},\\mathit{z2}\\}\\mapsto 1\\mapsto\\{\\mathit{z3},\\mathit{z4}\\}),(\\{\\mathit{z3},\\mathit{z4}\\}\\mapsto 0\\mapsto\\{\\mathit{z3},\\mathit{z4}\\}),(\\{\\mathit{z3},\\mathit{z4}\\}\\mapsto 1\\mapsto\\{\\mathit{z3},\\mathit{z4}\\})\\}$" + ], + "text/plain": [ + "{({z0}↦0↦{z1,z2}),({z0}↦1↦{z1,z2}),({z1,z2}↦0↦{z3,z4}),({z1,z2}↦1↦{z3,z4}),({z3,z4}↦0↦{z3,z4}),({z3,z4}↦1↦{z3,z4})}" + ] + }, + "execution_count": 32, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + ":let δF %(zfa,a).(zfa:ZF & a:Σ | closure(fusioniert)[UNION(za).(za:zfa|{δ(za,a)})])" + ] + }, + { + "cell_type": "code", + "execution_count": 33, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "Preference changed: DOT_DECOMPOSE_NODES = FALSE\n", + "Preference changed: DOT_ENGINE = dot\n" + ] + }, + "execution_count": 33, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + ":pref DOT_DECOMPOSE_NODES=FALSE DOT_ENGINE=dot" + ] + }, + { + "cell_type": "code", + "execution_count": 34, + "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.28.0 (20110509.1545)\n", + " -->\n", + "<!-- Title: state Pages: 1 -->\n", + "<svg width=\"270pt\" height=\"116pt\"\n", + " viewBox=\"0.00 0.00 270.00 116.02\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n", + "<g id=\"graph1\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 112.016)\">\n", + "<title>state</title>\n", + "<polygon fill=\"white\" stroke=\"white\" points=\"-4,5 -4,-112.016 267,-112.016 267,5 -4,5\"/>\n", + "<!-- \\{z3,z4\\} -->\n", + "<g id=\"node1\" class=\"node\"><title>\\{z3,z4\\}</title>\n", + "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"261.868,-40.0157 202.132,-40.0157 202.132,-4.01569 261.868,-4.01569 261.868,-40.0157\"/>\n", + "<text text-anchor=\"middle\" x=\"232\" y=\"-17.8157\" font-family=\"Times,serif\" font-size=\"14.00\">{z3,z4}</text>\n", + "</g>\n", + "<!-- \\{z3,z4\\}->\\{z3,z4\\} -->\n", + "<g id=\"edge2\" class=\"edge\"><title>\\{z3,z4\\}->\\{z3,z4\\}</title>\n", + "<path fill=\"none\" stroke=\"firebrick\" d=\"M227.296,-40.1684C226.573,-49.5548 228.141,-58.0157 232,-58.0157 234.352,-58.0157 235.853,-54.8738 236.503,-50.2953\"/>\n", + "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"240.004,-50.2359 236.704,-40.1684 233.006,-50.097 240.004,-50.2359\"/>\n", + "<text text-anchor=\"middle\" x=\"232\" y=\"-62.2157\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n", + "</g>\n", + "<!-- \\{z3,z4\\}->\\{z3,z4\\} -->\n", + "<g id=\"edge8\" class=\"edge\"><title>\\{z3,z4\\}->\\{z3,z4\\}</title>\n", + "<path fill=\"none\" stroke=\"sienna\" d=\"M224.116,-40.2733C220.028,-57.418 222.656,-76.0157 232,-76.0157 239.519,-76.0157 242.689,-63.9733 241.51,-50.3359\"/>\n", + "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"244.935,-49.5866 239.884,-40.2733 238.025,-50.7037 244.935,-49.5866\"/>\n", + "<text text-anchor=\"middle\" x=\"232\" y=\"-80.2157\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n", + "</g>\n", + "<!-- \\{z1,z2\\} -->\n", + "<g id=\"node3\" class=\"node\"><title>\\{z1,z2\\}</title>\n", + "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"157.868,-40.0157 98.1325,-40.0157 98.1325,-4.01569 157.868,-4.01569 157.868,-40.0157\"/>\n", + "<text text-anchor=\"middle\" x=\"128\" y=\"-17.8157\" font-family=\"Times,serif\" font-size=\"14.00\">{z1,z2}</text>\n", + "</g>\n", + "<!-- \\{z1,z2\\}->\\{z3,z4\\} -->\n", + "<g id=\"edge4\" class=\"edge\"><title>\\{z1,z2\\}->\\{z3,z4\\}</title>\n", + "<path fill=\"none\" stroke=\"firebrick\" d=\"M157.684,-22.0157C168.331,-22.0157 180.594,-22.0157 192.007,-22.0157\"/>\n", + "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"192.178,-25.5158 202.178,-22.0157 192.178,-18.5158 192.178,-25.5158\"/>\n", + "<text text-anchor=\"middle\" x=\"180\" y=\"-26.2157\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n", + "</g>\n", + "<!-- \\{z1,z2\\}->\\{z3,z4\\} -->\n", + "<g id=\"edge10\" class=\"edge\"><title>\\{z1,z2\\}->\\{z3,z4\\}</title>\n", + "<path fill=\"none\" stroke=\"sienna\" d=\"M157.9,-4.38817C166.175,-1.19273 175.311,0.621167 184,-1.21569 186.865,-1.82123 189.767,-2.61326 192.65,-3.53401\"/>\n", + "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"191.705,-6.91528 202.299,-7.07656 194.118,-0.344219 191.705,-6.91528\"/>\n", + "<text text-anchor=\"middle\" x=\"180\" y=\"-5.21569\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n", + "</g>\n", + "<!-- \\{z0\\} -->\n", + "<g id=\"node5\" class=\"node\"><title>\\{z0\\}</title>\n", + "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"54,-40.0157 0,-40.0157 0,-4.01569 54,-4.01569 54,-40.0157\"/>\n", + "<text text-anchor=\"middle\" x=\"27\" y=\"-17.8157\" font-family=\"Times,serif\" font-size=\"14.00\">{z0}</text>\n", + "</g>\n", + "<!-- \\{z0\\}->\\{z1,z2\\} -->\n", + "<g id=\"edge6\" class=\"edge\"><title>\\{z0\\}->\\{z1,z2\\}</title>\n", + "<path fill=\"none\" stroke=\"firebrick\" d=\"M54.0111,-22.0157C64.3625,-22.0157 76.498,-22.0157 87.8691,-22.0157\"/>\n", + "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"88.024,-25.5158 98.024,-22.0157 88.024,-18.5158 88.024,-25.5158\"/>\n", + "<text text-anchor=\"middle\" x=\"76\" y=\"-26.2157\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n", + "</g>\n", + "<!-- \\{z0\\}->\\{z1,z2\\} -->\n", + "<g id=\"edge12\" class=\"edge\"><title>\\{z0\\}->\\{z1,z2\\}</title>\n", + "<path fill=\"none\" stroke=\"sienna\" d=\"M54.3169,-7.29102C59.9867,-4.77625 66.0641,-2.54804 72,-1.21569 77.4162,-0 83.0129,-0.239126 88.469,-1.3699\"/>\n", + "<polygon fill=\"sienna\" stroke=\"sienna\" points=\"87.4851,-4.72877 98.0689,-4.24664 89.4945,1.97664 87.4851,-4.72877\"/>\n", + "<text text-anchor=\"middle\" x=\"76\" y=\"-5.21569\" font-family=\"Times,serif\" font-size=\"14.00\">0</text>\n", + "</g>\n", + "</g>\n", + "</svg>" + ], + "text/plain": [ + "<Dot visualization: expr_as_graph [δFZFδF={(({z0},0),{z1,z2}),(({z0},1),{z1,z2}),(({z1,z2},0),{z3,z4}),(({z1,z2},1),{z3,z4}),(({z3,z4},0),{z3,z4}),(({z3,z4},1),{z3,z4})} & ZF={{z0},{z1,z2},{z3,z4}}(\"0\",{a,b|a:ZF & b=δF(a, 0)})]>" + ] + }, + "execution_count": 34, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + ":dot expr_as_graph (\"0\",{a,b|a:ZF & b=δF(a,0)}, \"1\",{a,b|a:ZF & b=δF(a,1)})" + ] + }, + { + "cell_type": "code", + "execution_count": 35, + "metadata": {}, + "outputs": [ + { + "data": { + "text/markdown": [ + "|prj11|prj12|prj2|\n", + "|---|---|---|\n", + "|$\\{\\mathit{z0}\\}$|$0$|$\\{\\mathit{z1},\\mathit{z2}\\}$|\n", + "|$\\{\\mathit{z0}\\}$|$1$|$\\{\\mathit{z1},\\mathit{z2}\\}$|\n", + "|$\\{\\mathit{z1},\\mathit{z2}\\}$|$0$|$\\{\\mathit{z3},\\mathit{z4}\\}$|\n", + "|$\\{\\mathit{z1},\\mathit{z2}\\}$|$1$|$\\{\\mathit{z3},\\mathit{z4}\\}$|\n", + "|$\\{\\mathit{z3},\\mathit{z4}\\}$|$0$|$\\{\\mathit{z3},\\mathit{z4}\\}$|\n", + "|$\\{\\mathit{z3},\\mathit{z4}\\}$|$1$|$\\{\\mathit{z3},\\mathit{z4}\\}$|\n" + ], + "text/plain": [ + "prj11\tprj12\tprj2\n", + "{z0}\t0\t{z1,z2}\n", + "{z0}\t1\t{z1,z2}\n", + "{z1,z2}\t0\t{z3,z4}\n", + "{z1,z2}\t1\t{z3,z4}\n", + "{z3,z4}\t0\t{z3,z4}\n", + "{z3,z4}\t1\t{z3,z4}\n" + ] + }, + "execution_count": 35, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + ":table δF" + ] + }, { "cell_type": "code", - "execution_count": 15, + "execution_count": 36, "metadata": {}, "outputs": [ { @@ -1262,7 +1482,7 @@ "\tProlog: SICStus 4.5.1 (x86_64-darwin-17.7.0): Tue Apr 2 15:34:32 CEST 2019" ] }, - "execution_count": 15, + "execution_count": 36, "metadata": {}, "output_type": "execute_result" }