From 588b9e29febd971a510997d99ab6857d714878e2 Mon Sep 17 00:00:00 2001
From: Michael Leuschel <leuschel@uni-duesseldorf.de>
Date: Fri, 29 May 2020 12:15:53 +0200
Subject: [PATCH] add CYK notebook
---
info4/kapitel-3/CYK_Algorithmus.ipynb | 1023 +++++++++++++++++++++++++
1 file changed, 1023 insertions(+)
create mode 100644 info4/kapitel-3/CYK_Algorithmus.ipynb
diff --git a/info4/kapitel-3/CYK_Algorithmus.ipynb b/info4/kapitel-3/CYK_Algorithmus.ipynb
new file mode 100644
index 0000000..7a897c7
--- /dev/null
+++ b/info4/kapitel-3/CYK_Algorithmus.ipynb
@@ -0,0 +1,1023 @@
+{
+ "cells": [
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "# CYK Algorithmus"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 14,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Loaded machine: GrammarChomskyNormalForm_CYK"
+ ]
+ },
+ "execution_count": 14,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "::load\n",
+ "MACHINE GrammarChomskyNormalForm_CYK\n",
+ "/* An encoding of the CYK Algorithm in B */\n",
+ "SETS\n",
+ " Σ = {a,b, S,A,B,C}\n",
+ "DEFINITIONS\n",
+ " ANIMATION_FUNCTION_DEFAULT == {r,c,i| r=-1 ∧ c↦i ∈ target};\n",
+ " ANIMATION_FUNCTION == {r,c,i | c↦r ∈ dom(T) ∧ i=(T(c,r))}\n",
+ "CONSTANTS Terminals, NonTerminals, Productions, target, 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",
+ " [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",
+ "VARIABLES T, i,j\n",
+ "INVARIANT T ∈ ((1..n)*(0..n)) ⇸ ℙ(NonTerminals) ∧ 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",
+ "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",
+ " T(i,j) := Tij ||\n",
+ " IF i<n-j THEN\n",
+ " i := i+1\n",
+ " ELSE\n",
+ " i := 1 || j := j+1\n",
+ " END\n",
+ " END;\n",
+ " r <-- Accept = PRE j=n THEN r := bool(S∈ T(1,n-1)) END\n",
+ "END\n",
+ "\n",
+ "\n",
+ "\n"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 15,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Machine constants set up using operation 0: $setup_constants()"
+ ]
+ },
+ "execution_count": 15,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":constants"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 16,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Machine initialised using operation 1: $initialise_machine()"
+ ]
+ },
+ "execution_count": 16,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":init"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 17,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "<table style=\"font-family:monospace\"><tbody>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">b</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\">a</td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">{B}</td>\n",
+ "<td style=\"padding:10px\">{A,C}</td>\n",
+ "<td style=\"padding:10px\">{A,C}</td>\n",
+ "<td style=\"padding:10px\">{B}</td>\n",
+ "<td style=\"padding:10px\">{A,C}</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/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}\\})\\}$"
+ ],
+ "text/plain": [
+ "{(1↦0↦{B}),(2↦0↦{A,C}),(3↦0↦{A,C}),(4↦0↦{B}),(5↦0↦{A,C})}"
+ ]
+ },
+ "execution_count": 18,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "T"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 19,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$1$"
+ ],
+ "text/plain": [
+ "1"
+ ]
+ },
+ "execution_count": 19,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "i"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 20,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$1$"
+ ],
+ "text/plain": [
+ "1"
+ ]
+ },
+ "execution_count": 20,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "j"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 22,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: For_k_loop(1,1,{S,A})"
+ ]
+ },
+ "execution_count": 22,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec For_k_loop"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 23,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$(2\\mapsto 1)$"
+ ],
+ "text/plain": [
+ "(2↦1)"
+ ]
+ },
+ "execution_count": 23,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "(i,j)"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 24,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "<table style=\"font-family:monospace\"><tbody>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">b</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\">a</td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">{B}</td>\n",
+ "<td style=\"padding:10px\">{A,C}</td>\n",
+ "<td style=\"padding:10px\">{A,C}</td>\n",
+ "<td style=\"padding:10px\">{B}</td>\n",
+ "<td style=\"padding:10px\">{A,C}</td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">{S,A}</td>\n",
+ "<td style=\"padding:0px\"></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": 24,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":show"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 25,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: For_k_loop(2,1,{B})"
+ ]
+ },
+ "execution_count": 25,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec For_k_loop"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 26,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$(3\\mapsto 1)$"
+ ],
+ "text/plain": [
+ "(3↦1)"
+ ]
+ },
+ "execution_count": 26,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "(i,j)"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 27,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "<table style=\"font-family:monospace\"><tbody>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">b</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\">a</td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">{B}</td>\n",
+ "<td style=\"padding:10px\">{A,C}</td>\n",
+ "<td style=\"padding:10px\">{A,C}</td>\n",
+ "<td style=\"padding:10px\">{B}</td>\n",
+ "<td style=\"padding:10px\">{A,C}</td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">{S,A}</td>\n",
+ "<td style=\"padding:10px\">{B}</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": 27,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":show"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 28,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\{(1\\mapsto 0\\mapsto\\{\\mathit{B}\\}),(1\\mapsto 1\\mapsto\\{\\mathit{S},\\mathit{A}\\}),(2\\mapsto 0\\mapsto\\{\\mathit{A},\\mathit{C}\\}),(2\\mapsto 1\\mapsto\\{\\mathit{B}\\}),(3\\mapsto 0\\mapsto\\{\\mathit{A},\\mathit{C}\\}),(4\\mapsto 0\\mapsto\\{\\mathit{B}\\}),(5\\mapsto 0\\mapsto\\{\\mathit{A},\\mathit{C}\\})\\}$"
+ ],
+ "text/plain": [
+ "{(1↦0↦{B}),(1↦1↦{S,A}),(2↦0↦{A,C}),(2↦1↦{B}),(3↦0↦{A,C}),(4↦0↦{B}),(5↦0↦{A,C})}"
+ ]
+ },
+ "execution_count": 28,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "T"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 29,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: For_k_loop(3,1,{S,C})"
+ ]
+ },
+ "execution_count": 29,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec For_k_loop"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 30,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: For_k_loop(4,1,{S,A})"
+ ]
+ },
+ "execution_count": 30,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec For_k_loop"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 31,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "<table style=\"font-family:monospace\"><tbody>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">b</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\">a</td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">{B}</td>\n",
+ "<td style=\"padding:10px\">{A,C}</td>\n",
+ "<td style=\"padding:10px\">{A,C}</td>\n",
+ "<td style=\"padding:10px\">{B}</td>\n",
+ "<td style=\"padding:10px\">{A,C}</td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">{S,A}</td>\n",
+ "<td style=\"padding:10px\">{B}</td>\n",
+ "<td style=\"padding:10px\">{S,C}</td>\n",
+ "<td style=\"padding:10px\">{S,A}</td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "</tr>\n",
+ "</tbody></table>"
+ ],
+ "text/plain": [
+ "<Animation function visualisation>"
+ ]
+ },
+ "execution_count": 31,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":show"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 32,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: For_k_loop(1,2,{})"
+ ]
+ },
+ "execution_count": 32,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec For_k_loop"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 33,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$(2\\mapsto 2)$"
+ ],
+ "text/plain": [
+ "(2↦2)"
+ ]
+ },
+ "execution_count": 33,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "(i,j)"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 34,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "<table style=\"font-family:monospace\"><tbody>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">b</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\">a</td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">{B}</td>\n",
+ "<td style=\"padding:10px\">{A,C}</td>\n",
+ "<td style=\"padding:10px\">{A,C}</td>\n",
+ "<td style=\"padding:10px\">{B}</td>\n",
+ "<td style=\"padding:10px\">{A,C}</td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">{S,A}</td>\n",
+ "<td style=\"padding:10px\">{B}</td>\n",
+ "<td style=\"padding:10px\">{S,C}</td>\n",
+ "<td style=\"padding:10px\">{S,A}</td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">{}</td>\n",
+ "<td style=\"padding:0px\"></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": 34,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":show"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 35,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: For_k_loop(2,2,{B})"
+ ]
+ },
+ "execution_count": 35,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec For_k_loop"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 36,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: For_k_loop(3,2,{B})"
+ ]
+ },
+ "execution_count": 36,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec For_k_loop"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 37,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "<table style=\"font-family:monospace\"><tbody>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">b</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\">a</td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">{B}</td>\n",
+ "<td style=\"padding:10px\">{A,C}</td>\n",
+ "<td style=\"padding:10px\">{A,C}</td>\n",
+ "<td style=\"padding:10px\">{B}</td>\n",
+ "<td style=\"padding:10px\">{A,C}</td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">{S,A}</td>\n",
+ "<td style=\"padding:10px\">{B}</td>\n",
+ "<td style=\"padding:10px\">{S,C}</td>\n",
+ "<td style=\"padding:10px\">{S,A}</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",
+ "<td style=\"padding:0px\"></td>\n",
+ "<td style=\"padding:0px\"></td>\n",
+ "</tr>\n",
+ "</tbody></table>"
+ ],
+ "text/plain": [
+ "<Animation function visualisation>"
+ ]
+ },
+ "execution_count": 37,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":show"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 38,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: For_k_loop(1,3,{})"
+ ]
+ },
+ "execution_count": 38,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec For_k_loop"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 39,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "<table style=\"font-family:monospace\"><tbody>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">b</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\">a</td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">{B}</td>\n",
+ "<td style=\"padding:10px\">{A,C}</td>\n",
+ "<td style=\"padding:10px\">{A,C}</td>\n",
+ "<td style=\"padding:10px\">{B}</td>\n",
+ "<td style=\"padding:10px\">{A,C}</td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">{S,A}</td>\n",
+ "<td style=\"padding:10px\">{B}</td>\n",
+ "<td style=\"padding:10px\">{S,C}</td>\n",
+ "<td style=\"padding:10px\">{S,A}</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",
+ "<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:0px\"></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": 39,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":show"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 40,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: For_k_loop(2,3,{S,A,C})"
+ ]
+ },
+ "execution_count": 40,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec For_k_loop"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 41,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "<table style=\"font-family:monospace\"><tbody>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">b</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\">a</td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">{B}</td>\n",
+ "<td style=\"padding:10px\">{A,C}</td>\n",
+ "<td style=\"padding:10px\">{A,C}</td>\n",
+ "<td style=\"padding:10px\">{B}</td>\n",
+ "<td style=\"padding:10px\">{A,C}</td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">{S,A}</td>\n",
+ "<td style=\"padding:10px\">{B}</td>\n",
+ "<td style=\"padding:10px\">{S,C}</td>\n",
+ "<td style=\"padding:10px\">{S,A}</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",
+ "<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\">{S,A,C}</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": 41,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":show"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 42,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: For_k_loop(1,4,{S,A,C})"
+ ]
+ },
+ "execution_count": 42,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec For_k_loop"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 43,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "<table style=\"font-family:monospace\"><tbody>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">b</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\">a</td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">{B}</td>\n",
+ "<td style=\"padding:10px\">{A,C}</td>\n",
+ "<td style=\"padding:10px\">{A,C}</td>\n",
+ "<td style=\"padding:10px\">{B}</td>\n",
+ "<td style=\"padding:10px\">{A,C}</td>\n",
+ "</tr>\n",
+ "<tr>\n",
+ "<td style=\"padding:10px\">{S,A}</td>\n",
+ "<td style=\"padding:10px\">{B}</td>\n",
+ "<td style=\"padding:10px\">{S,C}</td>\n",
+ "<td style=\"padding:10px\">{S,A}</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",
+ "<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\">{S,A,C}</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\">{S,A,C}</td>\n",
+ "<td style=\"padding:0px\"></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": 43,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":show"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 46,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\mathit{TRUE}$"
+ ],
+ "text/plain": [
+ "TRUE"
+ ]
+ },
+ "execution_count": 46,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "S : T(1,n-1)"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 47,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: TRUE <-- Accept()"
+ ]
+ },
+ "execution_count": 47,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec Accept"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 48,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$(1\\mapsto 5\\mapsto 5)$"
+ ],
+ "text/plain": [
+ "(1↦5↦5)"
+ ]
+ },
+ "execution_count": 48,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "(i,j,n)"
+ ]
+ },
+ {
+ "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": 2
+}
--
GitLab