add descriptions and convert to Unicode

info4/kapitel-3/CYK_Algorithmus.ipynb

@@ -9,52 +9,60 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 14,
+   "execution_count": 74,
    "metadata": {},
    "outputs": [
     {
      "data": {
       "text/plain": [
-       "Loaded machine: GrammarChomskyNormalForm_CYK"
+       "Loaded machine: CYK"
       ]
      },
-     "execution_count": 14,
+     "execution_count": 74,
      "metadata": {},
      "output_type": "execute_result"
     }
    ],
    "source": [
     "::load\n",
-    "MACHINE GrammarChomskyNormalForm_CYK\n",
+    "MACHINE CYK\n",
     "/* An encoding of the CYK Algorithm in B */\n",
     "SETS\n",
-    " Σ = {a,b,   S,A,B,C}\n",
+    " ΣN = {a,b,   S,A,B,C}\n",
     "DEFINITIONS\n",
-    "  ANIMATION_FUNCTION_DEFAULT == {r,c,i| r=-1 ∧ c↦i ∈ target};\n",
+    "  ANIMATION_FUNCTION_DEFAULT == {r,c,i| r=-1 ∧ c↦i ∈ x};\n",
     "  ANIMATION_FUNCTION == {r,c,i | c↦r ∈ dom(T) ∧ i=(T(c,r))}\n",
-    "CONSTANTS Terminals, NonTerminals, Productions, target, n\n",
+    "CONSTANTS Σ, N, P, x, n\n",
     "PROPERTIES\n",
-    " Terminals = {a,b} ∧\n",
-    " Terminals ∩ NonTerminals = ∅ ∧\n",
-    " Terminals ∪ NonTerminals = Σ ∧\n",
-    " /* the following is the CFG from Example 6.7 illustrating CYK in Hopcroft/Ullman */\n",
-    " Productions = {\n",
+    " Σ = {a,b} ∧ // Terminalsymbole\n",
+    " Σ ∩ N = ∅ ∧\n",
+    " Σ ∪ N = ΣN ∧\n",
+    " /* eine kfG in Chomsky Normalform, Example 6.7 aus Hopcroft/Ullman */\n",
+    " P = { // die Regeln\n",
     "                  [S] ↦ [A,B], [S] ↦ [B,C],\n",
     "                  [A] ↦ [B,A], [A] ↦ [a],\n",
     "                  [B] ↦ [C,C], [B] ↦ [b],\n",
     "                  [C] ↦ [A,B], [C] ↦ [a]\n",
     "     } ∧\n",
-    "target ∈ seq(Σ) ∧ n = size(target) ∧ target = [b,a,a,b,a]\n",
+    "x ∈ seq(ΣN) ∧ n = size(x) ∧ \n",
+    "x = [b,a,a,b,a]\n",
     "VARIABLES T, i,j\n",
-    "INVARIANT T ∈ ((1..n)*(0..n)) ⇸ ℙ(NonTerminals) ∧ j∈1..n ∧ i∈1..n-1\n",
+    "INVARIANT T ∈ ((1..n)*(0..n)) ⇸ ℙ(N) ∧ j∈1..n ∧ i∈1..n-1\n",
     "INITIALISATION \n",
-    "  T := λ(i,j).(i∈1..n ∧ j=0 | {A| A∈NonTerminals ∧ [A] ↦ [target(i)] ∈ Productions}) ||\n",
-    "  j := 1 || i := 1\n",
+    "  T := λ(i,j).(i∈1..n ∧ j=0 | {A| A∈N ∧ [A] ↦ [x(i)] ∈ P}) \n",
+    "  // for(i =1,2,...,n){T(i,0)={A∈N | 􏰁􏰁A→x(i) ist Regel in P}; }\n",
+    "  ||\n",
+    "  j := 1 \n",
+    "  || \n",
+    "  i := 1\n",
     "OPERATIONS\n",
-    "  For_k_loop(ii,jj,Tij) = PRE j<n ∧ ii=i ∧ jj=j ∧\n",
-    "        Tij = { A | A∈NonTerminals ∧\n",
-    "                ∃(B,C,k).( [A] ↦ [B,C] ∈ Productions ∧ k∈0..j-1 ∧\n",
-    "                           B∈T(i,k) ∧ C∈T(i+k+1,j-k-1)) }  THEN\n",
+    "  For_k_loop(ii,jj,Tij) = // führt eine Iteration der for(k=0,1,...j-1) Schleife aus\n",
+    "    PRE j<n ∧ ii=i ∧ jj=j ∧\n",
+    "        Tij = { A | A∈N ∧\n",
+    "                ∃(B,C,k).( [A] ↦ [B,C] ∈ P ∧ \n",
+    "                           k∈0..j-1 ∧\n",
+    "                           B∈T(i,k) ∧\n",
+    "                           C∈T(i+k+1,j-k-1)) }  THEN\n",
     "    T(i,j) := Tij ||\n",
     "    IF i<n-j THEN\n",
     "       i := i+1\n",
@@ -71,7 +79,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 15,
+   "execution_count": 75,
    "metadata": {},
    "outputs": [
     {
@@ -80,7 +88,7 @@
        "Machine constants set up using operation 0: $setup_constants()"
       ]
      },
-     "execution_count": 15,
+     "execution_count": 75,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -91,7 +99,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 16,
+   "execution_count": 76,
    "metadata": {},
    "outputs": [
     {
@@ -100,7 +108,7 @@
        "Machine initialised using operation 1: $initialise_machine()"
       ]
      },
-     "execution_count": 16,
+     "execution_count": 76,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -109,9 +117,47 @@
     ":init"
    ]
   },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "Wir lassen den Algorithmus für folgendes Wort $x$ laufen (und wollen prüfen ob die Grammatik das Wort generieren kann):"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 77,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$\\{(1\\mapsto \\mathit{b}),(2\\mapsto \\mathit{a}),(3\\mapsto \\mathit{a}),(4\\mapsto \\mathit{b}),(5\\mapsto \\mathit{a})\\}$"
+      ],
+      "text/plain": [
+       "{(1↦b),(2↦a),(3↦a),(4↦b),(5↦a)}"
+      ]
+     },
+     "execution_count": 77,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "x"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "Am Anfang werden die Werte für T(i,0) in der INITIALISATION der Maschine berechnet:\n",
+    "* for(i =1,2,...,n){T(i,0)={A∈N | 􏰁􏰁A→x(i) ist Regel in P};"
+   ]
+  },
   {
    "cell_type": "code",
-   "execution_count": 17,
+   "execution_count": 78,
    "metadata": {},
    "outputs": [
     {
@@ -138,7 +184,7 @@
        "<Animation function visualisation>"
       ]
      },
-     "execution_count": 17,
+     "execution_count": 78,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -149,71 +195,71 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 18,
+   "execution_count": 79,
    "metadata": {},
    "outputs": [
     {
      "data": {
       "text/markdown": [
-       "$\\{(1\\mapsto 0\\mapsto\\{\\mathit{B}\\}),(2\\mapsto 0\\mapsto\\{\\mathit{A},\\mathit{C}\\}),(3\\mapsto 0\\mapsto\\{\\mathit{A},\\mathit{C}\\}),(4\\mapsto 0\\mapsto\\{\\mathit{B}\\}),(5\\mapsto 0\\mapsto\\{\\mathit{A},\\mathit{C}\\})\\}$"
+       "$\\{\\mathit{S},\\mathit{A},\\mathit{B},\\mathit{C}\\}$"
       ],
       "text/plain": [
-       "{(1↦0↦{B}),(2↦0↦{A,C}),(3↦0↦{A,C}),(4↦0↦{B}),(5↦0↦{A,C})}"
+       "{S,A,B,C}"
       ]
      },
-     "execution_count": 18,
+     "execution_count": 79,
      "metadata": {},
      "output_type": "execute_result"
     }
    ],
    "source": [
-    "T"
+    "N"
    ]
   },
   {
    "cell_type": "code",
-   "execution_count": 19,
+   "execution_count": 59,
    "metadata": {},
    "outputs": [
     {
      "data": {
       "text/markdown": [
-       "$1$"
+       "$\\{(\\{(1\\mapsto \\mathit{S})\\}\\mapsto\\{(1\\mapsto \\mathit{A}),(2\\mapsto \\mathit{B})\\}),(\\{(1\\mapsto \\mathit{S})\\}\\mapsto\\{(1\\mapsto \\mathit{B}),(2\\mapsto \\mathit{C})\\}),(\\{(1\\mapsto \\mathit{A})\\}\\mapsto\\{(1\\mapsto \\mathit{a})\\}),(\\{(1\\mapsto \\mathit{A})\\}\\mapsto\\{(1\\mapsto \\mathit{B}),(2\\mapsto \\mathit{A})\\}),(\\{(1\\mapsto \\mathit{B})\\}\\mapsto\\{(1\\mapsto \\mathit{b})\\}),(\\{(1\\mapsto \\mathit{B})\\}\\mapsto\\{(1\\mapsto \\mathit{C}),(2\\mapsto \\mathit{C})\\}),(\\{(1\\mapsto \\mathit{C})\\}\\mapsto\\{(1\\mapsto \\mathit{a})\\}),(\\{(1\\mapsto \\mathit{C})\\}\\mapsto\\{(1\\mapsto \\mathit{A}),(2\\mapsto \\mathit{B})\\})\\}$"
       ],
       "text/plain": [
-       "1"
+       "{({(1↦S)}↦{(1↦A),(2↦B)}),({(1↦S)}↦{(1↦B),(2↦C)}),({(1↦A)}↦{(1↦a)}),({(1↦A)}↦{(1↦B),(2↦A)}),({(1↦B)}↦{(1↦b)}),({(1↦B)}↦{(1↦C),(2↦C)}),({(1↦C)}↦{(1↦a)}),({(1↦C)}↦{(1↦A),(2↦B)})}"
       ]
      },
-     "execution_count": 19,
+     "execution_count": 59,
      "metadata": {},
      "output_type": "execute_result"
     }
    ],
    "source": [
-    "i"
+    "P"
    ]
   },
   {
    "cell_type": "code",
-   "execution_count": 20,
+   "execution_count": 56,
    "metadata": {},
    "outputs": [
     {
      "data": {
       "text/markdown": [
-       "$1$"
+       "$(1\\mapsto 1)$"
       ],
       "text/plain": [
-       "1"
+       "(1↦1)"
       ]
      },
-     "execution_count": 20,
+     "execution_count": 56,
      "metadata": {},
      "output_type": "execute_result"
     }
    ],
    "source": [
-    "j"
+    "(i,j)"
    ]
   },
   {