Commit 56305031 authored by Michael Leuschel's avatar Michael Leuschel
Browse files

Merge branch 'master' into 'master'

Master

See merge request !1
parents bcb84193 3047fa72
/info4/kapitel-*/.ipynb_checkpoints
/info4/kapitel-*/exports
/info4/kapitel-*/*/__pycache__/
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
{
"cells": [
{
"cell_type": "markdown",
"metadata": {},
"source": [
"# Das (spezielle) Halteproblem\n",
"\n",
"Im Skript wird das Halteproblem formal definiert. Hier wollen wir das Halteproblem einmal intuitiv betrachten.\n",
"\n",
"Intuitiv gesehen stellt man beim speziellen Halteproblem die Frage, ob eine Turingmaschiene hält, wenn Sie sich selbst als eine Eingabe erhält.\n",
"Um Turingmaschienen als Eingaben nutzen zu können benötigen wir eine Darstellung als Wörter über einem Alphabet. Als Alphabet wählen wir $\\Sigma$ = {0, 1} und als Möglichkeit eine TM über $\\Sigma$ darzustellen wählen wir die Gödelisierung. Die genau Definition finden Sie im Skript auf Seite 153 (zwischen Korrolar 10.18 und Beispiel 10.19). Für unsere Zwecke reicht es allerdings aus zu verstehen, dass mit der Gödelisierung jeder TM ein Wort aus $\\Sigma^*$ zugeordet wird. Auf Grund der Art der Gödelisierung gilt die Umkehrung allerdings nicht. Um die Umkehrabbildung angeben zu können sei $M_0$ eine beliebige feste TM. Dann ist für jedes Wort $w\\in\\Sigma^*$ eine TM $M_w$ definiert durch:\n",
"\n",
"$M_w$ = M, falls w = code(M)\n",
"\n",
"$M_w$ = $M_0$, sonst\n",
"\n",
"Mit dieser Definition lässt sich das spezielle Halteproblem definieren als:\n",
"$K=\\{w\\in\\{0,1\\}^* | \\text{$M_w$ angesetzt auf w hält nach endlich vielen Schritten}\\}$\n",
"\n",
"Nun zeigen wir, dass K nicht entscheidbar ist, es also keine TM gibt, die für jedes $x\\in\\Sigma^*$ entscheidet, ob es in K liegt oder nicht. Für einen Wiederspruchsbeweis nehmen wir an, dass K entscheidbar wäre.\n",
"\n",
"Sei H dann die TM, die für alle x entscheided, ob x in K liegt oder nicht.\n",
"Wenn also die TM M mit code(M)=x hält, dann gibt H bei der Eingabe x 1 und sonst 0 aus.\n",
"\n",
"Sei nun N eine TM, die bei der Eingabe 1 in eine Endlosschleife läuft und bei der Eingabe 0 eine 1 ausgibt.\n",
"\n",
"Betrachten wir nun die TM C, die aus der Hintereinanderschaltung von H und N entsteht.\n",
"Wenn wir C auf die Gödelisierung einer TM anwenden, die mit sich selbst als Eingabe hält, dann gibt H eine 1 aus und somit hält N nicht an. Damit hält auch C nicht.\n",
"Und wenn wir C auf die Gödelisierung einer TM anwenden, die in eine Endlosschleife läuft, wenn Sie sich selbst als Eingabe erhält, dann gibt H eine O aus und somit N eine 1 und C hält.\n",
"\n",
"Wenn wir nun C auf sich selbst anwenden, was geschieht dann?\n",
"Angenommen C hält, dann gibt H eine 1 aus und N läuft in eine Endlosschleife. Daher hält C nicht.\n",
"Wenn C allerdings in eine Endlosschleife läuft, dann gibt H eine 0 aus und somit N eine 1. Damit hält C.\n",
"Dies ist ein Wiederspruch dazu, dass K entscheidbar ist."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"<table align=\"LEFT\">\n",
" <tr>\n",
" <td width=50%><center>Die Turingmaschiene $H$</center></td>\n",
" <td width=50%><center>Die Turingmaschiene $N$</center></td>\n",
" </tr>\n",
" <tr>\n",
" <td width=50% align=\"CENTER\"><img src=\"./img/TM H.svg\" width=100%></td>\n",
" <td width=50%><img src=\"./img/TM N.svg\" width=100%></td>\n",
" </tr>\n",
" <tr>\n",
" <td width=100% colspan=2><center>Die Turingmaschiene $C$</center></td>\n",
" </tr>\n",
" <tr>\n",
" <td width=100% colspan=2><img src=\"./img/TM C2.svg\" width=100%></td>\n",
" </tr>\n",
"</table>"
]
},
{
"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": 4
}
<svg width="1174" height="282" xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink" overflow="hidden"><defs><clipPath id="clip0"><rect x="59" y="219" width="1174" height="282"/></clipPath></defs><g clip-path="url(#clip0)" transform="translate(-59 -219)"><rect x="261.5" y="235.5" width="271" height="249" stroke="#000000" stroke-width="1.33333" stroke-miterlimit="8" fill="none"/><path d="M0.0236198-1.99986 94.3379-0.885938 94.2907 3.11378-0.0236198 1.99986ZM92.3853-4.90928 104.314 1.23202 92.2436 7.08988Z" transform="matrix(1 0 0 -1 154 360.232)"/><text font-family="Calibri,Calibri_MSFontService,sans-serif" font-weight="400" font-size="16" transform="translate(171.552 355)">code(M) für<tspan x="0" y="19">eine TM M</tspan></text><path d="M532.72 302.134 670.737 355.422 669.296 359.154 531.28 305.866ZM670.312 350.97 679.345 360.89 665.99 362.165Z"/><path d="M0.669392-1.88465 138.591 47.1025 137.252 50.8718-0.669392 1.88465ZM138.045 42.6639 147.345 52.3342 134.029 53.9718Z" transform="matrix(1 0 0 -1 532 411.334)"/><text font-family="Calibri,Calibri_MSFontService,sans-serif" font-weight="400" font-size="15" transform="translate(547.106 264)">1, falls M bei <tspan x="0" y="17">Eingabe code(M) </tspan><tspan x="0" y="35">hält</tspan><tspan font-size="16" x="2.59369" y="157">0, sonst</tspan><tspan font-size="24" x="-269.068" y="12">Die TM H</tspan></text><path d="M948 448.5C948 428.894 958.521 413 971.5 413 984.479 413 995 428.894 995 448.5 995 468.106 984.479 484 971.5 484 958.521 484 948 468.106 948 448.5Z" stroke="#000000" stroke-width="4" stroke-miterlimit="8" fill="none" fill-rule="evenodd"/><rect x="678.5" y="249.5" width="277" height="231" stroke="#000000" stroke-width="1.33333" stroke-miterlimit="8" fill="#FFFFFF"/><path d="M955 311 1109.12 311 1109.12 315 955 315ZM1107.12 307 1119.12 313 1107.12 319Z"/><text font-family="Calibri,Calibri_MSFontService,sans-serif" font-weight="400" font-size="16" transform="translate(972.277 300)">1, falls die <tspan x="0" y="38">Eingabe 0 ist</tspan><tspan x="31.9123" y="142">Endlosschleife, </tspan><tspan x="31.9123" y="161">sonst</tspan><tspan font-size="24" x="-276.951" y="-11">Die TM N</tspan></text><path d="M956.183 485.364 955 472 966.401 479.072Z"/><rect x="161.5" y="220.5" width="958" height="280" stroke="#2F528F" stroke-width="1.33333" stroke-miterlimit="8" fill="none"/><path d="M60 358 151.027 358 151.027 362 60 362ZM149.027 354 161.027 360 149.027 366Z"/><path d="M1119 311 1210.03 311 1210.03 315 1119 315ZM1208.03 307 1220.03 313 1208.03 319Z"/></g></svg>
\ No newline at end of file
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE svg PUBLIC "-//W3C//DTD SVG 1.1//EN" "http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd">
<svg version="1.2" width="310.89mm" height="74.88mm" viewBox="0 0 31089 7488" preserveAspectRatio="xMidYMid" fill-rule="evenodd" stroke-width="28.222" stroke-linejoin="round" xmlns="http://www.w3.org/2000/svg" xmlns:ooo="http://xml.openoffice.org/svg/export" xmlns:xlink="http://www.w3.org/1999/xlink" xmlns:presentation="http://sun.com/xmlns/staroffice/presentation" xmlns:smil="http://www.w3.org/2001/SMIL20/" xmlns:anim="urn:oasis:names:tc:opendocument:xmlns:animation:1.0" xml:space="preserve">
<defs class="ClipPathGroup">
<clipPath id="presentation_clip_path" clipPathUnits="userSpaceOnUse">
<rect x="0" y="0" width="31089" height="7488"/>
</clipPath>
<clipPath id="presentation_clip_path_shrink" clipPathUnits="userSpaceOnUse">
<rect x="31" y="7" width="31027" height="7474"/>
</clipPath>
</defs>
<defs>
<font id="EmbeddedFont_1" horiz-adv-x="2048">
<font-face font-family="Calibri embedded" units-per-em="2048" font-weight="normal" font-style="normal" ascent="1879" descent="476"/>
<missing-glyph horiz-adv-x="2048" d="M 0,0 L 2047,0 2047,2047 0,2047 0,0 Z"/>
<glyph unicode="ü" horiz-adv-x="953" d="M 174,442 L 174,1120 358,1120 358,449 C 358,343 379,264 420,211 461,158 523,131 606,131 705,131 784,163 842,226 899,289 928,376 928,485 L 928,1120 1112,1120 1112,0 928,0 928,172 C 883,104 832,54 773,21 714,-12 645,-29 567,-29 438,-29 341,11 274,91 207,171 174,288 174,442 Z M 729,1552 L 932,1552 932,1350 729,1350 729,1552 Z M 338,1552 L 541,1552 541,1350 338,1350 338,1552 Z"/>
<glyph unicode="ä" horiz-adv-x="980" d="M 702,563 C 553,563 450,546 393,512 336,478 307,420 307,338 307,273 329,221 372,183 415,144 473,125 547,125 649,125 731,161 793,234 854,306 885,402 885,522 L 885,563 702,563 Z M 1069,639 L 1069,0 885,0 885,170 C 843,102 791,52 728,20 665,-13 589,-29 498,-29 383,-29 292,3 225,68 157,132 123,218 123,326 123,452 165,547 250,611 334,675 460,707 627,707 L 885,707 885,725 C 885,810 857,875 802,922 746,968 668,991 567,991 503,991 441,983 380,968 319,953 261,930 205,899 L 205,1069 C 272,1095 338,1115 401,1128 464,1141 526,1147 586,1147 748,1147 869,1105 949,1021 1029,937 1069,810 1069,639 Z M 688,1552 L 891,1552 891,1350 688,1350 688,1552 Z M 297,1552 L 500,1552 500,1350 297,1350 297,1552 Z"/>
<glyph unicode="t" horiz-adv-x="715" d="M 375,1438 L 375,1120 754,1120 754,977 375,977 375,369 C 375,278 388,219 413,193 438,167 488,154 565,154 L 754,154 754,0 565,0 C 423,0 325,27 271,80 217,133 190,229 190,369 L 190,977 55,977 55,1120 190,1120 190,1438 375,1438 Z"/>
<glyph unicode="s" horiz-adv-x="874" d="M 907,1087 L 907,913 C 855,940 801,960 745,973 689,986 631,993 571,993 480,993 411,979 366,951 320,923 297,881 297,825 297,782 313,749 346,725 379,700 444,677 543,655 L 606,641 C 737,613 830,574 885,523 940,472 967,400 967,309 967,205 926,123 844,62 761,1 648,-29 504,-29 444,-29 382,-23 317,-12 252,0 183,18 111,41 L 111,231 C 179,196 246,169 312,152 378,134 443,125 508,125 595,125 661,140 708,170 755,199 778,241 778,295 778,345 761,383 728,410 694,437 620,462 506,487 L 442,502 C 328,526 246,563 195,613 144,662 119,730 119,817 119,922 156,1004 231,1061 306,1118 412,1147 549,1147 617,1147 681,1142 741,1132 801,1122 856,1107 907,1087 Z"/>
<glyph unicode="r" horiz-adv-x="663" d="M 842,948 C 821,960 799,969 775,975 750,980 723,983 694,983 590,983 510,949 455,882 399,814 371,717 371,590 L 371,0 186,0 186,1120 371,1120 371,946 C 410,1014 460,1065 522,1098 584,1131 659,1147 748,1147 761,1147 775,1146 790,1145 805,1143 822,1140 841,1137 L 842,948 Z"/>
<glyph unicode="o" horiz-adv-x="1033" d="M 627,991 C 528,991 450,953 393,876 336,799 307,693 307,559 307,425 336,320 393,243 450,166 528,127 627,127 725,127 803,166 860,243 917,320 946,426 946,559 946,692 917,797 860,875 803,952 725,991 627,991 Z M 627,1147 C 787,1147 913,1095 1004,991 1095,887 1141,743 1141,559 1141,376 1095,232 1004,128 913,23 787,-29 627,-29 466,-29 341,23 250,128 159,232 113,376 113,559 113,743 159,887 250,991 341,1095 466,1147 627,1147 Z"/>
<glyph unicode="n" horiz-adv-x="954" d="M 1124,676 L 1124,0 940,0 940,670 C 940,776 919,855 878,908 837,961 775,987 692,987 593,987 514,955 457,892 400,829 371,742 371,633 L 371,0 186,0 186,1120 371,1120 371,946 C 415,1013 467,1064 527,1097 586,1130 655,1147 733,1147 862,1147 959,1107 1025,1028 1091,948 1124,831 1124,676 Z"/>
<glyph unicode="l" horiz-adv-x="213" d="M 193,1556 L 377,1556 377,0 193,0 193,1556 Z"/>
<glyph unicode="i" horiz-adv-x="213" d="M 193,1120 L 377,1120 377,0 193,0 193,1120 Z M 193,1556 L 377,1556 377,1323 193,1323 193,1556 Z"/>
<glyph unicode="h" horiz-adv-x="954" d="M 1124,676 L 1124,0 940,0 940,670 C 940,776 919,855 878,908 837,961 775,987 692,987 593,987 514,955 457,892 400,829 371,742 371,633 L 371,0 186,0 186,1556 371,1556 371,946 C 415,1013 467,1064 527,1097 586,1130 655,1147 733,1147 862,1147 959,1107 1025,1028 1091,948 1124,831 1124,676 Z"/>
<glyph unicode="g" horiz-adv-x="1006" d="M 930,573 C 930,706 903,810 848,883 793,956 715,993 616,993 517,993 441,956 386,883 331,810 303,706 303,573 303,440 331,337 386,264 441,191 517,154 616,154 715,154 793,191 848,264 903,337 930,440 930,573 Z M 1114,139 C 1114,-52 1072,-193 987,-287 902,-379 773,-426 598,-426 533,-426 472,-421 415,-412 358,-402 302,-387 248,-367 L 248,-188 C 302,-217 355,-239 408,-253 461,-267 514,-274 569,-274 690,-274 780,-242 840,-180 900,-116 930,-21 930,106 L 930,197 C 892,131 843,82 784,49 725,16 654,0 571,0 434,0 323,52 239,157 155,262 113,400 113,573 113,746 155,885 239,990 323,1095 434,1147 571,1147 654,1147 725,1131 784,1098 843,1065 892,1016 930,950 L 930,1120 1114,1120 1114,139 Z"/>
<glyph unicode="f" horiz-adv-x="742" d="M 760,1556 L 760,1403 584,1403 C 518,1403 472,1390 447,1363 421,1336 408,1288 408,1219 L 408,1120 711,1120 711,977 408,977 408,0 223,0 223,977 47,977 47,1120 223,1120 223,1198 C 223,1323 252,1414 310,1471 368,1528 460,1556 586,1556 L 760,1556 Z"/>
<glyph unicode="e" horiz-adv-x="1059" d="M 1151,606 L 1151,516 305,516 C 313,389 351,293 420,227 488,160 583,127 705,127 776,127 844,136 911,153 977,170 1043,196 1108,231 L 1108,57 C 1042,29 974,8 905,-7 836,-22 765,-29 694,-29 515,-29 374,23 270,127 165,231 113,372 113,549 113,732 163,878 262,986 361,1093 494,1147 662,1147 813,1147 932,1099 1020,1002 1107,905 1151,773 1151,606 Z M 967,659 C 966,760 938,841 883,901 828,961 755,991 664,991 561,991 479,962 418,904 356,846 320,764 311,659 L 967,659 Z"/>
<glyph unicode="d" horiz-adv-x="1006" d="M 930,950 L 930,1556 1114,1556 1114,0 930,0 930,168 C 891,101 843,52 784,20 725,-13 654,-29 571,-29 436,-29 326,25 241,133 156,241 113,383 113,559 113,735 156,877 241,985 326,1093 436,1147 571,1147 654,1147 725,1131 784,1099 843,1066 891,1017 930,950 Z M 303,559 C 303,424 331,318 387,241 442,164 519,125 616,125 713,125 790,164 846,241 902,318 930,424 930,559 930,694 902,801 846,878 790,955 713,993 616,993 519,993 442,955 387,878 331,801 303,694 303,559 Z"/>
<glyph unicode="c" horiz-adv-x="900" d="M 999,1077 L 999,905 C 947,934 895,955 843,970 790,984 737,991 684,991 565,991 472,953 406,878 340,802 307,696 307,559 307,422 340,316 406,241 472,165 565,127 684,127 737,127 790,134 843,149 895,163 947,184 999,213 L 999,43 C 948,19 895,1 840,-11 785,-23 726,-29 664,-29 495,-29 361,24 262,130 163,236 113,379 113,559 113,742 163,885 264,990 364,1095 501,1147 676,1147 733,1147 788,1141 842,1130 896,1118 948,1100 999,1077 Z"/>
<glyph unicode="b" horiz-adv-x="1007" d="M 997,559 C 997,694 969,801 914,878 858,955 781,993 684,993 587,993 510,955 455,878 399,801 371,694 371,559 371,424 399,318 455,241 510,164 587,125 684,125 781,125 858,164 914,241 969,318 997,424 997,559 Z M 371,950 C 410,1017 459,1066 518,1099 577,1131 647,1147 729,1147 865,1147 976,1093 1061,985 1146,877 1188,735 1188,559 1188,383 1146,241 1061,133 976,25 865,-29 729,-29 647,-29 577,-13 518,20 459,52 410,101 371,168 L 371,0 186,0 186,1556 371,1556 371,950 Z"/>
<glyph unicode="a" horiz-adv-x="980" d="M 702,563 C 553,563 450,546 393,512 336,478 307,420 307,338 307,273 329,221 372,183 415,144 473,125 547,125 649,125 731,161 793,234 854,306 885,402 885,522 L 885,563 702,563 Z M 1069,639 L 1069,0 885,0 885,170 C 843,102 791,52 728,20 665,-13 589,-29 498,-29 383,-29 292,3 225,68 157,132 123,218 123,326 123,452 165,547 250,611 334,675 460,707 627,707 L 885,707 885,725 C 885,810 857,875 802,922 746,968 668,991 567,991 503,991 441,983 380,968 319,953 261,930 205,899 L 205,1069 C 272,1095 338,1115 401,1128 464,1141 526,1147 586,1147 748,1147 869,1105 949,1021 1029,937 1069,810 1069,639 Z"/>
<glyph unicode="T" horiz-adv-x="1297" d="M -6,1493 L 1257,1493 1257,1323 727,1323 727,0 524,0 524,1323 -6,1323 -6,1493 Z"/>
<glyph unicode="N" horiz-adv-x="1165" d="M 201,1493 L 473,1493 1135,244 1135,1493 1331,1493 1331,0 1059,0 397,1249 397,0 201,0 201,1493 Z"/>
<glyph unicode="M" horiz-adv-x="1377" d="M 201,1493 L 502,1493 883,477 1266,1493 1567,1493 1567,0 1370,0 1370,1311 985,287 782,287 397,1311 397,0 201,0 201,1493 Z"/>
<glyph unicode="H" horiz-adv-x="1165" d="M 201,1493 L 403,1493 403,881 1137,881 1137,1493 1339,1493 1339,0 1137,0 1137,711 403,711 403,0 201,0 201,1493 Z"/>
<glyph unicode="E" horiz-adv-x="980" d="M 201,1493 L 1145,1493 1145,1323 403,1323 403,881 1114,881 1114,711 403,711 403,170 1163,170 1163,0 201,0 201,1493 Z"/>
<glyph unicode="D" horiz-adv-x="1271" d="M 403,1327 L 403,166 647,166 C 853,166 1004,213 1100,306 1195,399 1243,547 1243,748 1243,948 1195,1095 1100,1188 1004,1281 853,1327 647,1327 L 403,1327 Z M 201,1493 L 616,1493 C 905,1493 1118,1433 1253,1313 1388,1192 1456,1004 1456,748 1456,491 1388,302 1252,181 1116,60 904,0 616,0 L 201,0 201,1493 Z"/>
<glyph unicode="1" horiz-adv-x="900" d="M 254,170 L 584,170 584,1309 225,1237 225,1421 582,1493 784,1493 784,170 1114,170 1114,0 254,0 254,170 Z"/>
<glyph unicode="0" horiz-adv-x="1033" d="M 651,1360 C 547,1360 469,1309 417,1207 364,1104 338,950 338,745 338,540 364,387 417,285 469,182 547,131 651,131 756,131 834,182 887,285 939,387 965,540 965,745 965,950 939,1104 887,1207 834,1309 756,1360 651,1360 Z M 651,1520 C 818,1520 946,1454 1035,1322 1123,1189 1167,997 1167,745 1167,494 1123,302 1035,170 946,37 818,-29 651,-29 484,-29 356,37 268,170 179,302 135,494 135,745 135,997 179,1189 268,1322 356,1454 484,1520 651,1520 Z"/>
<glyph unicode="," horiz-adv-x="319" d="M 240,254 L 451,254 451,82 287,-238 158,-238 240,82 240,254 Z"/>
<glyph unicode=")" horiz-adv-x="477" d="M 164,1554 L 324,1554 C 424,1397 499,1243 549,1092 598,941 623,792 623,643 623,494 598,343 549,192 499,41 424,-113 324,-270 L 164,-270 C 253,-117 319,35 363,186 406,337 428,489 428,643 428,797 406,949 363,1099 319,1249 253,1401 164,1554 Z"/>
<glyph unicode="(" horiz-adv-x="477" d="M 635,1554 C 546,1401 479,1249 436,1099 393,949 371,797 371,643 371,489 393,337 437,186 480,35 546,-117 635,-270 L 475,-270 C 375,-113 300,41 251,192 201,343 176,494 176,643 176,792 201,941 250,1092 299,1243 374,1397 475,1554 L 635,1554 Z"/>
<glyph unicode=" " horiz-adv-x="635"/>
</font>
</defs>
<defs class="TextShapeIndex">
<g ooo:slide="id1" ooo:id-list="id3"/>
</defs>
<defs class="EmbeddedBulletChars">
<g id="bullet-char-template-57356" transform="scale(0.00048828125,-0.00048828125)">
<path d="M 580,1141 L 1163,571 580,0 -4,571 580,1141 Z"/>
</g>
<g id="bullet-char-template-57354" transform="scale(0.00048828125,-0.00048828125)">
<path d="M 8,1128 L 1137,1128 1137,0 8,0 8,1128 Z"/>
</g>
<g id="bullet-char-template-10146" transform="scale(0.00048828125,-0.00048828125)">
<path d="M 174,0 L 602,739 174,1481 1456,739 174,0 Z M 1358,739 L 309,1346 659,739 1358,739 Z"/>
</g>
<g id="bullet-char-template-10132" transform="scale(0.00048828125,-0.00048828125)">
<path d="M 2015,739 L 1276,0 717,0 1260,543 174,543 174,936 1260,936 717,1481 1274,1481 2015,739 Z"/>
</g>
<g id="bullet-char-template-10007" transform="scale(0.00048828125,-0.00048828125)">
<path d="M 0,-2 C -7,14 -16,27 -25,37 L 356,567 C 262,823 215,952 215,954 215,979 228,992 255,992 264,992 276,990 289,987 310,991 331,999 354,1012 L 381,999 492,748 772,1049 836,1024 860,1049 C 881,1039 901,1025 922,1006 886,937 835,863 770,784 769,783 710,716 594,584 L 774,223 C 774,196 753,168 711,139 L 727,119 C 717,90 699,76 672,76 641,76 570,178 457,381 L 164,-76 C 142,-110 111,-127 72,-127 30,-127 9,-110 8,-76 1,-67 -2,-52 -2,-32 -2,-23 -1,-13 0,-2 Z"/>
</g>
<g id="bullet-char-template-10004" transform="scale(0.00048828125,-0.00048828125)">
<path d="M 285,-33 C 182,-33 111,30 74,156 52,228 41,333 41,471 41,549 55,616 82,672 116,743 169,778 240,778 293,778 328,747 346,684 L 369,508 C 377,444 397,411 428,410 L 1163,1116 C 1174,1127 1196,1133 1229,1133 1271,1133 1292,1118 1292,1087 L 1292,965 C 1292,929 1282,901 1262,881 L 442,47 C 390,-6 338,-33 285,-33 Z"/>
</g>
<g id="bullet-char-template-9679" transform="scale(0.00048828125,-0.00048828125)">
<path d="M 813,0 C 632,0 489,54 383,161 276,268 223,411 223,592 223,773 276,916 383,1023 489,1130 632,1184 813,1184 992,1184 1136,1130 1245,1023 1353,916 1407,772 1407,592 1407,412 1353,268 1245,161 1136,54 992,0 813,0 Z"/>
</g>
<g id="bullet-char-template-8226" transform="scale(0.00048828125,-0.00048828125)">
<path d="M 346,457 C 273,457 209,483 155,535 101,586 74,649 74,723 74,796 101,859 155,911 209,963 273,989 346,989 419,989 480,963 531,910 582,859 608,796 608,723 608,648 583,586 532,535 482,483 420,457 346,457 Z"/>
</g>
<g id="bullet-char-template-8211" transform="scale(0.00048828125,-0.00048828125)">
<path d="M -4,459 L 1135,459 1135,606 -4,606 -4,459 Z"/>
</g>
<g id="bullet-char-template-61548" transform="scale(0.00048828125,-0.00048828125)">
<path d="M 173,740 C 173,903 231,1043 346,1159 462,1274 601,1332 765,1332 928,1332 1067,1274 1183,1159 1299,1043 1357,903 1357,740 1357,577 1299,437 1183,322 1067,206 928,148 765,148 601,148 462,206 346,322 231,437 173,577 173,740 Z"/>
</g>
</defs>
<g>
<g id="id2" class="Master_Slide">
<g id="bg-id2" class="Background"/>
<g id="bo-id2" class="BackgroundObjects"/>
</g>
</g>
<g class="SlideGroup">
<g>
<g id="container-id1">
<g id="id1" class="Slide" clip-path="url(#presentation_clip_path)">
<g class="Page">
<g class="Graphic">
<g id="id3">
<rect class="BoundingBox" stroke="none" fill="none" x="4700" y="1092" width="21693" height="5225"/>
<defs>
<clipPath id="clip_path_1" clipPathUnits="userSpaceOnUse">
<path d="M 4728,1117 L 26143,1117 26143,6307 4728,6307 4728,1117 Z"/>
</clipPath>
</defs>
<g clip-path="url(#clip_path_1)">
<path fill="none" stroke="rgb(0,0,0)" stroke-width="25" stroke-linejoin="miter" d="M 10949,6002 L 8448,6002 8448,1406 13451,1406 13451,6002 10949,6002 Z"/>
<path fill="rgb(0,0,0)" stroke="none" d="M 6463,3745 L 8168,3725 8169,3799 8389,3686 8166,3577 8167,3651 6463,3671 6463,3745 Z"/>
<text class="TextShape"><tspan class="TextParagraph" font-family="Calibri, sans-serif" font-size="295px" font-weight="400"><tspan class="TextPosition" x="6787" y="3612"><tspan fill="rgb(0,0,0)" stroke="none">code(M) für </tspan></tspan></tspan></text>
<text class="TextShape"><tspan class="TextParagraph" font-family="Calibri, sans-serif" font-size="295px" font-weight="400"><tspan class="TextPosition" x="6787" y="3962"><tspan fill="rgb(0,0,0)" stroke="none">eine TM M</tspan></tspan></tspan></text>
<path fill="rgb(0,0,0)" stroke="none" d="M 13455,2636 L 15968,3606 15995,3537 16162,3720 15915,3744 15942,3675 13428,2705 13455,2636 Z"/>
<path fill="rgb(0,0,0)" stroke="none" d="M 13454,4686 L 15965,3794 15990,3864 16162,3686 15916,3655 15940,3725 13429,4617 13454,4686 Z"/>
<text class="TextShape"><tspan class="TextParagraph" font-family="Calibri, sans-serif" font-size="277px" font-weight="400"><tspan class="TextPosition" x="13720" y="1932"><tspan fill="rgb(0,0,0)" stroke="none">1, falls M bei </tspan></tspan></tspan></text>
<text class="TextShape"><tspan class="TextParagraph" font-family="Calibri, sans-serif" font-size="277px" font-weight="400"><tspan class="TextPosition" x="13720" y="2246"><tspan fill="rgb(0,0,0)" stroke="none">Eingabe code(M) </tspan></tspan></tspan></text>
<text class="TextShape"><tspan class="TextParagraph" font-family="Calibri, sans-serif" font-size="277px" font-weight="400"><tspan class="TextPosition" x="13720" y="2578"><tspan fill="rgb(0,0,0)" stroke="none">hält </tspan></tspan></tspan></text>
<text class="TextShape"><tspan class="TextParagraph" font-family="Calibri, sans-serif" font-size="295px" font-weight="400"><tspan class="TextPosition" x="13768" y="4830"><tspan fill="rgb(0,0,0)" stroke="none">0, sonst </tspan></tspan></tspan></text>
<text class="TextShape"><tspan class="TextParagraph" font-family="Calibri, sans-serif" font-size="443px" font-weight="400"><tspan class="TextPosition" x="8753" y="2153"><tspan fill="rgb(0,0,0)" stroke="none">Die TM H</tspan></tspan></tspan></text>
<path fill="none" stroke="rgb(0,0,0)" stroke-width="74" stroke-linejoin="miter" d="M 21121,5338 C 21121,4976 21316,4682 21555,4682 21795,4682 21989,4976 21989,5338 21989,5700 21795,5993 21555,5993 21316,5993 21121,5700 21121,5338 Z"/>
<path fill="rgb(255,255,255)" stroke="none" d="M 18703,5928 L 16146,5928 16146,1664 21260,1664 21260,5928 18703,5928 Z"/>
<path fill="none" stroke="rgb(0,0,0)" stroke-width="25" stroke-linejoin="miter" d="M 18703,5928 L 16146,5928 16146,1664 21260,1664 21260,5928 18703,5928 Z"/>
<path fill="rgb(0,0,0)" stroke="none" d="M 21251,2799 L 24059,2799 24059,2726 24280,2836 24059,2947 24059,2873 21251,2873 21251,2799 Z"/>
<text class="TextShape"><tspan class="TextParagraph" font-family="Calibri, sans-serif" font-size="295px" font-weight="400"><tspan class="TextPosition" x="21569" y="2596"><tspan fill="rgb(0,0,0)" stroke="none">1, falls die </tspan></tspan></tspan></text>
<text class="TextShape"><tspan class="TextParagraph" font-family="Calibri, sans-serif" font-size="295px" font-weight="400"><tspan class="TextPosition" x="21569" y="3298"><tspan fill="rgb(0,0,0)" stroke="none">Eingabe 0 ist </tspan></tspan></tspan></text>
<text class="TextShape"><tspan class="TextParagraph" font-family="Calibri, sans-serif" font-size="295px" font-weight="400"><tspan class="TextPosition" x="22159" y="5218"><tspan fill="rgb(0,0,0)" stroke="none">Endlosschleife, </tspan></tspan></tspan></text>
<text class="TextShape"><tspan class="TextParagraph" font-family="Calibri, sans-serif" font-size="295px" font-weight="400"><tspan class="TextPosition" x="22159" y="5568"><tspan fill="rgb(0,0,0)" stroke="none">sonst </tspan></tspan></tspan></text>
<text class="TextShape"><tspan class="TextParagraph" font-family="Calibri, sans-serif" font-size="443px" font-weight="400"><tspan class="TextPosition" x="16457" y="2393"><tspan fill="rgb(0,0,0)" stroke="none">Die TM N</tspan></tspan></tspan></text>
<path fill="rgb(0,0,0)" stroke="none" d="M 21272,6018 L 21251,5771 21461,5902 21272,6018 Z"/>
<path fill="none" stroke="rgb(47,82,143)" stroke-width="25" stroke-linejoin="miter" d="M 15444,6298 L 6602,6298 6602,1129 24287,1129 24287,6298 15444,6298 Z"/>
<path fill="rgb(0,0,0)" stroke="none" d="M 4728,3667 L 6371,3667 6371,3593 6593,3704 6371,3815 6371,3741 4728,3741 4728,3667 Z"/>
<path fill="rgb(0,0,0)" stroke="none" d="M 24278,2799 L 25922,2799 25922,2726 26143,2836 25922,2947 25922,2873 24278,2873 24278,2799 Z"/>
</g>
</g>
</g>
</g>
</g>
</g>
</g>
</g>
</svg>
\ No newline at end of file
<svg width="853" height="234" xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink" overflow="hidden"><defs><clipPath id="clip0"><rect x="162" y="141" width="853" height="234"/></clipPath></defs><g clip-path="url(#clip0)" transform="translate(-162 -141)"><rect x="319.5" y="143.5" width="443" height="230" stroke="#000000" stroke-width="1.33333" stroke-miterlimit="8" fill="none"/><path d="M168 256 309.486 256 309.486 260 168 260ZM307.486 252 319.486 258 307.486 264Z"/><text font-family="Calibri,Calibri_MSFontService,sans-serif" font-weight="400" font-size="24" transform="translate(177.101 236)">code(M) für<tspan x="0" y="58">eine TM M</tspan></text><path d="M762 205 992.359 205 992.359 209 762 209ZM990.359 201 1002.36 207 990.359 213Z"/><path d="M762 304 992.359 304 992.359 308 762 308ZM990.359 300 1002.36 306 990.359 312Z"/><text font-family="Calibri,Calibri_MSFontService,sans-serif" font-weight="400" font-size="24" transform="translate(783.855 185)">1, falls M bei Eingabe<tspan x="0" y="58">code(M) hält</tspan><tspan x="6.10352e-05" y="101">0, sonst</tspan><tspan x="-443.153" y="-2">Die TM H</tspan></text></g></svg>
\ No newline at end of file
<svg width="1160" height="282" xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink" overflow="hidden"><defs><clipPath id="clip0"><rect x="59" y="219" width="1160" height="282"/></clipPath></defs><g clip-path="url(#clip0)" transform="translate(-59 -219)"><rect x="261.5" y="235.5" width="271" height="249" stroke="#000000" stroke-width="1.33333" stroke-miterlimit="8" fill="none"/><path d="M0.0236198-1.99986 94.3379-0.885938 94.2907 3.11378-0.0236198 1.99986ZM92.3853-4.90928 104.314 1.23202 92.2436 7.08988Z" transform="matrix(1 0 0 -1 161 360.232)"/><text font-family="Calibri,Calibri_MSFontService,sans-serif" font-weight="400" font-size="16" transform="translate(178.04 355)">code(M) für<tspan x="0" y="19">eine TM M</tspan></text><path d="M532.72 302.134 670.737 355.422 669.296 359.154 531.28 305.866ZM670.312 350.97 679.345 360.89 665.99 362.165Z"/><path d="M0.669392-1.88465 138.591 47.1025 137.252 50.8718-0.669392 1.88465ZM138.045 42.6639 147.345 52.3342 134.029 53.9718Z" transform="matrix(1 0 0 -1 532 411.334)"/><text font-family="Calibri,Calibri_MSFontService,sans-serif" font-weight="400" font-size="15" transform="translate(549.699 270)">1, falls M bei <tspan x="0" y="17">Eingabe code(M) </tspan><tspan x="0" y="35">hält</tspan><tspan font-size="16" x="-0.000183105" y="151">0, sonst</tspan><tspan font-size="24" x="-271.662" y="6">Die TM H</tspan></text><path d="M948 448.5C948 428.894 958.521 413 971.5 413 984.479 413 995 428.894 995 448.5 995 468.106 984.479 484 971.5 484 958.521 484 948 468.106 948 448.5Z" stroke="#000000" stroke-width="4" stroke-miterlimit="8" fill="none" fill-rule="evenodd"/><rect x="678.5" y="249.5" width="277" height="231" stroke="#000000" stroke-width="1.33333" stroke-miterlimit="8" fill="#FFFFFF"/><path d="M955 311 1094.83 311 1094.83 315 955 315ZM1092.83 307 1104.83 313 1092.83 319Z"/><text font-family="Calibri,Calibri_MSFontService,sans-serif" font-weight="400" font-size="16" transform="translate(972.277 300)">1, falls die <tspan x="0" y="38">Eingabe 0 ist</tspan><tspan x="31.9123" y="142">Endlosschleife, </tspan><tspan x="31.9123" y="161">sonst</tspan><tspan font-size="24" x="-276.951" y="-11">Die TM N</tspan></text><path d="M956.183 485.364 955 472 966.401 479.072Z"/><rect x="161.5" y="220.5" width="944" height="280" stroke="#2F528F" stroke-width="1.33333" stroke-miterlimit="8" fill="none"/><path d="M60 358 151.027 358 151.027 362 60 362ZM149.027 354 161.027 360 149.027 366Z"/><path d="M1105 313 1196.03 313 1196.03 317 1105 317ZM1194.03 309 1206.03 315 1194.03 321Z"/></g></svg>
\ No newline at end of file
<svg width="838" height="243" xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink" overflow="hidden"><defs><clipPath id="clip0"><rect x="162" y="141" width="838" height="243"/></clipPath></defs><g clip-path="url(#clip0)" transform="translate(-162 -141)"><path d="M750 342C750 322.67 766.789 307 787.5 307 808.211 307 825 322.67 825 342 825 361.33 808.211 377 787.5 377 766.789 377 750 361.33 750 342Z" stroke="#000000" stroke-width="4" stroke-miterlimit="8" fill="none" fill-rule="evenodd"/><rect x="319.5" y="143.5" width="443" height="230" stroke="#000000" stroke-width="1.33333" stroke-miterlimit="8" fill="#FFFFFF"/><path d="M0.0195984-1.9999 141.506-0.613381 141.467 3.38643-0.0195984 1.9999ZM139.546-4.63279 151.486 1.48451 139.428 7.36664Z" transform="matrix(1 0 0 -1 168 259.485)"/><text font-family="Calibri,Calibri_MSFontService,sans-serif" font-weight="400" font-size="24" transform="translate(177.101 236)">0 oder 1</text><path d="M1.05382e-06-2 189.249-1.9999 189.249 2.0001-1.05382e-06 2ZM187.249-5.9999 199.249 0.000104987 187.249 6.0001Z" transform="matrix(1 0 0 -1 762 207)"/><text font-family="Calibri,Calibri_MSFontService,sans-serif" font-weight="400" font-size="24" transform="translate(783.855 185)">1, falls die <tspan x="0" y="58">Eingabe 0 ist</tspan><tspan x="50.6421" y="149">Endlosschleife, </tspan><tspan x="50.6421" y="178">sonst</tspan><tspan x="-443.153" y="-2">Die TM N</tspan></text><path d="M766.143 377.761 762 365 774.694 369.342Z"/></g></svg>
\ No newline at end of file
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
{
"cells": [
{
"cell_type": "markdown",
"metadata": {},
"source": [
"# Der Satz von Myhill und Nerode\n",
"Wir betrachten die Myhill-Nerode-Äquivalenzrelation anhand der Sprache L = {a, b, aa, bb, aac, bbc, ccc}."
]
},
{
"cell_type": "code",
"execution_count": 1,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"Loaded machine: EquivalenceRelation"
]
},
"execution_count": 1,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"MACHINE EquivalenceRelation\n",
"/* Ein Modell der Myhill-Nerode Äquivalenzrelation R_L,\n",
" der entsprechenden Äquivalenzklassen und dem Index der Sprache.*/\n",
"SETS\n",
" Alphabet = {a,b,c}\n",
"CONSTANTS L, RL, maxsize, All, Classes, index\n",
"DEFINITIONS\n",
" class(x) == {y | x↦y : RL} ;\n",
" ANIMATION_FUNCTION1 == {r,c,i |r=1 ∧ c∈ dom(word) ∧ i=word(c)};\n",
" ANIMATION_FUNCTION2 == {r,c,i |r=2 ∧ c=1 ∧ i=z};\n",
" ANIMATION_FUNCTION3 == {(1, 0, \"Wort:\"), (2, 0, \"Äquivalenzklasse:\")};\n",
" \n",
"PROPERTIES\n",
" L ⊆ seq(Alphabet) ∧\n",
" \n",
" // All = {z | z∈seq(Alphabet) ∧ size(z)<=maxsz} & /* beschränkt auf endliche Folgen */\n",
" All = UNION(ii).(ii:0..maxsize| (1..ii) --> Alphabet) ∧\n",
"\n",
" RL = ({x,y| x∈All ∧ y∈All ∧ ∀z.(z∈All ⇒ ( x^z ∈ L ⇔ y^z ∈ L))}) ∧\n",
"\n",
" L = {[a],[b],[a,a],[b,b],[a,a,c],[b,b,c],[c,c,c]} ∧ maxsize = 3 ∧\n",
"\n",
" Classes = ran( %x.(x∈All|class(x))) ∧ /* Menge der Äquivalenzklassen {class(x)|x∈All} */\n",
" index = card( Classes ) \n",
"\n",
"ASSERTIONS\n",
" /* Test ob wir eine Äquivalenzrelation haben: */\n",
" ∀x.(x∈All ⇒ x↦x ∈ RL); /* Reflexivität */\n",
" ∀(x,y).(x↦y ∈ RL ⇒ y↦x ∈ RL); /* Symetrie */\n",
" ∀(x,y,z).(x↦y ∈ RL ∧ y↦z ∈ RL ⇒ x↦z ∈ RL); /* Transitivität */\n",
"\n",
" /* Einige Beispiele : */\n",
" [a,a] ↦ [b,b] ∈ RL;\n",
" [a,a] ↦ [c,c] ∉ RL;\n",
" [b,b,c] ↦ [c,c,c] ∈ RL;\n",
" class([a,a]) = {[a,a],[b,b]};\n",
" class([c,c,c]) = {[a,a,c],[b,b,c],[c,c,c]}\n",
"\n",
"/* Der durch die Äquivalenzklassen induzierte DFA: */\n",
"VARIABLES z, word\n",
"INVARIANT z ⊆ All ∧ word ∈ seq(Alphabet)\n",
"INITIALISATION z := class([]); word := []\n",
"OPERATIONS\n",
" Delta(terminal) = PRE terminal∈Alphabet THEN\n",
" ANY x WHERE x∈z ∧ ∀x2.(x2∈z ⇒ size(x2)≥size(x)) THEN\n",
" z := class(x^[terminal]);\n",
" word := word^[terminal]\n",
" END\n",
" END;\n",
" Final = SELECT z ∩ L ≠ {} THEN skip END\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/plain": [
"Machine initialised using operation 1: $initialise_machine()"
]
},
"execution_count": 3,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
":init"
]
},
{
"cell_type": "code",
"execution_count": 4,
"metadata": {
"scrolled": true
},
"outputs": [
{
"data": {
"text/markdown": [
"$8$"
],
"text/plain": [
"8"
]
},
"execution_count": 4,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"index"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Da der $Index(L)=8<\\infty$ ist die gegebene Sprache regulär."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Durch die Äquivalenzklassen wird ein Minimalautomat induziert.\n",
"Die Menge der Zustände ist gleich der Menge der Äquivalenzklassen.\n",
"Und nach dem Einlesen eines Wortes $w∈Σ^*$ landet man in dem Zustand, der der Äquivalenzklasse von $w$ bezüglich $R_L$ entspricht."
]
},
{
"cell_type": "code",
"execution_count": 5,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"Machine: EquivalenceRelation\n",
"Sets: Alphabet\n",
"Constants: L, RL, maxsize, All, Classes, index\n",
"Variables: z, word\n",
"Operations: \n",
"Delta(a)\n",
"Delta(b)\n",
"Delta(c)"
]
},
"execution_count": 5,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
":browse"
]
},
{
"cell_type": "code",
"execution_count": 6,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"Executed operation: Delta(a)"
]
},
"execution_count": 6,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
":exec Delta terminal=a"
]
},
{
"cell_type": "code",
"execution_count": 7,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"Executed operation: Delta(a)"
]
},
"execution_count": 7,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
":exec Delta terminal=a"
]
},
{
"cell_type": "code",
"execution_count": 8,
"metadata": {},
"outputs": [
{
"data": {
"text/markdown": [
"<table style=\"font-family:monospace\"><tbody>\n",
"<tr>\n",
"<td style=\"padding:10px\">Wort:</td>\n",
"<td style=\"padding:10px\">a</td>\n",
"<td style=\"padding:10px\">a</td>\n",
"</tr>\n",
"<tr>\n",
"<td style=\"padding:10px\">Äquivalenzklasse:</td>\n",
"<td style=\"padding:10px\">{{(1|->a),(2|->a)},{(1|->b),(2|->b)}}</td>\n",
"<td style=\"padding:0px\"></td>\n",
"</tr>\n",
"</tbody></table>"
],
"text/plain": [
"<Animation function visualisation>"
]
},
"execution_count": 8,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
":show"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Ein weiteres Beispiel ist die Sprache $L=\\{a^n | n\\geq0\\}$.\n"
]
},
{
"cell_type": "code",
"execution_count": 9,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"Loaded machine: EquivalenceRelation2"
]
},
"execution_count": 9,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"MACHINE EquivalenceRelation2\n",
"SETS\n",
" Alphabet = {a,b,c}\n",
"CONSTANTS L, RL, maxsize, All, Classes, index\n",
"DEFINITIONS\n",
" class(x) == {y | x↦y : RL} ;\n",
" \n",
"PROPERTIES\n",
" L ⊆ seq(Alphabet) ∧\n",
" \n",
" // All = {z | z∈seq(Alphabet) ∧ size(z)≤maxsize} & /* Beschränkt auf endliche Folgen */\n",
" All = UNION(ii).(ii:0..maxsize| (1..ii) --> Alphabet) ∧\n",
"\n",
" RL = ({x,y| x∈All ∧ y∈All ∧ ∀z.(z∈All ⇒ ( x^z ∈ L ⇔ y^z ∈ L))}) ∧\n",
"\n",
" /*L = {x | x=a^n ∧ size(x)≤maxsize} Beschränkt auf endliche Folgen*/ \n",
" L = UNION(ii).(ii:0..maxsize| (1..ii) --> {a}) ∧ maxsize = 3 ∧\n",
"\n",
" Classes = ran( %x.(x∈All|class(x))) ∧ /* Menge der Äquivalenzklassen {class(x)|x∈All} */\n",
" index = card( Classes )\n",
"END"
]
},
{
"cell_type": "code",
"execution_count": 10,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"Machine constants set up using operation 0: $setup_constants()"
]
},
"execution_count": 10,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
":constants"
]
},
{
"cell_type": "code",
"execution_count": 11,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"Machine initialised using operation 1: $initialise_machine()"
]
},
"execution_count": 11,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [