diff --git a/info4/kapitel-3/PDA-Kellerautomaten.ipynb b/info4/kapitel-3/PDA-Kellerautomaten.ipynb index 1ec21713cf6fc266fd50bc42240398ff28aaf881..b84b16852226830d57c56088cc6afb48244002ef 100644 --- a/info4/kapitel-3/PDA-Kellerautomaten.ipynb +++ b/info4/kapitel-3/PDA-Kellerautomaten.ipynb @@ -57,7 +57,7 @@ " Γ == {A,BOT}; // das Kelleralphabet\n", " \n", " ANIMATION_FUNCTION_DEFAULT == {(1,1,z)};\n", - " ANIMATION_FUNCTION == {2}*α \\/ {3}*(γ);\n", + " ANIMATION_FUNCTION == {2}*α ∪ {3}*(γ);\n", " ANIMATION_FUNCTION1 == {(1,0,\"z: \"),(2,0,\"α:\"),(3,0,\"γ:\")};\n", " ANIMATION_STR_JUSTIFY_LEFTx == TRUE;\n", " SET_PREF_PRETTY_PRINT_SEQUENCES == TRUE\n", @@ -682,6 +682,796 @@ "Das Eingabewort ``aabb`` wurde akzeptiert." ] }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "## PDA für eine kfG\n", + "\n", + "Aus einer kontextfreien Grammatik kann man einen PDA konstruieren der die gleiche Sprache akzeptiert." + ] + }, + { + "cell_type": "code", + "execution_count": 3, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "Loaded machine: PDA" + ] + }, + "execution_count": 3, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "::load\n", + "MACHINE PDA\n", + "/* B Modell eines PDA */\n", + "SETS\n", + " Z = {z0}; // die Zustände des Automaten, z0 ist der Startzustand\n", + " SYMBOLE={a,b, S, C, lambda} /* BOT = # = Bottom-Symbol im Keller*/\n", + "DEFINITIONS\n", + " Σ == {a,b}; // das Eingabe-Alphabet\n", + " BOT == S;\n", + " Γ == {S,C}; // das Kelleralphabet\n", + " \n", + " ANIMATION_FUNCTION_DEFAULT == {(1,1,z)};\n", + " ANIMATION_FUNCTION == {2}*α ∪ {3}*(γ);\n", + " ANIMATION_FUNCTION1 == {(1,0,\"z: \"),(2,0,\"α:\"),(3,0,\"γ:\")};\n", + " ANIMATION_STR_JUSTIFY_LEFTx == TRUE;\n", + " SET_PREF_PRETTY_PRINT_SEQUENCES == TRUE\n", + "CONSTANTS P, δ\n", + "PROPERTIES\n", + "/* Die Grammatik Regeln */\n", + " P = { S ↦ [a,S,b], S ↦ [C],\n", + " C ↦ [a,b] } ∧\n", + " \n", + " /* Berechnung von δ aus P */\n", + " δ = /* lässt sich eine Regel auf das Top-Symbol im Keller anwenden tue \n", + " dies ohne etwas zu lesen :*/\n", + " { lhs,rhs | ∃(A,q).( A↦q ∈ P ∧ lhs=(z0,lambda,A) ∧ rhs=(z0,q))}\n", + " ∪\n", + " /* ist das Top-Symbol im Keller ein Terminalzeichen a welches\n", + " auf der Eingabe steht, so wird dies aus dem Keller gePOPt */\n", + " { lhs,rhs | ∃a.(a∈Σ ∧ lhs = (z0,a,a) & rhs = (z0,[]))}\n", + " \n", + " \n", + "VARIABLES \n", + " z, α, γ // Konfiguration in dem sich der PDA befindet\n", + "INVARIANT\n", + " z ∈ Z ∧ // der aktuelle Zustand\n", + " α ∈ seq(Σ) ∧ // der noch zu lesende Teil des Eingabeworts\n", + " γ ∈ seq(Γ) // aktuelle Kellerinhalt\n", + "INITIALISATION\n", + " z := z0 ||\n", + " γ := [BOT] || // Initialisierung des Stapels\n", + " α := [a,a,b,b] // das Eingabewort\n", + "OPERATIONS\n", + " // die Operationen Schritt und LambdaSchritt modellieren\n", + " // Schritte in der Ableitungsrelation\n", + " Schritt(z‘,s) = PRE α ≠ ∅ ∧ γ ≠ ∅ ∧\n", + " z‘↦s ∈ δ[{(z,first(α),first(γ))}] THEN\n", + " z := z‘ || // in den neuen Zustand wechseln\n", + " α := tail(α) || // das erste Symbol auf der Eingabe löschen\n", + " γ := s^tail(γ) // s auf den Stapel packen\n", + " END;\n", + " LambdaSchritt(z‘,s) = PRE γ ≠ ∅ ∧\n", + " z‘↦s ∈ δ[{(z,lambda,first(γ))}] THEN\n", + " z := z‘ || // in den neuen Zustand wechseln\n", + " γ := s^tail(γ) // s auf den Stapel packen\n", + " END;\n", + " Akzeptieren = PRE γ = ∅ ∧ α = ∅ THEN \n", + " /* Wir akzeptieren wenn Eingabe und Stapel leer sind */\n", + " skip END\n", + "END\n", + "\n" + ] + }, + { + "cell_type": "code", + "execution_count": 5, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "Machine constants set up using operation 0: $setup_constants()" + ] + }, + "execution_count": 5, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + ":constants" + ] + }, + { + "cell_type": "code", + "execution_count": 6, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "Machine initialised using operation 1: $initialise_machine()" + ] + }, + "execution_count": 6, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + ":init" + ] + }, + { + "cell_type": "code", + "execution_count": 33, + "metadata": {}, + "outputs": [ + { + "data": { + "text/markdown": [ + "|z|x|X|z2|Xs|\n", + "|---|---|---|---|---|\n", + "|$\\renewcommand{\\emptyset}{\\mathord\\varnothing}\\renewcommand{\\emptyset}{\\mathord\\varnothing}\\renewcommand{\\emptyset}{\\mathord\\varnothing}\\renewcommand{\\emptyset}{\\mathord\\varnothing}\\renewcommand{\\emptyset}{\\mathord\\varnothing}\\mathit{z0}$|$\\mathit{a}$|$\\mathit{a}$|$\\mathit{z0}$|$\\emptyset$|\n", + "|$\\mathit{z0}$|$\\mathit{b}$|$\\mathit{b}$|$\\mathit{z0}$|$\\emptyset$|\n", + "|$\\mathit{z0}$|$\\mathit{S}$|$\\mathit{S}$|$\\mathit{z0}$|$\\emptyset$|\n", + "|$\\mathit{z0}$|$\\mathit{C}$|$\\mathit{C}$|$\\mathit{z0}$|$\\emptyset$|\n", + "|$\\mathit{z0}$|$\\mathit{lambda}$|$\\mathit{S}$|$\\mathit{z0}$|$\\{(1\\mapsto \\mathit{C})\\}$|\n", + "|$\\mathit{z0}$|$\\mathit{lambda}$|$\\mathit{S}$|$\\mathit{z0}$|$\\{(1\\mapsto \\mathit{a}),(2\\mapsto \\mathit{S}),(3\\mapsto \\mathit{b})\\}$|\n", + "|$\\mathit{z0}$|$\\mathit{lambda}$|$\\mathit{C}$|$\\mathit{z0}$|$\\{(1\\mapsto \\mathit{a}),(2\\mapsto \\mathit{b})\\}$|\n", + "|$\\mathit{z0}$|$\\mathit{lambda}$|$\\mathit{lambda}$|$\\mathit{z0}$|$\\emptyset$|\n" + ], + "text/plain": [ + "z\tx\tX\tz2\tXs\n", + "z0\ta\ta\tz0\t{}\n", + "z0\tb\tb\tz0\t{}\n", + "z0\tS\tS\tz0\t{}\n", + "z0\tC\tC\tz0\t{}\n", + "z0\tlambda\tS\tz0\t{(1|->C)}\n", + "z0\tlambda\tS\tz0\t{(1|->a),(2|->S),(3|->b)}\n", + "z0\tlambda\tC\tz0\t{(1|->a),(2|->b)}\n", + "z0\tlambda\tlambda\tz0\t{}\n" + ] + }, + "execution_count": 33, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + ":table {z,x,X,z2,Xs| ((z,x,X)↦(z2,Xs)) : δ}" + ] + }, + { + "cell_type": "code", + "execution_count": 7, + "metadata": {}, + "outputs": [ + { + "data": { + "text/markdown": [ + "<table style=\"font-family:monospace\"><tbody>\n", + "<tr>\n", + "<td style=\"padding:10px\">z: </td>\n", + "<td style=\"padding:10px\">z0</td>\n", + "<td style=\"padding:0px\"></td>\n", + "<td style=\"padding:0px\"></td>\n", + "<td style=\"padding:0px\"></td>\n", + "</tr>\n", + "<tr>\n", + "<td style=\"padding:10px\">α:</td>\n", + "<td style=\"padding:10px\">a</td>\n", + "<td style=\"padding:10px\">a</td>\n", + "<td style=\"padding:10px\">b</td>\n", + "<td style=\"padding:10px\">b</td>\n", + "</tr>\n", + "<tr>\n", + "<td style=\"padding:10px\">γ:</td>\n", + "<td style=\"padding:10px\">S</td>\n", + "<td style=\"padding:0px\"></td>\n", + "<td style=\"padding:0px\"></td>\n", + "<td style=\"padding:0px\"></td>\n", + "</tr>\n", + "</tbody></table>" + ], + "text/plain": [ + "<Animation function visualisation>" + ] + }, + "execution_count": 7, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + ":show" + ] + }, + { + "cell_type": "code", + "execution_count": 8, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "Machine: PDA\n", + "Sets: Z, SYMBOLE\n", + "Constants: P, δ\n", + "Variables: z, α, γ\n", + "Operations: \n", + "LambdaSchritt(z0,{(1|->C)})\n", + "LambdaSchritt(z0,{(1|->a),(2|->S),(3|->b)})" + ] + }, + "execution_count": 8, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + ":browse" + ] + }, + { + "cell_type": "code", + "execution_count": 9, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "Executed operation: LambdaSchritt(z0,{(1|->a),(2|->S),(3|->b)})" + ] + }, + "execution_count": 9, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + ":exec LambdaSchritt s = [a,S,b]" + ] + }, + { + "cell_type": "code", + "execution_count": 10, + "metadata": {}, + "outputs": [ + { + "data": { + "text/markdown": [ + "<table style=\"font-family:monospace\"><tbody>\n", + "<tr>\n", + "<td style=\"padding:10px\">z: </td>\n", + "<td style=\"padding:10px\">z0</td>\n", + "<td style=\"padding:0px\"></td>\n", + "<td style=\"padding:0px\"></td>\n", + "<td style=\"padding:0px\"></td>\n", + "</tr>\n", + "<tr>\n", + "<td style=\"padding:10px\">α:</td>\n", + "<td style=\"padding:10px\">a</td>\n", + "<td style=\"padding:10px\">a</td>\n", + "<td style=\"padding:10px\">b</td>\n", + "<td style=\"padding:10px\">b</td>\n", + "</tr>\n", + "<tr>\n", + "<td style=\"padding:10px\">γ:</td>\n", + "<td style=\"padding:10px\">a</td>\n", + "<td style=\"padding:10px\">S</td>\n", + "<td style=\"padding:10px\">b</td>\n", + "<td style=\"padding:0px\"></td>\n", + "</tr>\n", + "</tbody></table>" + ], + "text/plain": [ + "<Animation function visualisation>" + ] + }, + "execution_count": 10, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + ":show" + ] + }, + { + "cell_type": "code", + "execution_count": 11, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "Machine: PDA\n", + "Sets: Z, SYMBOLE\n", + "Constants: P, δ\n", + "Variables: z, α, γ\n", + "Operations: \n", + "Schritt(z0,{})" + ] + }, + "execution_count": 11, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + ":browse" + ] + }, + { + "cell_type": "code", + "execution_count": 13, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "Executed operation: Schritt(z0,{})" + ] + }, + "execution_count": 13, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + ":exec Schritt" + ] + }, + { + "cell_type": "code", + "execution_count": 14, + "metadata": {}, + "outputs": [ + { + "data": { + "text/markdown": [ + "<table style=\"font-family:monospace\"><tbody>\n", + "<tr>\n", + "<td style=\"padding:10px\">z: </td>\n", + "<td style=\"padding:10px\">z0</td>\n", + "<td style=\"padding:0px\"></td>\n", + "<td style=\"padding:0px\"></td>\n", + "</tr>\n", + "<tr>\n", + "<td style=\"padding:10px\">α:</td>\n", + "<td style=\"padding:10px\">a</td>\n", + "<td style=\"padding:10px\">b</td>\n", + "<td style=\"padding:10px\">b</td>\n", + "</tr>\n", + "<tr>\n", + "<td style=\"padding:10px\">γ:</td>\n", + "<td style=\"padding:10px\">S</td>\n", + "<td style=\"padding:10px\">b</td>\n", + "<td style=\"padding:0px\"></td>\n", + "</tr>\n", + "</tbody></table>" + ], + "text/plain": [ + "<Animation function visualisation>" + ] + }, + "execution_count": 14, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + ":show" + ] + }, + { + "cell_type": "code", + "execution_count": 15, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "Machine: PDA\n", + "Sets: Z, SYMBOLE\n", + "Constants: P, δ\n", + "Variables: z, α, γ\n", + "Operations: \n", + "LambdaSchritt(z0,{(1|->C)})\n", + "LambdaSchritt(z0,{(1|->a),(2|->S),(3|->b)})" + ] + }, + "execution_count": 15, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + ":browse" + ] + }, + { + "cell_type": "code", + "execution_count": 16, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "Executed operation: LambdaSchritt(z0,{(1|->C)})" + ] + }, + "execution_count": 16, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + ":exec LambdaSchritt s = [C]" + ] + }, + { + "cell_type": "code", + "execution_count": 17, + "metadata": {}, + "outputs": [ + { + "data": { + "text/markdown": [ + "<table style=\"font-family:monospace\"><tbody>\n", + "<tr>\n", + "<td style=\"padding:10px\">z: </td>\n", + "<td style=\"padding:10px\">z0</td>\n", + "<td style=\"padding:0px\"></td>\n", + "<td style=\"padding:0px\"></td>\n", + "</tr>\n", + "<tr>\n", + "<td style=\"padding:10px\">α:</td>\n", + "<td style=\"padding:10px\">a</td>\n", + "<td style=\"padding:10px\">b</td>\n", + "<td style=\"padding:10px\">b</td>\n", + "</tr>\n", + "<tr>\n", + "<td style=\"padding:10px\">γ:</td>\n", + "<td style=\"padding:10px\">C</td>\n", + "<td style=\"padding:10px\">b</td>\n", + "<td style=\"padding:0px\"></td>\n", + "</tr>\n", + "</tbody></table>" + ], + "text/plain": [ + "<Animation function visualisation>" + ] + }, + "execution_count": 17, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + ":show" + ] + }, + { + "cell_type": "code", + "execution_count": 18, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "Machine: PDA\n", + "Sets: Z, SYMBOLE\n", + "Constants: P, δ\n", + "Variables: z, α, γ\n", + "Operations: \n", + "LambdaSchritt(z0,{(1|->a),(2|->b)})" + ] + }, + "execution_count": 18, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + ":browse" + ] + }, + { + "cell_type": "code", + "execution_count": 19, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "Executed operation: LambdaSchritt(z0,{(1|->a),(2|->b)})" + ] + }, + "execution_count": 19, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + ":exec LambdaSchritt s=[a,b]" + ] + }, + { + "cell_type": "code", + "execution_count": 20, + "metadata": {}, + "outputs": [ + { + "data": { + "text/markdown": [ + "<table style=\"font-family:monospace\"><tbody>\n", + "<tr>\n", + "<td style=\"padding:10px\">z: </td>\n", + "<td style=\"padding:10px\">z0</td>\n", + "<td style=\"padding:0px\"></td>\n", + "<td style=\"padding:0px\"></td>\n", + "</tr>\n", + "<tr>\n", + "<td style=\"padding:10px\">α:</td>\n", + "<td style=\"padding:10px\">a</td>\n", + "<td style=\"padding:10px\">b</td>\n", + "<td style=\"padding:10px\">b</td>\n", + "</tr>\n", + "<tr>\n", + "<td style=\"padding:10px\">γ:</td>\n", + "<td style=\"padding:10px\">a</td>\n", + "<td style=\"padding:10px\">b</td>\n", + "<td style=\"padding:10px\">b</td>\n", + "</tr>\n", + "</tbody></table>" + ], + "text/plain": [ + "<Animation function visualisation>" + ] + }, + "execution_count": 20, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + ":show" + ] + }, + { + "cell_type": "code", + "execution_count": 22, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "Machine: PDA\n", + "Sets: Z, SYMBOLE\n", + "Constants: P, δ\n", + "Variables: z, α, γ\n", + "Operations: \n", + "Schritt(z0,{})" + ] + }, + "execution_count": 22, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + ":browse" + ] + }, + { + "cell_type": "code", + "execution_count": 23, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "Executed operation: Schritt(z0,{})" + ] + }, + "execution_count": 23, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + ":exec Schritt" + ] + }, + { + "cell_type": "code", + "execution_count": 24, + "metadata": {}, + "outputs": [ + { + "data": { + "text/markdown": [ + "<table style=\"font-family:monospace\"><tbody>\n", + "<tr>\n", + "<td style=\"padding:10px\">z: </td>\n", + "<td style=\"padding:10px\">z0</td>\n", + "<td style=\"padding:0px\"></td>\n", + "</tr>\n", + "<tr>\n", + "<td style=\"padding:10px\">α:</td>\n", + "<td style=\"padding:10px\">b</td>\n", + "<td style=\"padding:10px\">b</td>\n", + "</tr>\n", + "<tr>\n", + "<td style=\"padding:10px\">γ:</td>\n", + "<td style=\"padding:10px\">b</td>\n", + "<td style=\"padding:10px\">b</td>\n", + "</tr>\n", + "</tbody></table>" + ], + "text/plain": [ + "<Animation function visualisation>" + ] + }, + "execution_count": 24, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + ":show" + ] + }, + { + "cell_type": "code", + "execution_count": 25, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "Executed operation: Schritt(z0,{})" + ] + }, + "execution_count": 25, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + ":exec Schritt" + ] + }, + { + "cell_type": "code", + "execution_count": 26, + "metadata": {}, + "outputs": [ + { + "data": { + "text/markdown": [ + "<table style=\"font-family:monospace\"><tbody>\n", + "<tr>\n", + "<td style=\"padding:10px\">z: </td>\n", + "<td style=\"padding:10px\">z0</td>\n", + "</tr>\n", + "<tr>\n", + "<td style=\"padding:10px\">α:</td>\n", + "<td style=\"padding:10px\">b</td>\n", + "</tr>\n", + "<tr>\n", + "<td style=\"padding:10px\">γ:</td>\n", + "<td style=\"padding:10px\">b</td>\n", + "</tr>\n", + "</tbody></table>" + ], + "text/plain": [ + "<Animation function visualisation>" + ] + }, + "execution_count": 26, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + ":show" + ] + }, + { + "cell_type": "code", + "execution_count": 27, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "Executed operation: Schritt(z0,{})" + ] + }, + "execution_count": 27, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + ":exec Schritt" + ] + }, + { + "cell_type": "code", + "execution_count": 28, + "metadata": {}, + "outputs": [ + { + "data": { + "text/markdown": [ + "<table style=\"font-family:monospace\"><tbody>\n", + "<tr>\n", + "<td style=\"padding:10px\">z: </td>\n", + "<td style=\"padding:10px\">z0</td>\n", + "</tr>\n", + "<tr>\n", + "<td style=\"padding:10px\">α:</td>\n", + "<td style=\"padding:0px\"></td>\n", + "</tr>\n", + "<tr>\n", + "<td style=\"padding:10px\">γ:</td>\n", + "<td style=\"padding:0px\"></td>\n", + "</tr>\n", + "</tbody></table>" + ], + "text/plain": [ + "<Animation function visualisation>" + ] + }, + "execution_count": 28, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + ":show" + ] + }, + { + "cell_type": "code", + "execution_count": 30, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "Executed operation: Akzeptieren()" + ] + }, + "execution_count": 30, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + ":exec Akzeptieren" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Das Wort ``aabb`` wird sowohl von der Grammatik generiert als auch von diesem generierten PDA akzeptiert." + ] + }, { "cell_type": "code", "execution_count": null,