Neues Notebook zur Myhill-Nerode Äquivalenzrelation

info4/kapitel-2/Der Satz von Myhill und Nerode.ipynb

+{
+ "cells": [
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "# Der Satz von Myhill und Nerode"
+   ]
+  },
+  {
+   "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": "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": 4,
+   "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": 4,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":browse"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 5,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "Executed operation: Delta(a)"
+      ]
+     },
+     "execution_count": 5,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":exec Delta terminal=a"
+   ]
+  },
+  {
+   "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/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": 7,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":show"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 8,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$8$"
+      ],
+      "text/plain": [
+       "8"
+      ]
+     },
+     "execution_count": 8,
+     "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": "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
+}