PDA-Kellerautomaten.ipynb 34.7 KB
 Michael Leuschel committed Jun 02, 2020 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 { "cells": [ { "cell_type": "markdown", "metadata": {}, "source": [ "# PDA (Push Down Automata - Kellerautomaten)" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "\n", "Ein __(nichtdeterministischer) Kellerautomat__ \n", "(kurz PDA für __push-down automaton__) ist ein $6$-Tupel \n", " $M = (\\Sigma, \\Gamma, Z, \\delta , z_0, \\#)$, wobei\n", "* $\\Sigma$ das Eingabe-Alphabet ist, \n", "* $\\Gamma$ das Kelleralphabet, \n", "* $Z$ eine endliche Menge von Zuständen,\n", "* $\\delta : Z \\times (\\Sigma \\cup \\{\\lambda\\}) \\times \\Gamma\n", " \\rightarrow \\mathfrak{P}_e(Z \\times \\Gamma^{\\ast})$ die\n", " Überführungsfunktion,\n", "* $z_0 \\in Z$ der Startzustand,\n", "* $\\# \\in \\Gamma$ das Bottom-Symbol im Keller.\n", "\n", "\n", "Anmerkung: $\\mathfrak{P}_e(Z \\times \\Gamma^{\\ast})$ ist die Menge aller\n", " __endlichen__ Teilmengen von $Z \\times \\Gamma^{\\ast}$." ] }, { "cell_type": "code",  Michael Leuschel committed Jun 10, 2020 34  "execution_count": 1,  Michael Leuschel committed Jun 02, 2020 35 36 37 38 39 40 41 42  "metadata": {}, "outputs": [ { "data": { "text/plain": [ "Loaded machine: PDA" ] },  Michael Leuschel committed Jun 10, 2020 43  "execution_count": 1,  Michael Leuschel committed Jun 02, 2020 44 45 46 47 48 49 50 51 52 53 54 55 56 57  "metadata": {}, "output_type": "execute_result" } ], "source": [ "::load\n", "MACHINE PDA\n", "/* B Modell eines PDA */\n", "SETS\n", " Z = {z0,z1}; // die Zustände des Automaten, z0 ist der Startzustand\n", " SYMBOLE={a,b, A, BOT, lambda} /* BOT = # = Bottom-Symbol im Keller*/\n", "DEFINITIONS\n", " \n", " ANIMATION_FUNCTION_DEFAULT == {(1,1,z)};\n",  Michael Leuschel committed Jun 02, 2020 58  " ANIMATION_FUNCTION == {2}*α ∪ {3}*(γ);\n",  Michael Leuschel committed Jun 02, 2020 59 60  " ANIMATION_FUNCTION1 == {(1,0,\"z: \"),(2,0,\"α:\"),(3,0,\"γ:\")};\n", " ANIMATION_STR_JUSTIFY_LEFTx == TRUE;\n",  Michael Leuschel committed Jun 03, 2020 61  " SET_PREF_PP_SEQUENCES == TRUE\n",  Michael Leuschel committed Jun 10, 2020 62  "CONSTANTS δ, Σ, Γ\n",  Michael Leuschel committed Jun 02, 2020 63  "PROPERTIES\n",  Michael Leuschel committed Jun 10, 2020 64 65 66 67  " Σ = {a,b} // das Eingabe-Alphabet\n", " ∧\n", " Γ = {A,BOT} // das Kelleralphabet\n", " ∧\n",  Michael Leuschel committed Jun 02, 2020 68  " /* Der PDA für {a^m b^m| m>=1} ; Beispiel von Info 4 (Folie 95ff) */\n",  Michael Leuschel committed Jun 02, 2020 69 70 71 72 73  " δ = { (z0,a,BOT) ↦ (z0,[A,BOT]),\n", " (z0,a,A) ↦ (z0,[A,A]),\n", " (z0,b,A) ↦ (z1,[]),\n", " (z1,lambda,BOT) ↦ (z1,[]),\n", " (z1,b,A) ↦ (z1,[]) }\n",  Michael Leuschel committed Jun 02, 2020 74 75  " // Anmerkung: δ ist hier als Relation anstatt als Funktion zu Mengen definiert\n", " // Deshalb entspricht δ[{(z,a,g)}] in der B Maschine δ(z,a,g) aus dem Skript\n",  Michael Leuschel committed Jun 02, 2020 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108  "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",  Michael Leuschel committed Jun 10, 2020 109  "execution_count": 2,  Michael Leuschel committed Jun 02, 2020 110 111 112 113 114 115 116 117  "metadata": {}, "outputs": [ { "data": { "text/plain": [ "Machine constants set up using operation 0: $setup_constants()" ] },  Michael Leuschel committed Jun 10, 2020 118  "execution_count": 2,  Michael Leuschel committed Jun 02, 2020 119 120 121 122 123 124 125 126 127 128  "metadata": {}, "output_type": "execute_result" } ], "source": [ ":constants" ] }, { "cell_type": "code",  Michael Leuschel committed Jun 10, 2020 129  "execution_count": 3,  Michael Leuschel committed Jun 02, 2020 130 131 132 133 134 135 136 137  "metadata": {}, "outputs": [ { "data": { "text/plain": [ "Machine initialised using operation 1:$initialise_machine()" ] },  Michael Leuschel committed Jun 10, 2020 138  "execution_count": 3,  Michael Leuschel committed Jun 02, 2020 139 140 141 142 143 144 145 146 147 148  "metadata": {}, "output_type": "execute_result" } ], "source": [ ":init" ] }, { "cell_type": "code",  Michael Leuschel committed Jun 10, 2020 149  "execution_count": 4,  Michael Leuschel committed Jun 02, 2020 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182  "metadata": {}, "outputs": [ { "data": { "text/markdown": [ "
z: z0
α:aabb
γ:BOT
\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "" ], "text/plain": [ "" ] },  Michael Leuschel committed Jun 10, 2020 183  "execution_count": 4,  Michael Leuschel committed Jun 02, 2020 184 185 186 187 188 189 190 191 192 193  "metadata": {}, "output_type": "execute_result" } ], "source": [ ":show" ] }, { "cell_type": "code",  Chris committed Nov 07, 2020 194  "execution_count": 5,  Michael Leuschel committed Jun 02, 2020 195 196 197 198 199 200 201  "metadata": {}, "outputs": [ { "data": { "text/plain": [ "Machine: PDA\n", "Sets: Z, SYMBOLE\n",  Chris committed Nov 07, 2020 202  "Constants: δ, Σ, Γ\n",  Michael Leuschel committed Jun 02, 2020 203 204  "Variables: z, α, γ\n", "Operations: \n",  Michael Leuschel committed Jun 03, 2020 205  "Schritt(z0,[A,BOT])"  Michael Leuschel committed Jun 02, 2020 206 207  ] },  Chris committed Nov 07, 2020 208  "execution_count": 5,  Michael Leuschel committed Jun 02, 2020 209 210 211 212 213 214 215 216 217 218  "metadata": {}, "output_type": "execute_result" } ], "source": [ ":browse" ] }, { "cell_type": "code",  Chris committed Nov 07, 2020 219  "execution_count": 6,  Michael Leuschel committed Jun 02, 2020 220 221 222 223 224  "metadata": {}, "outputs": [ { "data": { "text/plain": [  Michael Leuschel committed Jun 03, 2020 225  "Executed operation: Schritt(z0,[A,BOT])"  Michael Leuschel committed Jun 02, 2020 226 227  ] },  Chris committed Nov 07, 2020 228  "execution_count": 6,  Michael Leuschel committed Jun 02, 2020 229 230 231 232 233 234 235 236 237 238  "metadata": {}, "output_type": "execute_result" } ], "source": [ ":exec Schritt" ] }, { "cell_type": "code",  Chris committed Nov 07, 2020 239  "execution_count": 7,  Michael Leuschel committed Jun 02, 2020 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269  "metadata": {}, "outputs": [ { "data": { "text/markdown": [ "
z: z0
α:abb
γ:ABOT
\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "" ], "text/plain": [ "" ] },  Chris committed Nov 07, 2020 270  "execution_count": 7,  Michael Leuschel committed Jun 02, 2020 271 272 273 274 275 276 277 278 279 280  "metadata": {}, "output_type": "execute_result" } ], "source": [ ":show" ] }, { "cell_type": "code",  Chris committed Nov 07, 2020 281  "execution_count": 8,  Michael Leuschel committed Jun 02, 2020 282 283 284 285 286  "metadata": {}, "outputs": [ { "data": { "text/markdown": [  Michael Leuschel committed Jun 03, 2020 287  "$(\\mathit{z0}\\mapsto [a,\\mathit{b},b]\\mapsto [A,BOT])$"  Michael Leuschel committed Jun 02, 2020 288 289  ], "text/plain": [  Michael Leuschel committed Jun 03, 2020 290  "(z0↦[a,b,b]↦[A,BOT])"  Michael Leuschel committed Jun 02, 2020 291 292  ] },  Chris committed Nov 07, 2020 293  "execution_count": 8,  Michael Leuschel committed Jun 02, 2020 294 295 296 297 298 299 300 301 302 303  "metadata": {}, "output_type": "execute_result" } ], "source": [ "(z,α,γ)" ] }, { "cell_type": "code",  Chris committed Nov 07, 2020 304  "execution_count": 9,  Michael Leuschel committed Jun 02, 2020 305 306 307 308 309 310 311  "metadata": {}, "outputs": [ { "data": { "text/plain": [ "Machine: PDA\n", "Sets: Z, SYMBOLE\n",  Chris committed Nov 07, 2020 312  "Constants: δ, Σ, Γ\n",  Michael Leuschel committed Jun 02, 2020 313 314  "Variables: z, α, γ\n", "Operations: \n",  Michael Leuschel committed Jun 03, 2020 315  "Schritt(z0,[A,A])"  Michael Leuschel committed Jun 02, 2020 316 317  ] },  Chris committed Nov 07, 2020 318  "execution_count": 9,  Michael Leuschel committed Jun 02, 2020 319 320 321 322 323 324 325 326 327 328  "metadata": {}, "output_type": "execute_result" } ], "source": [ ":browse" ] }, { "cell_type": "code",  Chris committed Nov 07, 2020 329  "execution_count": 10,  Michael Leuschel committed Jun 02, 2020 330 331 332 333 334  "metadata": {}, "outputs": [ { "data": { "text/plain": [  Michael Leuschel committed Jun 03, 2020 335  "Executed operation: Schritt(z0,[A,A])"  Michael Leuschel committed Jun 02, 2020 336 337  ] },  Chris committed Nov 07, 2020 338  "execution_count": 10,  Michael Leuschel committed Jun 02, 2020 339 340 341 342 343 344 345 346 347 348  "metadata": {}, "output_type": "execute_result" } ], "source": [ ":exec Schritt" ] }, { "cell_type": "code",  Chris committed Nov 07, 2020 349  "execution_count": 11,  Michael Leuschel committed Jun 02, 2020 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379  "metadata": {}, "outputs": [ { "data": { "text/markdown": [ "
z: z0
α:bb
γ:AABOT
\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "" ], "text/plain": [ "" ] },  Chris committed Nov 07, 2020 380  "execution_count": 11,  Michael Leuschel committed Jun 02, 2020 381 382 383 384 385 386 387 388 389 390  "metadata": {}, "output_type": "execute_result" } ], "source": [ ":show" ] }, { "cell_type": "code",  Chris committed Nov 07, 2020 391  "execution_count": 12,  Michael Leuschel committed Jun 02, 2020 392 393 394 395 396 397 398  "metadata": {}, "outputs": [ { "data": { "text/plain": [ "Machine: PDA\n", "Sets: Z, SYMBOLE\n",  Chris committed Nov 07, 2020 399  "Constants: δ, Σ, Γ\n",  Michael Leuschel committed Jun 02, 2020 400 401  "Variables: z, α, γ\n", "Operations: \n",  Michael Leuschel committed Jun 03, 2020 402  "Schritt(z1,[])"  Michael Leuschel committed Jun 02, 2020 403 404  ] },  Chris committed Nov 07, 2020 405  "execution_count": 12,  Michael Leuschel committed Jun 02, 2020 406 407 408 409 410 411 412 413 414 415  "metadata": {}, "output_type": "execute_result" } ], "source": [ ":browse" ] }, { "cell_type": "code",  Chris committed Nov 07, 2020 416  "execution_count": 13,  Michael Leuschel committed Jun 02, 2020 417 418 419 420 421  "metadata": {}, "outputs": [ { "data": { "text/plain": [  Michael Leuschel committed Jun 03, 2020 422  "Executed operation: Schritt(z1,[])"  Michael Leuschel committed Jun 02, 2020 423 424  ] },  Chris committed Nov 07, 2020 425  "execution_count": 13,  Michael Leuschel committed Jun 02, 2020 426 427 428 429 430 431 432 433 434 435  "metadata": {}, "output_type": "execute_result" } ], "source": [ ":exec Schritt" ] }, { "cell_type": "code",  Chris committed Nov 07, 2020 436  "execution_count": 14,  Michael Leuschel committed Jun 02, 2020 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463  "metadata": {}, "outputs": [ { "data": { "text/markdown": [ "
z: z1
α:b
γ:ABOT
\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "" ], "text/plain": [ "" ] },  Chris committed Nov 07, 2020 464  "execution_count": 14,  Michael Leuschel committed Jun 02, 2020 465 466 467 468 469 470 471 472 473 474  "metadata": {}, "output_type": "execute_result" } ], "source": [ ":show" ] }, { "cell_type": "code",  Chris committed Nov 07, 2020 475  "execution_count": 15,  Michael Leuschel committed Jun 02, 2020 476 477 478 479 480 481 482  "metadata": {}, "outputs": [ { "data": { "text/plain": [ "Machine: PDA\n", "Sets: Z, SYMBOLE\n",  Chris committed Nov 07, 2020 483  "Constants: δ, Σ, Γ\n",  Michael Leuschel committed Jun 02, 2020 484 485  "Variables: z, α, γ\n", "Operations: \n",  Michael Leuschel committed Jun 03, 2020 486  "Schritt(z1,[])"  Michael Leuschel committed Jun 02, 2020 487 488  ] },  Chris committed Nov 07, 2020 489  "execution_count": 15,  Michael Leuschel committed Jun 02, 2020 490 491 492 493 494 495 496 497 498 499  "metadata": {}, "output_type": "execute_result" } ], "source": [ ":browse" ] }, { "cell_type": "code",  Chris committed Nov 07, 2020 500  "execution_count": 16,  Michael Leuschel committed Jun 02, 2020 501 502 503 504 505  "metadata": {}, "outputs": [ { "data": { "text/plain": [  Michael Leuschel committed Jun 03, 2020 506  "Executed operation: Schritt(z1,[])"  Michael Leuschel committed Jun 02, 2020 507 508  ] },  Chris committed Nov 07, 2020 509  "execution_count": 16,  Michael Leuschel committed Jun 02, 2020 510 511 512 513 514 515 516 517 518 519  "metadata": {}, "output_type": "execute_result" } ], "source": [ ":exec Schritt" ] }, { "cell_type": "code",  Chris committed Nov 07, 2020 520  "execution_count": 17,  Michael Leuschel committed Jun 02, 2020 521 522 523 524 525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544  "metadata": {}, "outputs": [ { "data": { "text/markdown": [ "
z: z1
α:
γ:BOT
\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "" ], "text/plain": [ "" ] },  Chris committed Nov 07, 2020 545  "execution_count": 17,  Michael Leuschel committed Jun 02, 2020 546 547 548 549 550 551 552 553 554 555  "metadata": {}, "output_type": "execute_result" } ], "source": [ ":show" ] }, { "cell_type": "code",  Chris committed Nov 07, 2020 556  "execution_count": 18,  Michael Leuschel committed Jun 02, 2020 557 558 559 560 561 562 563  "metadata": {}, "outputs": [ { "data": { "text/plain": [ "Machine: PDA\n", "Sets: Z, SYMBOLE\n",  Chris committed Nov 07, 2020 564  "Constants: δ, Σ, Γ\n",  Michael Leuschel committed Jun 02, 2020 565 566  "Variables: z, α, γ\n", "Operations: \n",  Michael Leuschel committed Jun 03, 2020 567  "LambdaSchritt(z1,[])"  Michael Leuschel committed Jun 02, 2020 568 569  ] },  Chris committed Nov 07, 2020 570  "execution_count": 18,  Michael Leuschel committed Jun 02, 2020 571 572 573 574 575 576 577 578 579 580  "metadata": {}, "output_type": "execute_result" } ], "source": [ ":browse" ] }, { "cell_type": "code",  Chris committed Nov 07, 2020 581  "execution_count": 19,  Michael Leuschel committed Jun 02, 2020 582 583 584 585 586  "metadata": {}, "outputs": [ { "data": { "text/plain": [  Michael Leuschel committed Jun 03, 2020 587  "Executed operation: LambdaSchritt(z1,[])"  Michael Leuschel committed Jun 02, 2020 588 589  ] },  Chris committed Nov 07, 2020 590  "execution_count": 19,  Michael Leuschel committed Jun 02, 2020 591 592 593 594 595 596 597 598 599 600  "metadata": {}, "output_type": "execute_result" } ], "source": [ ":exec LambdaSchritt" ] }, { "cell_type": "code",  Chris committed Nov 07, 2020 601  "execution_count": 20,  Michael Leuschel committed Jun 02, 2020 602 603 604 605 606 607 608 609 610 611 612 613 614 615 616 617 618 619 620 621 622 623 624 625  "metadata": {}, "outputs": [ { "data": { "text/markdown": [ "
z: z1
α:
γ:
\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "" ], "text/plain": [ "" ] },  Chris committed Nov 07, 2020 626  "execution_count": 20,  Michael Leuschel committed Jun 02, 2020 627 628 629 630 631 632 633 634 635 636  "metadata": {}, "output_type": "execute_result" } ], "source": [ ":show" ] }, { "cell_type": "code",  Chris committed Nov 07, 2020 637  "execution_count": 21,  Michael Leuschel committed Jun 02, 2020 638 639 640 641 642 643 644  "metadata": {}, "outputs": [ { "data": { "text/plain": [ "Machine: PDA\n", "Sets: Z, SYMBOLE\n",  Chris committed Nov 07, 2020 645  "Constants: δ, Σ, Γ\n",  Michael Leuschel committed Jun 02, 2020 646 647 648 649 650  "Variables: z, α, γ\n", "Operations: \n", "Akzeptieren()" ] },  Chris committed Nov 07, 2020 651  "execution_count": 21,  Michael Leuschel committed Jun 02, 2020 652 653 654 655 656 657 658 659 660 661  "metadata": {}, "output_type": "execute_result" } ], "source": [ ":browse" ] }, { "cell_type": "code",  Chris committed Nov 07, 2020 662  "execution_count": 22,  Michael Leuschel committed Jun 02, 2020 663 664 665 666 667 668 669 670  "metadata": {}, "outputs": [ { "data": { "text/plain": [ "Executed operation: Akzeptieren()" ] },  Chris committed Nov 07, 2020 671  "execution_count": 22,  Michael Leuschel committed Jun 02, 2020 672 673 674 675 676 677 678 679 680 681 682 683 684 685 686  "metadata": {}, "output_type": "execute_result" } ], "source": [ ":exec Akzeptieren" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Das Eingabewort aabb wurde akzeptiert." ] },  Michael Leuschel committed Jun 02, 2020 687 688 689 690 691 692 693 694 695 696 697  { "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",  Chris committed Nov 07, 2020 698  "execution_count": 23,  Michael Leuschel committed Jun 02, 2020 699 700 701 702 703  "metadata": {}, "outputs": [ { "data": { "text/plain": [  Michael Leuschel committed Jun 03, 2020 704  "Loaded machine: PDA_für_kfG"  Michael Leuschel committed Jun 02, 2020 705 706  ] },  Chris committed Nov 07, 2020 707  "execution_count": 23,  Michael Leuschel committed Jun 02, 2020 708 709 710 711 712 713  "metadata": {}, "output_type": "execute_result" } ], "source": [ "::load\n",  Michael Leuschel committed Jun 03, 2020 714  "MACHINE PDA_für_kfG\n",  Michael Leuschel committed Jun 02, 2020 715 716 717 718 719 720 721 722 723 724 725 726 727  "/* 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",  Michael Leuschel committed Jun 03, 2020 728  " SET_PREF_PP_SEQUENCES == TRUE\n",  Michael Leuschel committed Jun 02, 2020 729 730 731 732 733 734 735 736 737 738 739 740 741 742 743 744 745 746 747 748 749 750 751 752 753 754 755 756 757 758 759 760 761 762 763 764 765 766 767 768 769 770 771 772 773 774 775 776 777  "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",  Chris committed Nov 07, 2020 778  "execution_count": 24,  Michael Leuschel committed Jun 02, 2020 779 780 781 782 783 784 785 786  "metadata": {}, "outputs": [ { "data": { "text/plain": [ "Machine constants set up using operation 0: $setup_constants()" ] },  Chris committed Nov 07, 2020 787  "execution_count": 24,  Michael Leuschel committed Jun 02, 2020 788 789 790 791 792 793 794 795 796 797  "metadata": {}, "output_type": "execute_result" } ], "source": [ ":constants" ] }, { "cell_type": "code",  Chris committed Nov 07, 2020 798  "execution_count": 25,  Michael Leuschel committed Jun 02, 2020 799 800 801 802 803 804 805 806  "metadata": {}, "outputs": [ { "data": { "text/plain": [ "Machine initialised using operation 1:$initialise_machine()" ] },  Chris committed Nov 07, 2020 807  "execution_count": 25,  Michael Leuschel committed Jun 02, 2020 808 809 810 811 812 813 814 815 816 817  "metadata": {}, "output_type": "execute_result" } ], "source": [ ":init" ] }, { "cell_type": "code",  Chris committed Nov 07, 2020 818  "execution_count": 26,  Michael Leuschel committed Jun 02, 2020 819 820 821 822 823 824 825  "metadata": {}, "outputs": [ { "data": { "text/markdown": [ "|z|x|X|z2|Xs|\n", "|---|---|---|---|---|\n",  Michael Leuschel committed Jun 03, 2020 826 827 828 829 830 831 832 833  "|$\\mathit{z0}$|$\\mathit{a}$|$\\mathit{a}$|$\\mathit{z0}$|$[]$|\n", "|$\\mathit{z0}$|$\\mathit{b}$|$\\mathit{b}$|$\\mathit{z0}$|$[]$|\n", "|$\\mathit{z0}$|$\\mathit{S}$|$\\mathit{S}$|$\\mathit{z0}$|$[]$|\n", "|$\\mathit{z0}$|$\\mathit{C}$|$\\mathit{C}$|$\\mathit{z0}$|$[]$|\n", "|$\\mathit{z0}$|$\\mathit{lambda}$|$\\mathit{S}$|$\\mathit{z0}$|$[C]$|\n", "|$\\mathit{z0}$|$\\mathit{lambda}$|$\\mathit{S}$|$\\mathit{z0}$|$[a,\\mathit{S},b]$|\n", "|$\\mathit{z0}$|$\\mathit{lambda}$|$\\mathit{C}$|$\\mathit{z0}$|$[a,b]$|\n", "|$\\mathit{z0}$|$\\mathit{lambda}$|$\\mathit{lambda}$|$\\mathit{z0}$|$[]$|\n"  Michael Leuschel committed Jun 02, 2020 834 835 836  ], "text/plain": [ "z\tx\tX\tz2\tXs\n",  Michael Leuschel committed Jun 03, 2020 837 838 839 840 841 842 843 844  "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[C]\n", "z0\tlambda\tS\tz0\t[a,S,b]\n", "z0\tlambda\tC\tz0\t[a,b]\n", "z0\tlambda\tlambda\tz0\t[]\n"  Michael Leuschel committed Jun 02, 2020 845 846  ] },  Chris committed Nov 07, 2020 847  "execution_count": 26,  Michael Leuschel committed Jun 02, 2020 848 849 850 851 852 853 854 855 856 857  "metadata": {}, "output_type": "execute_result" } ], "source": [ ":table {z,x,X,z2,Xs| ((z,x,X)↦(z2,Xs)) : δ}" ] }, { "cell_type": "code",  Chris committed Nov 07, 2020 858  "execution_count": 27,  Michael Leuschel committed Jun 02, 2020 859 860 861 862 863 864 865 866 867 868 869 870 871 872 873 874 875 876 877 878 879 880 881 882 883 884 885 886 887 888 889 890 891  "metadata": {}, "outputs": [ { "data": { "text/markdown": [ "
z: z0
α:aabb
γ:S
\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "" ], "text/plain": [ "" ] },  Chris committed Nov 07, 2020 892  "execution_count": 27,  Michael Leuschel committed Jun 02, 2020 893 894 895 896 897 898 899 900 901 902  "metadata": {}, "output_type": "execute_result" } ], "source": [ ":show" ] }, { "cell_type": "code",  Chris committed Nov 07, 2020 903  "execution_count": 28,  Michael Leuschel committed Jun 02, 2020 904 905 906 907 908  "metadata": {}, "outputs": [ { "data": { "text/plain": [  Michael Leuschel committed Jun 03, 2020 909  "Machine: PDA_für_kfG\n",  Michael Leuschel committed Jun 02, 2020 910 911 912 913  "Sets: Z, SYMBOLE\n", "Constants: P, δ\n", "Variables: z, α, γ\n", "Operations: \n",  Michael Leuschel committed Jun 03, 2020 914 915  "LambdaSchritt(z0,[C])\n", "LambdaSchritt(z0,[a,S,b])"  Michael Leuschel committed Jun 02, 2020 916 917  ] },  Chris committed Nov 07, 2020 918  "execution_count": 28,  Michael Leuschel committed Jun 02, 2020 919 920 921 922 923 924 925 926 927 928  "metadata": {}, "output_type": "execute_result" } ], "source": [ ":browse" ] }, { "cell_type": "code",  Chris committed Nov 07, 2020 929  "execution_count": 29,  Michael Leuschel committed Jun 02, 2020 930 931 932 933 934  "metadata": {}, "outputs": [ { "data": { "text/plain": [  Michael Leuschel committed Jun 03, 2020 935  "Executed operation: LambdaSchritt(z0,[a,S,b])"  Michael Leuschel committed Jun 02, 2020 936 937  ] },  Chris committed Nov 07, 2020 938  "execution_count": 29,  Michael Leuschel committed Jun 02, 2020 939 940 941 942 943 944 945 946 947 948  "metadata": {}, "output_type": "execute_result" } ], "source": [ ":exec LambdaSchritt s = [a,S,b]" ] }, { "cell_type": "code",  Chris committed Nov 07, 2020 949  "execution_count": 30,  Michael Leuschel committed Jun 02, 2020 950 951 952 953 954 955 956 957 958 959 960 961 962 963 964 965 966 967 968 969 970 971 972 973 974 975 976 977 978 979 980 981 982  "metadata": {}, "outputs": [ { "data": { "text/markdown": [ "
z: z0
α:aabb
γ:aSb
\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "" ], "text/plain": [ "" ] },  Chris committed Nov 07, 2020 983  "execution_count": 30,  Michael Leuschel committed Jun 02, 2020 984 985 986 987 988 989 990 991 992 993  "metadata": {}, "output_type": "execute_result" } ], "source": [ ":show" ] }, { "cell_type": "code",  Chris committed Nov 07, 2020 994  "execution_count": 31,  Michael Leuschel committed Jun 02, 2020 995 996 997 998 999  "metadata": {}, "outputs": [ { "data": { "text/plain": [  Michael Leuschel committed Jun 03, 2020 1000  "Machine: PDA_für_kfG\n", 
For faster browsing, not all history is shown.