diff --git a/info4/kapitel-1/FormaleSprachen.ipynb b/info4/kapitel-1/FormaleSprachen.ipynb new file mode 100644 index 0000000000000000000000000000000000000000..e453c1af09938570ac3708cd933ff4df63449545 --- /dev/null +++ b/info4/kapitel-1/FormaleSprachen.ipynb @@ -0,0 +1,1588 @@ +{ + "cells": [ + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "## Formale Sprachen" + ] + }, + { + "cell_type": "code", + "execution_count": 1, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "Loaded machine: Alphabet" + ] + }, + "execution_count": 1, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "::load\n", + "MACHINE Alphabet\n", + "SETS Σ = {a,b,c}\n", + "END" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Ein Wort ist eine endliche Folge von Elementen aus dem Alphabet.\n", + "Im Skript schreiben wir $w \\in \\Sigma^{*}$; hier im Notebook schreiben wir\n", + "$w \\in seq(\\Sigma)$.\n", + "\n", + "Im Skript schreiben wir Wörter in dem wir die Symbole aus $\\Sigma$ hintereinander setzten: $abc$. Im Notebook schreiben wir $[a,b,c]$ für die Folge mit den drei Symbolen $a$, $b$ und $c$.\n", + "\n", + "Also aus $abc \\in \\Sigma^*$ wird dies:" + ] + }, + { + "cell_type": "code", + "execution_count": 2, + "metadata": {}, + "outputs": [ + { + "data": { + "text/markdown": [ + "$\\mathit{TRUE}$" + ], + "text/plain": [ + "TRUE" + ] + }, + "execution_count": 2, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "[a,b,c] ∈ seq(Σ)" + ] + }, + { + "cell_type": "code", + "execution_count": 3, + "metadata": {}, + "outputs": [ + { + "data": { + "text/markdown": [ + "$\\mathit{TRUE}$" + ], + "text/plain": [ + "TRUE" + ] + }, + "execution_count": 3, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "[a,a,b,c] ∈ seq(Σ)" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Die Länge eines Wortes $w$ ist die Anzahl der Symbole in $w$. Im Skript schreiben wir $\\|w\\|$, im Notebook benutzen wir ```size(w)```:" + ] + }, + { + "cell_type": "code", + "execution_count": 4, + "metadata": {}, + "outputs": [ + { + "data": { + "text/markdown": [ + "$3$" + ], + "text/plain": [ + "3" + ] + }, + "execution_count": 4, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "size([a,b,c])" + ] + }, + { + "cell_type": "code", + "execution_count": 5, + "metadata": {}, + "outputs": [ + { + "data": { + "text/markdown": [ + "$4$" + ], + "text/plain": [ + "4" + ] + }, + "execution_count": 5, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "size([a,a,b,c])" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Das leere Wort ist das eindeutig bestimmte Wort der Laenge 0:" + ] + }, + { + "cell_type": "code", + "execution_count": 6, + "metadata": {}, + "outputs": [ + { + "data": { + "text/markdown": [ + "$\\renewcommand{\\emptyset}{\\mathord\\varnothing}\\mathit{TRUE}$\n", + "\n", + "**Solution:**\n", + "* $ε = \\emptyset$" + ], + "text/plain": [ + "TRUE\n", + "\n", + "Solution:\n", + "\tε = ∅" + ] + }, + "execution_count": 6, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "ε ∈ seq(Σ) ∧ size(ε) = 0" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Leider ist in der B Sprache das Symbol λ schon vergeben (zur Definition von Funktionen). Deshalb müssen wir in einer weiteren Abweichung vom Skript Epsilon verwenden.\n", + "\n", + "Eine formale Sprache ist eine jede Teilmenge von $\\Sigma^*$." + ] + }, + { + "cell_type": "code", + "execution_count": 7, + "metadata": {}, + "outputs": [ + { + "data": { + "text/markdown": [ + "$\\mathit{TRUE}$\n", + "\n", + "**Solution:**\n", + "* $\\mathit{Sprachen} = \\{\\mathit{L}\\mid \\mathit{L} \\subseteq \\mathit{seq}(Σ)\\}$" + ], + "text/plain": [ + "TRUE\n", + "\n", + "Solution:\n", + "\tSprachen = {L∣L ⊆ seq(Σ)}" + ] + }, + "execution_count": 7, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "Sprachen = {L | L ⊆ seq(Σ)}" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "In folgender B Maschine werden wir ein paar Sprachen definieren:" + ] + }, + { + "cell_type": "code", + "execution_count": 8, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "Loaded machine: Alphabet" + ] + }, + "execution_count": 8, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "::load\n", + "MACHINE Alphabet\n", + "SETS Σ = {a,b,c}\n", + "CONSTANTS ε, Sprachen, w₁, w₂, L₁, L₂\n", + "PROPERTIES \n", + " ε ∈ seq(Σ) ∧ size(ε) = 0 ∧\n", + " Sprachen = {L | L ⊆ seq(Σ)}∧\n", + " w₁ = [a,a,b,c] ∧\n", + " w₂ = [c,a,b,a] ∧\n", + " L₁ = {w₁,w₂} ∧\n", + " L₂ = {w₂, [a,a,a] }\n", + "END" + ] + }, + { + "cell_type": "code", + "execution_count": 9, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "Machine constants set up using operation 0: $setup_constants()" + ] + }, + "execution_count": 9, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + ":constants" + ] + }, + { + "cell_type": "code", + "execution_count": 10, + "metadata": {}, + "outputs": [ + { + "data": { + "text/markdown": [ + "$\\{(1\\mapsto \\mathit{a}),(2\\mapsto \\mathit{a}),(3\\mapsto \\mathit{b}),(4\\mapsto \\mathit{c})\\}$" + ], + "text/plain": [ + "{(1↦a),(2↦a),(3↦b),(4↦c)}" + ] + }, + "execution_count": 10, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "w₁" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Man sieht hier, dass die Folge aabc, mathematisch gesehen eine totale Funktion von 1..4 nach $\\Sigma$ ist. Wir können aber den \"Pretty-Printer\" beeinflussen und Folgen anders ausgeben:" + ] + }, + { + "cell_type": "code", + "execution_count": 11, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "Preference changed: PP_SEQUENCES = TRUE\n" + ] + }, + "execution_count": 11, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + ":pref PP_SEQUENCES=TRUE" + ] + }, + { + "cell_type": "code", + "execution_count": 12, + "metadata": {}, + "outputs": [ + { + "data": { + "text/markdown": [ + "$[a,\\mathit{a},\\mathit{b},c]$" + ], + "text/plain": [ + "[a,a,b,c]" + ] + }, + "execution_count": 12, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "w₁" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Hier wird die Schreibweise von B für Folgen verwendet. Diese kann man auch so im Notebook eingeben." + ] + }, + { + "cell_type": "code", + "execution_count": 13, + "metadata": {}, + "outputs": [ + { + "data": { + "text/markdown": [ + "$[c,\\mathit{a},\\mathit{b},a]$" + ], + "text/plain": [ + "[c,a,b,a]" + ] + }, + "execution_count": 13, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "w₂" + ] + }, + { + "cell_type": "code", + "execution_count": 14, + "metadata": {}, + "outputs": [ + { + "data": { + "text/markdown": [ + "$\\{[a,\\mathit{a},\\mathit{b},c],[c,\\mathit{a},\\mathit{b},a]\\}$" + ], + "text/plain": [ + "{[a,a,b,c],[c,a,b,a]}" + ] + }, + "execution_count": 14, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "L₁" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Die Leere Sprache ist die Sprache die keine Wörter enthält, sie ist unterschiedlich von der Sprache die nur das leere Wort beinhaltet:" + ] + }, + { + "cell_type": "code", + "execution_count": 15, + "metadata": {}, + "outputs": [ + { + "data": { + "text/markdown": [ + "$\\mathit{TRUE}$\n", + "\n", + "**Solution:**\n", + "* $\\mathit{LeereSprache} = []$" + ], + "text/plain": [ + "TRUE\n", + "\n", + "Solution:\n", + "\tLeereSprache = []" + ] + }, + "execution_count": 15, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "LeereSprache = ∅ ∧ LeereSprache ≠ {ε}" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Die Kardinalität einer Sprache L ist die Anzahl der Wörter von L." + ] + }, + { + "cell_type": "code", + "execution_count": 16, + "metadata": {}, + "outputs": [ + { + "data": { + "text/markdown": [ + "$2$" + ], + "text/plain": [ + "2" + ] + }, + "execution_count": 16, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "card(L₁)" + ] + }, + { + "cell_type": "code", + "execution_count": 17, + "metadata": {}, + "outputs": [ + { + "data": { + "text/markdown": [ + "$1$" + ], + "text/plain": [ + "1" + ] + }, + "execution_count": 17, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "card( {ε} )" + ] + }, + { + "cell_type": "code", + "execution_count": 18, + "metadata": {}, + "outputs": [ + { + "data": { + "text/markdown": [ + "$0$" + ], + "text/plain": [ + "0" + ] + }, + "execution_count": 18, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "card( ∅ )" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Die Mengeoperatoren (Vereinigung, Schnitt, Differenz) kann man auch auf Sprachen anwenden:" + ] + }, + { + "cell_type": "code", + "execution_count": 19, + "metadata": {}, + "outputs": [ + { + "data": { + "text/markdown": [ + "$\\{[a,\\mathit{a},a],[a,\\mathit{a},\\mathit{b},c],[c,\\mathit{a},\\mathit{b},a]\\}$" + ], + "text/plain": [ + "{[a,a,a],[a,a,b,c],[c,a,b,a]}" + ] + }, + "execution_count": 19, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "L₁ ∪ L₂" + ] + }, + { + "cell_type": "code", + "execution_count": 20, + "metadata": {}, + "outputs": [ + { + "data": { + "text/markdown": [ + "$\\{[a,\\mathit{a},a],[a,\\mathit{a},\\mathit{b},c],[c,\\mathit{a},\\mathit{b},a]\\}$" + ], + "text/plain": [ + "{[a,a,a],[a,a,b,c],[c,a,b,a]}" + ] + }, + "execution_count": 20, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "{x| x∈seq(Σ) ∧ (x∈L₁ ∨ x∈L₂)}" + ] + }, + { + "cell_type": "code", + "execution_count": 21, + "metadata": {}, + "outputs": [ + { + "data": { + "text/markdown": [ + "$\\{[c,\\mathit{a},\\mathit{b},a]\\}$" + ], + "text/plain": [ + "{[c,a,b,a]}" + ] + }, + "execution_count": 21, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "L₁ ∩ L₂" + ] + }, + { + "cell_type": "code", + "execution_count": 22, + "metadata": {}, + "outputs": [ + { + "data": { + "text/markdown": [ + "$\\{[c,\\mathit{a},\\mathit{b},a]\\}$" + ], + "text/plain": [ + "{[c,a,b,a]}" + ] + }, + "execution_count": 22, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "{x| x∈seq(Σ) ∧ (x∈L₁ ∧ x∈L₂)}" + ] + }, + { + "cell_type": "code", + "execution_count": 23, + "metadata": {}, + "outputs": [ + { + "data": { + "text/markdown": [ + "$\\{[a,\\mathit{a},\\mathit{b},c]\\}$" + ], + "text/plain": [ + "{[a,a,b,c]}" + ] + }, + "execution_count": 23, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "L₁ \\ L₂" + ] + }, + { + "cell_type": "code", + "execution_count": 24, + "metadata": {}, + "outputs": [ + { + "data": { + "text/markdown": [ + "$\\{[a,\\mathit{a},a]\\}$" + ], + "text/plain": [ + "{[a,a,a]}" + ] + }, + "execution_count": 24, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "L₂ \\ L₁" + ] + }, + { + "cell_type": "code", + "execution_count": 25, + "metadata": {}, + "outputs": [ + { + "data": { + "text/markdown": [ + "$\\mathit{TRUE}$\n", + "\n", + "**Solution:**\n", + "* $\\mathit{Komplement} = (\\mathit{seq}(Σ) - \\{[a,\\mathit{a},\\mathit{b},c],[c,\\mathit{a},\\mathit{b},a]\\})$" + ], + "text/plain": [ + "TRUE\n", + "\n", + "Solution:\n", + "\tKomplement = (seq(Σ) − {[a,a,b,c],[c,a,b,a]})" + ] + }, + "execution_count": 25, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "Komplement = seq(Σ) \\ L₁ ∧ \n", + "[a,a,b,c] ∉ Komplement ∧\n", + "[a,a,c,c] ∈ Komplement " + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Konkatenation von Wörtern wird in B mit ^ geschrieben:" + ] + }, + { + "cell_type": "code", + "execution_count": 26, + "metadata": {}, + "outputs": [ + { + "data": { + "text/markdown": [ + "$[a,\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},c]$" + ], + "text/plain": [ + "[a,a,b,c,a,a,b,c]" + ] + }, + "execution_count": 26, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "w₁^w₁" + ] + }, + { + "cell_type": "code", + "execution_count": 27, + "metadata": {}, + "outputs": [ + { + "data": { + "text/markdown": [ + "$[a,\\mathit{a},\\mathit{b},c]$" + ], + "text/plain": [ + "[a,a,b,c]" + ] + }, + "execution_count": 27, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "w₁^ε" + ] + }, + { + "cell_type": "code", + "execution_count": 28, + "metadata": {}, + "outputs": [ + { + "data": { + "text/markdown": [ + "$[a,\\mathit{a},\\mathit{b},c]$" + ], + "text/plain": [ + "[a,a,b,c]" + ] + }, + "execution_count": 28, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "ε^w₁" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Die Verkettung von Sprachen:" + ] + }, + { + "cell_type": "code", + "execution_count": 29, + "metadata": {}, + "outputs": [ + { + "data": { + "text/markdown": [ + "$\\{[a,\\mathit{a},\\mathit{b},c],[c,\\mathit{a},\\mathit{b},a]\\}$" + ], + "text/plain": [ + "{[a,a,b,c],[c,a,b,a]}" + ] + }, + "execution_count": 29, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "L₁" + ] + }, + { + "cell_type": "code", + "execution_count": 30, + "metadata": {}, + "outputs": [ + { + "data": { + "text/markdown": [ + "$\\{[a,\\mathit{a},a],[c,\\mathit{a},\\mathit{b},a]\\}$" + ], + "text/plain": [ + "{[a,a,a],[c,a,b,a]}" + ] + }, + "execution_count": 30, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "L₂" + ] + }, + { + "cell_type": "code", + "execution_count": 31, + "metadata": {}, + "outputs": [ + { + "data": { + "text/markdown": [ + "$\\{[c,\\mathit{a},\\mathit{b},\\mathit{a},\\mathit{a},\\mathit{a},a],[c,\\mathit{a},\\mathit{b},\\mathit{a},\\mathit{c},\\mathit{a},\\mathit{b},a],[a,\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{a},\\mathit{a},a],[a,\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{c},\\mathit{a},\\mathit{b},a]\\}$" + ], + "text/plain": [ + "{[c,a,b,a,a,a,a],[c,a,b,a,c,a,b,a],[a,a,b,c,a,a,a],[a,a,b,c,c,a,b,a]}" + ] + }, + "execution_count": 31, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + " {w | ∃(a,b).(a∈L₁ ∧ b∈L₂ ∧ w = a^b)}" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Man kann eine Sprache auch mit sich selber verketten:" + ] + }, + { + "cell_type": "code", + "execution_count": 32, + "metadata": {}, + "outputs": [ + { + "data": { + "text/markdown": [ + "$\\{[c,\\mathit{a},\\mathit{b},\\mathit{a},\\mathit{a},\\mathit{a},\\mathit{b},c],[c,\\mathit{a},\\mathit{b},\\mathit{a},\\mathit{c},\\mathit{a},\\mathit{b},a],[a,\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},c],[a,\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{c},\\mathit{a},\\mathit{b},a]\\}$" + ], + "text/plain": [ + "{[c,a,b,a,a,a,b,c],[c,a,b,a,c,a,b,a],[a,a,b,c,a,a,b,c],[a,a,b,c,c,a,b,a]}" + ] + }, + "execution_count": 32, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "{w | ∃(a,b).(a∈L₁ ∧ b∈L₁ ∧ w = a^b)}" + ] + }, + { + "cell_type": "code", + "execution_count": 33, + "metadata": {}, + "outputs": [ + { + "data": { + "text/markdown": [ + "$\\{[a,\\mathit{a},\\mathit{b},c],[c,\\mathit{a},\\mathit{b},a]\\}$" + ], + "text/plain": [ + "{[a,a,b,c],[c,a,b,a]}" + ] + }, + "execution_count": 33, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "L₁" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Die Spiegelung eines Wortes kann im Notebook mit dem ```rev``` Operator verwirklicht werden:" + ] + }, + { + "cell_type": "code", + "execution_count": 34, + "metadata": {}, + "outputs": [ + { + "data": { + "text/markdown": [ + "$[c,\\mathit{b},\\mathit{a},a]$" + ], + "text/plain": [ + "[c,b,a,a]" + ] + }, + "execution_count": 34, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "rev(w₁)" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Eine Sprache wird gespiegelt indem jedes Wort gespiegelt wird:" + ] + }, + { + "cell_type": "code", + "execution_count": 35, + "metadata": {}, + "outputs": [ + { + "data": { + "text/markdown": [ + "$\\{[a,\\mathit{b},\\mathit{a},c],[c,\\mathit{b},\\mathit{a},a]\\}$" + ], + "text/plain": [ + "{[a,b,a,c],[c,b,a,a]}" + ] + }, + "execution_count": 35, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "{ws|∃w.(w∈L₁ ∧ ws=rev(w))}" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Die Teilwort und Präfix Relationen definieren wir in folgender B Maschine:" + ] + }, + { + "cell_type": "code", + "execution_count": 36, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "Loaded machine: Alphabet" + ] + }, + "execution_count": 36, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "::load\n", + "MACHINE Alphabet\n", + "SETS Σ = {a,b,c}\n", + "CONSTANTS ε, Sprachen, w₁, w₂, L₁, L₂\n", + "ABSTRACT_CONSTANTS\n", + " teilwort, präfix\n", + "PROPERTIES \n", + " ε ∈ seq(Σ) ∧ size(ε) = 0 ∧\n", + " Sprachen = {L | L ⊆ seq(Σ)}∧\n", + " w₁ = [a,a,b,c] ∧\n", + " w₂ = [c,a,b,a] ∧\n", + " L₁ = {w₁,w₂} ∧\n", + " L₂ = {w₂, [a,a,a] } ∧\n", + " teilwort = {ut,vt | ut∈seq(Σ) & vt∈seq(Σ) ∧ ∃(vt1,vt2).(vt1^ut^vt2 = vt)} ∧\n", + " präfix = {up,vp | up∈seq(Σ) & vp∈seq(Σ) ∧ ∃(wp).(up^wp = vp)}\n", + "DEFINITIONS SET_PREF_PP_SEQUENCES == TRUE\n", + "END" + ] + }, + { + "cell_type": "code", + "execution_count": 37, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "Machine constants set up using operation 0: $setup_constants()" + ] + }, + "execution_count": 37, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + ":constants" + ] + }, + { + "cell_type": "code", + "execution_count": 38, + "metadata": {}, + "outputs": [ + { + "data": { + "text/markdown": [ + "$\\mathit{TRUE}$" + ], + "text/plain": [ + "TRUE" + ] + }, + "execution_count": 38, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "[a,a] ↦ [c,b,a,a,b] ∈ teilwort" + ] + }, + { + "cell_type": "code", + "execution_count": 39, + "metadata": {}, + "outputs": [ + { + "data": { + "text/markdown": [ + "$\\mathit{FALSE}$" + ], + "text/plain": [ + "FALSE" + ] + }, + "execution_count": 39, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "[a,a,a] ↦ [c,b,a,a,b] ∈ teilwort" + ] + }, + { + "cell_type": "code", + "execution_count": 40, + "metadata": {}, + "outputs": [ + { + "data": { + "text/markdown": [ + "$\\mathit{TRUE}$" + ], + "text/plain": [ + "TRUE" + ] + }, + "execution_count": 40, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "[c] ↦ [c,b,a,a,b] ∈ präfix" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Man kann den Verkettungs Operator mehrfach anwenden:" + ] + }, + { + "cell_type": "code", + "execution_count": 41, + "metadata": {}, + "outputs": [ + { + "data": { + "text/markdown": [ + "$\\{[],[c],[c,b],[c,\\mathit{b},a],[c,\\mathit{b},\\mathit{a},a],[c,\\mathit{b},\\mathit{a},\\mathit{a},b]\\}$" + ], + "text/plain": [ + "{[],[c],[c,b],[c,b,a],[c,b,a,a],[c,b,a,a,b]}" + ] + }, + "execution_count": 41, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "{x| x ↦ [c,b,a,a,b] ∈ präfix}" + ] + }, + { + "cell_type": "code", + "execution_count": 42, + "metadata": {}, + "outputs": [ + { + "data": { + "text/markdown": [ + "$\\{[],[a],[a,a],[a,b],[b],[b,a],[c],[c,b],[a,\\mathit{a},b],[b,\\mathit{a},a],[b,\\mathit{a},\\mathit{a},b],[c,\\mathit{b},a],[c,\\mathit{b},\\mathit{a},a],[c,\\mathit{b},\\mathit{a},\\mathit{a},b]\\}$" + ], + "text/plain": [ + "{[],[a],[a,a],[a,b],[b],[b,a],[c],[c,b],[a,a,b],[b,a,a],[b,a,a,b],[c,b,a],[c,b,a,a],[c,b,a,a,b]}" + ] + }, + "execution_count": 42, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "{x| x ↦ [c,b,a,a,b] ∈ teilwort}" + ] + }, + { + "cell_type": "code", + "execution_count": 51, + "metadata": {}, + "outputs": [ + { + "data": { + "text/markdown": [ + "$\\{[],[a],[a,b],[b],[b,c],[c],[a,\\mathit{b},c]\\}$" + ], + "text/plain": [ + "{[],[a],[a,b],[b],[b,c],[c],[a,b,c]}" + ] + }, + "execution_count": 51, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + ":let TW {x| x ↦ [a,b,c] ∈ teilwort}" + ] + }, + { + "cell_type": "code", + "execution_count": 52, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "Preference changed: DOT_DECOMPOSE_NODES = FALSE\n" + ] + }, + "execution_count": 52, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + ":pref DOT_DECOMPOSE_NODES=FALSE" + ] + }, + { + "cell_type": "code", + "execution_count": 53, + "metadata": {}, + "outputs": [ + { + "data": { + "image/svg+xml": [ + "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n", + "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n", + " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n", + "<!-- Generated by graphviz version 2.28.0 (20110509.1545)\n", + " -->\n", + "<!-- Title: state Pages: 1 -->\n", + "<svg width=\"414pt\" height=\"314pt\"\n", + " viewBox=\"0.00 0.00 413.60 314.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n", + "<g id=\"graph1\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 310)\">\n", + "<title>state</title>\n", + "<polygon fill=\"white\" stroke=\"white\" points=\"-4,5 -4,-310 410.603,-310 410.603,5 -4,5\"/>\n", + "<!-- [a,b,c] -->\n", + "<g id=\"node1\" class=\"node\"><title>[a,b,c]</title>\n", + "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"192.606,-36 138.606,-36 138.606,-0 192.606,-0 192.606,-36\"/>\n", + "<text text-anchor=\"middle\" x=\"165.606\" y=\"-13.8\" font-family=\"Times,serif\" font-size=\"14.00\">[a,b,c]</text>\n", + "</g>\n", + "<!-- [a,b,c]->[a,b,c] -->\n", + "<g id=\"edge2\" class=\"edge\"><title>[a,b,c]->[a,b,c]</title>\n", + "<path fill=\"none\" stroke=\"firebrick\" d=\"M192.846,-26.2419C202.629,-26.4192 210.606,-23.6719 210.606,-18 210.606,-14.5437 207.644,-12.1734 203.116,-10.8891\"/>\n", + "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"203.169,-7.3739 192.846,-9.75806 202.403,-14.3318 203.169,-7.3739\"/>\n", + "<text text-anchor=\"middle\" x=\"217.604\" y=\"-13.8\" font-family=\"Times,serif\" font-size=\"14.00\">tw</text>\n", + "</g>\n", + "<!-- [c] -->\n", + "<g id=\"node3\" class=\"node\"><title>[c]</title>\n", + "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"67.6055,-216 13.6055,-216 13.6055,-180 67.6055,-180 67.6055,-216\"/>\n", + "<text text-anchor=\"middle\" x=\"40.6055\" y=\"-193.8\" font-family=\"Times,serif\" font-size=\"14.00\">[c]</text>\n", + "</g>\n", + "<!-- [c]->[a,b,c] -->\n", + "<g id=\"edge4\" class=\"edge\"><title>[c]->[a,b,c]</title>\n", + "<path fill=\"none\" stroke=\"firebrick\" d=\"M38.2249,-179.963C35.9901,-157.532 35.2109,-117.703 52.6083,-90 70.0898,-62.1634 102.9,-43.3742 128.68,-32.1538\"/>\n", + "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"130.272,-35.283 138.17,-28.221 127.592,-28.8163 130.272,-35.283\"/>\n", + "<text text-anchor=\"middle\" x=\"60.6041\" y=\"-103.8\" font-family=\"Times,serif\" font-size=\"14.00\">tw</text>\n", + "</g>\n", + "<!-- [c]->[c] -->\n", + "<g id=\"edge6\" class=\"edge\"><title>[c]->[c]</title>\n", + "<path fill=\"none\" stroke=\"firebrick\" d=\"M67.8463,-206.242C77.6295,-206.419 85.6055,-203.672 85.6055,-198 85.6055,-194.544 82.6437,-192.173 78.116,-190.889\"/>\n", + "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"78.1694,-187.374 67.8463,-189.758 77.403,-194.332 78.1694,-187.374\"/>\n", + "<text text-anchor=\"middle\" x=\"92.6041\" y=\"-193.8\" font-family=\"Times,serif\" font-size=\"14.00\">tw</text>\n", + "</g>\n", + "<!-- [b,c] -->\n", + "<g id=\"node7\" class=\"node\"><title>[b,c]</title>\n", + "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"129.606,-126 75.6055,-126 75.6055,-90 129.606,-90 129.606,-126\"/>\n", + "<text text-anchor=\"middle\" x=\"102.606\" y=\"-103.8\" font-family=\"Times,serif\" font-size=\"14.00\">[b,c]</text>\n", + "</g>\n", + "<!-- [c]->[b,c] -->\n", + "<g id=\"edge8\" class=\"edge\"><title>[c]->[b,c]</title>\n", + "<path fill=\"none\" stroke=\"firebrick\" d=\"M52.8547,-179.614C61.9145,-166.755 74.3967,-149.038 84.5916,-134.568\"/>\n", + "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"87.6944,-136.241 90.5928,-126.05 81.972,-132.209 87.6944,-136.241\"/>\n", + "<text text-anchor=\"middle\" x=\"84.6041\" y=\"-148.8\" font-family=\"Times,serif\" font-size=\"14.00\">tw</text>\n", + "</g>\n", + "<!-- [b,c]->[a,b,c] -->\n", + "<g id=\"edge10\" class=\"edge\"><title>[b,c]->[a,b,c]</title>\n", + "<path fill=\"none\" stroke=\"firebrick\" d=\"M115.052,-89.614C124.258,-76.7551 136.942,-59.0384 147.301,-44.5682\"/>\n", + "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"150.424,-46.2189 153.399,-36.0504 144.732,-42.1441 150.424,-46.2189\"/>\n", + "<text text-anchor=\"middle\" x=\"147.604\" y=\"-58.8\" font-family=\"Times,serif\" font-size=\"14.00\">tw</text>\n", + "</g>\n", + "<!-- [b,c]->[b,c] -->\n", + "<g id=\"edge12\" class=\"edge\"><title>[b,c]->[b,c]</title>\n", + "<path fill=\"none\" stroke=\"firebrick\" d=\"M129.846,-116.242C139.629,-116.419 147.606,-113.672 147.606,-108 147.606,-104.544 144.644,-102.173 140.116,-100.889\"/>\n", + "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"140.169,-97.3739 129.846,-99.7581 139.403,-104.332 140.169,-97.3739\"/>\n", + "<text text-anchor=\"middle\" x=\"154.604\" y=\"-103.8\" font-family=\"Times,serif\" font-size=\"14.00\">tw</text>\n", + "</g>\n", + "<!-- [b] -->\n", + "<g id=\"node10\" class=\"node\"><title>[b]</title>\n", + "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"220.606,-216 166.606,-216 166.606,-180 220.606,-180 220.606,-216\"/>\n", + "<text text-anchor=\"middle\" x=\"193.606\" y=\"-193.8\" font-family=\"Times,serif\" font-size=\"14.00\">[b]</text>\n", + "</g>\n", + "<!-- [b]->[a,b,c] -->\n", + "<g id=\"edge14\" class=\"edge\"><title>[b]->[a,b,c]</title>\n", + "<path fill=\"none\" stroke=\"firebrick\" d=\"M190.921,-179.933C186.05,-148.966 175.72,-83.2989 169.873,-46.1292\"/>\n", + "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"173.294,-45.3503 168.282,-36.0157 166.379,-46.4381 173.294,-45.3503\"/>\n", + "<text text-anchor=\"middle\" x=\"189.604\" y=\"-103.8\" font-family=\"Times,serif\" font-size=\"14.00\">tw</text>\n", + "</g>\n", + "<!-- [b]->[b,c] -->\n", + "<g id=\"edge16\" class=\"edge\"><title>[b]->[b,c]</title>\n", + "<path fill=\"none\" stroke=\"firebrick\" d=\"M179.098,-179.68C169.884,-169.016 157.494,-155.278 145.606,-144 141.59,-140.191 137.209,-136.327 132.829,-132.626\"/>\n", + "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"134.967,-129.851 125.027,-126.185 130.51,-135.25 134.967,-129.851\"/>\n", + "<text text-anchor=\"middle\" x=\"169.604\" y=\"-148.8\" font-family=\"Times,serif\" font-size=\"14.00\">tw</text>\n", + "</g>\n", + "<!-- [b]->[b] -->\n", + "<g id=\"edge18\" class=\"edge\"><title>[b]->[b]</title>\n", + "<path fill=\"none\" stroke=\"firebrick\" d=\"M220.846,-206.242C230.629,-206.419 238.606,-203.672 238.606,-198 238.606,-194.544 235.644,-192.173 231.116,-190.889\"/>\n", + "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"231.169,-187.374 220.846,-189.758 230.403,-194.332 231.169,-187.374\"/>\n", + "<text text-anchor=\"middle\" x=\"245.604\" y=\"-193.8\" font-family=\"Times,serif\" font-size=\"14.00\">tw</text>\n", + "</g>\n", + "<!-- [a,b] -->\n", + "<g id=\"node15\" class=\"node\"><title>[a,b]</title>\n", + "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"282.606,-126 228.606,-126 228.606,-90 282.606,-90 282.606,-126\"/>\n", + "<text text-anchor=\"middle\" x=\"255.606\" y=\"-103.8\" font-family=\"Times,serif\" font-size=\"14.00\">[a,b]</text>\n", + "</g>\n", + "<!-- [b]->[a,b] -->\n", + "<g id=\"edge20\" class=\"edge\"><title>[b]->[a,b]</title>\n", + "<path fill=\"none\" stroke=\"firebrick\" d=\"M205.855,-179.614C214.914,-166.755 227.397,-149.038 237.592,-134.568\"/>\n", + "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"240.694,-136.241 243.593,-126.05 234.972,-132.209 240.694,-136.241\"/>\n", + "<text text-anchor=\"middle\" x=\"237.604\" y=\"-148.8\" font-family=\"Times,serif\" font-size=\"14.00\">tw</text>\n", + "</g>\n", + "<!-- [a,b]->[a,b,c] -->\n", + "<g id=\"edge22\" class=\"edge\"><title>[a,b]->[a,b,c]</title>\n", + "<path fill=\"none\" stroke=\"firebrick\" d=\"M242.644,-89.9856C234.067,-79.1861 222.285,-65.1893 210.606,-54 206.585,-50.1487 202.159,-46.3001 197.7,-42.6389\"/>\n", + "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"199.722,-39.7756 189.717,-36.2911 195.366,-45.2545 199.722,-39.7756\"/>\n", + "<text text-anchor=\"middle\" x=\"233.604\" y=\"-58.8\" font-family=\"Times,serif\" font-size=\"14.00\">tw</text>\n", + "</g>\n", + "<!-- [a,b]->[a,b] -->\n", + "<g id=\"edge24\" class=\"edge\"><title>[a,b]->[a,b]</title>\n", + "<path fill=\"none\" stroke=\"firebrick\" d=\"M282.846,-116.242C292.629,-116.419 300.606,-113.672 300.606,-108 300.606,-104.544 297.644,-102.173 293.116,-100.889\"/>\n", + "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"293.169,-97.3739 282.846,-99.7581 292.403,-104.332 293.169,-97.3739\"/>\n", + "<text text-anchor=\"middle\" x=\"307.604\" y=\"-103.8\" font-family=\"Times,serif\" font-size=\"14.00\">tw</text>\n", + "</g>\n", + "<!-- [a] -->\n", + "<g id=\"node18\" class=\"node\"><title>[a]</title>\n", + "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"373.606,-216 319.606,-216 319.606,-180 373.606,-180 373.606,-216\"/>\n", + "<text text-anchor=\"middle\" x=\"346.606\" y=\"-193.8\" font-family=\"Times,serif\" font-size=\"14.00\">[a]</text>\n", + "</g>\n", + "<!-- [a]->[a,b,c] -->\n", + "<g id=\"edge26\" class=\"edge\"><title>[a]->[a,b,c]</title>\n", + "<path fill=\"none\" stroke=\"firebrick\" d=\"M347.226,-179.804C347.149,-156.832 343.725,-116.013 322.606,-90 292.574,-53.0088 239.137,-34.5634 203.044,-25.9056\"/>\n", + "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"203.427,-22.4042 192.902,-23.6194 201.888,-29.2328 203.427,-22.4042\"/>\n", + "<text text-anchor=\"middle\" x=\"346.604\" y=\"-103.8\" font-family=\"Times,serif\" font-size=\"14.00\">tw</text>\n", + "</g>\n", + "<!-- [a]->[a,b] -->\n", + "<g id=\"edge28\" class=\"edge\"><title>[a]->[a,b]</title>\n", + "<path fill=\"none\" stroke=\"firebrick\" d=\"M332.098,-179.68C322.884,-169.016 310.494,-155.278 298.606,-144 294.59,-140.191 290.209,-136.327 285.829,-132.626\"/>\n", + "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"287.967,-129.851 278.027,-126.185 283.51,-135.25 287.967,-129.851\"/>\n", + "<text text-anchor=\"middle\" x=\"322.604\" y=\"-148.8\" font-family=\"Times,serif\" font-size=\"14.00\">tw</text>\n", + "</g>\n", + "<!-- [a]->[a] -->\n", + "<g id=\"edge30\" class=\"edge\"><title>[a]->[a]</title>\n", + "<path fill=\"none\" stroke=\"firebrick\" d=\"M373.846,-206.242C383.629,-206.419 391.606,-203.672 391.606,-198 391.606,-194.544 388.644,-192.173 384.116,-190.889\"/>\n", + "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"384.169,-187.374 373.846,-189.758 383.403,-194.332 384.169,-187.374\"/>\n", + "<text text-anchor=\"middle\" x=\"398.604\" y=\"-193.8\" font-family=\"Times,serif\" font-size=\"14.00\">tw</text>\n", + "</g>\n", + "<!-- [] -->\n", + "<g id=\"node22\" class=\"node\"><title>[]</title>\n", + "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"184.606,-306 130.606,-306 130.606,-270 184.606,-270 184.606,-306\"/>\n", + "<text text-anchor=\"middle\" x=\"157.606\" y=\"-283.8\" font-family=\"Times,serif\" font-size=\"14.00\">[]</text>\n", + "</g>\n", + "<!-- []->[a,b,c] -->\n", + "<g id=\"edge32\" class=\"edge\"><title>[]->[a,b,c]</title>\n", + "<path fill=\"none\" stroke=\"firebrick\" d=\"M130.501,-283.347C94.4995,-276.875 32.244,-259.674 4.60554,-216 -3.95044,-202.48 1.88589,-195.767 4.60554,-180 15.1162,-119.065 13.6017,-90.376 63.6055,-54 82.7738,-40.0558 107.931,-31.3434 128.465,-26.0986\"/>\n", + "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"129.507,-29.4484 138.425,-23.7286 127.887,-22.6385 129.507,-29.4484\"/>\n", + "<text text-anchor=\"middle\" x=\"17.6041\" y=\"-148.8\" font-family=\"Times,serif\" font-size=\"14.00\">tw</text>\n", + "</g>\n", + "<!-- []->[c] -->\n", + "<g id=\"edge34\" class=\"edge\"><title>[]->[c]</title>\n", + "<path fill=\"none\" stroke=\"firebrick\" d=\"M131.92,-269.924C123.738,-264.338 114.711,-258.02 106.608,-252 94.0787,-242.69 80.5838,-231.982 69.0817,-222.638\"/>\n", + "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"71.0586,-219.733 61.1008,-216.115 66.6287,-225.153 71.0586,-219.733\"/>\n", + "<text text-anchor=\"middle\" x=\"114.604\" y=\"-238.8\" font-family=\"Times,serif\" font-size=\"14.00\">tw</text>\n", + "</g>\n", + "<!-- []->[b,c] -->\n", + "<g id=\"edge36\" class=\"edge\"><title>[]->[b,c]</title>\n", + "<path fill=\"none\" stroke=\"firebrick\" d=\"M152.332,-269.933C142.723,-238.833 122.299,-172.735 110.841,-135.652\"/>\n", + "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"114.159,-134.537 107.863,-126.016 107.471,-136.603 114.159,-134.537\"/>\n", + "<text text-anchor=\"middle\" x=\"142.604\" y=\"-193.8\" font-family=\"Times,serif\" font-size=\"14.00\">tw</text>\n", + "</g>\n", + "<!-- []->[b] -->\n", + "<g id=\"edge38\" class=\"edge\"><title>[]->[b]</title>\n", + "<path fill=\"none\" stroke=\"firebrick\" d=\"M164.718,-269.614C169.879,-256.998 176.953,-239.705 182.809,-225.391\"/>\n", + "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"186.083,-226.631 186.63,-216.05 179.605,-223.981 186.083,-226.631\"/>\n", + "<text text-anchor=\"middle\" x=\"186.604\" y=\"-238.8\" font-family=\"Times,serif\" font-size=\"14.00\">tw</text>\n", + "</g>\n", + "<!-- []->[a,b] -->\n", + "<g id=\"edge40\" class=\"edge\"><title>[]->[a,b]</title>\n", + "<path fill=\"none\" stroke=\"firebrick\" d=\"M184.789,-276.902C209.602,-266.052 244.75,-246.188 260.606,-216 273.595,-191.27 269.62,-158.722 264.116,-136.045\"/>\n", + "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"267.416,-134.838 261.447,-126.084 260.654,-136.649 267.416,-134.838\"/>\n", + "<text text-anchor=\"middle\" x=\"276.604\" y=\"-193.8\" font-family=\"Times,serif\" font-size=\"14.00\">tw</text>\n", + "</g>\n", + "<!-- []->[a] -->\n", + "<g id=\"edge42\" class=\"edge\"><title>[]->[a]</title>\n", + "<path fill=\"none\" stroke=\"firebrick\" d=\"M184.732,-285.403C215.199,-282.528 265.145,-274.487 301.606,-252 312.923,-245.02 322.833,-234.234 330.451,-224.209\"/>\n", + "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"333.306,-226.234 336.291,-216.068 327.618,-222.153 333.306,-226.234\"/>\n", + "<text text-anchor=\"middle\" x=\"328.604\" y=\"-238.8\" font-family=\"Times,serif\" font-size=\"14.00\">tw</text>\n", + "</g>\n", + "<!-- []->[] -->\n", + "<g id=\"edge44\" class=\"edge\"><title>[]->[]</title>\n", + "<path fill=\"none\" stroke=\"firebrick\" d=\"M184.846,-296.242C194.629,-296.419 202.606,-293.672 202.606,-288 202.606,-284.544 199.644,-282.173 195.116,-280.889\"/>\n", + "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"195.169,-277.374 184.846,-279.758 194.403,-284.332 195.169,-277.374\"/>\n", + "<text text-anchor=\"middle\" x=\"209.604\" y=\"-283.8\" font-family=\"Times,serif\" font-size=\"14.00\">tw</text>\n", + "</g>\n", + "</g>\n", + "</svg>" + ], + "text/plain": [ + "<Dot visualization: expr_as_graph [TWTW={[],[a],[a,b],[b],[b,c],[c],[a,b,c]}(\"tw\",{x,y|(x,y):teilwort & y:TW})]>" + ] + }, + "execution_count": 53, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + ":dot expr_as_graph (\"tw\",{x,y | x |-> y : teilwort & y : TW })" + ] + }, + { + "cell_type": "code", + "execution_count": 55, + "metadata": {}, + "outputs": [ + { + "data": { + "image/svg+xml": [ + "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n", + "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n", + " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n", + "<!-- Generated by graphviz version 2.28.0 (20110509.1545)\n", + " -->\n", + "<!-- Title: state Pages: 1 -->\n", + "<svg width=\"517pt\" height=\"314pt\"\n", + " viewBox=\"0.00 0.00 517.25 314.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n", + "<g id=\"graph1\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 310)\">\n", + "<title>state</title>\n", + "<polygon fill=\"white\" stroke=\"white\" points=\"-4,5 -4,-310 514.25,-310 514.25,5 -4,5\"/>\n", + "<!-- [a,b,c] -->\n", + "<g id=\"node1\" class=\"node\"><title>[a,b,c]</title>\n", + "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"369.041,-36 315.041,-36 315.041,-0 369.041,-0 369.041,-36\"/>\n", + "<text text-anchor=\"middle\" x=\"342.041\" y=\"-13.8\" font-family=\"Times,serif\" font-size=\"14.00\">[a,b,c]</text>\n", + "</g>\n", + "<!-- [a,b,c]->[a,b,c] -->\n", + "<g id=\"edge2\" class=\"edge\"><title>[a,b,c]->[a,b,c]</title>\n", + "<path fill=\"none\" stroke=\"firebrick\" d=\"M369.282,-26.2419C379.065,-26.4192 387.041,-23.6719 387.041,-18 387.041,-14.5437 384.079,-12.1734 379.551,-10.8891\"/>\n", + "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"379.605,-7.3739 369.282,-9.75806 378.838,-14.3318 379.605,-7.3739\"/>\n", + "<text text-anchor=\"middle\" x=\"404.145\" y=\"-13.8\" font-family=\"Times,serif\" font-size=\"14.00\">präfix</text>\n", + "</g>\n", + "<!-- [c] -->\n", + "<g id=\"node3\" class=\"node\"><title>[c]</title>\n", + "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"69.041,-216 15.041,-216 15.041,-180 69.041,-180 69.041,-216\"/>\n", + "<text text-anchor=\"middle\" x=\"42.041\" y=\"-193.8\" font-family=\"Times,serif\" font-size=\"14.00\">[c]</text>\n", + "</g>\n", + "<!-- [c]->[c] -->\n", + "<g id=\"edge4\" class=\"edge\"><title>[c]->[c]</title>\n", + "<path fill=\"none\" stroke=\"firebrick\" d=\"M69.2817,-206.242C79.0649,-206.419 87.041,-203.672 87.041,-198 87.041,-194.544 84.0792,-192.173 79.5515,-190.889\"/>\n", + "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"79.6048,-187.374 69.2817,-189.758 78.8385,-194.332 79.6048,-187.374\"/>\n", + "<text text-anchor=\"middle\" x=\"104.145\" y=\"-193.8\" font-family=\"Times,serif\" font-size=\"14.00\">präfix</text>\n", + "</g>\n", + "<!-- [b,c] -->\n", + "<g id=\"node5\" class=\"node\"><title>[b,c]</title>\n", + "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"212.041,-126 158.041,-126 158.041,-90 212.041,-90 212.041,-126\"/>\n", + "<text text-anchor=\"middle\" x=\"185.041\" y=\"-103.8\" font-family=\"Times,serif\" font-size=\"14.00\">[b,c]</text>\n", + "</g>\n", + "<!-- [b,c]->[b,c] -->\n", + "<g id=\"edge6\" class=\"edge\"><title>[b,c]->[b,c]</title>\n", + "<path fill=\"none\" stroke=\"firebrick\" d=\"M212.282,-116.242C222.065,-116.419 230.041,-113.672 230.041,-108 230.041,-104.544 227.079,-102.173 222.551,-100.889\"/>\n", + "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"222.605,-97.3739 212.282,-99.7581 221.838,-104.332 222.605,-97.3739\"/>\n", + "<text text-anchor=\"middle\" x=\"247.145\" y=\"-103.8\" font-family=\"Times,serif\" font-size=\"14.00\">präfix</text>\n", + "</g>\n", + "<!-- [b] -->\n", + "<g id=\"node7\" class=\"node\"><title>[b]</title>\n", + "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"263.041,-216 209.041,-216 209.041,-180 263.041,-180 263.041,-216\"/>\n", + "<text text-anchor=\"middle\" x=\"236.041\" y=\"-193.8\" font-family=\"Times,serif\" font-size=\"14.00\">[b]</text>\n", + "</g>\n", + "<!-- [b]->[b,c] -->\n", + "<g id=\"edge8\" class=\"edge\"><title>[b]->[b,c]</title>\n", + "<path fill=\"none\" stroke=\"firebrick\" d=\"M225.965,-179.614C218.583,-166.876 208.439,-149.372 200.097,-134.979\"/>\n", + "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"202.965,-132.947 194.922,-126.05 196.909,-136.457 202.965,-132.947\"/>\n", + "<text text-anchor=\"middle\" x=\"232.145\" y=\"-148.8\" font-family=\"Times,serif\" font-size=\"14.00\">präfix</text>\n", + "</g>\n", + "<!-- [b]->[b] -->\n", + "<g id=\"edge10\" class=\"edge\"><title>[b]->[b]</title>\n", + "<path fill=\"none\" stroke=\"firebrick\" d=\"M263.282,-206.242C273.065,-206.419 281.041,-203.672 281.041,-198 281.041,-194.544 278.079,-192.173 273.551,-190.889\"/>\n", + "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"273.605,-187.374 263.282,-189.758 272.838,-194.332 273.605,-187.374\"/>\n", + "<text text-anchor=\"middle\" x=\"298.145\" y=\"-193.8\" font-family=\"Times,serif\" font-size=\"14.00\">präfix</text>\n", + "</g>\n", + "<!-- [a,b] -->\n", + "<g id=\"node10\" class=\"node\"><title>[a,b]</title>\n", + "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"369.041,-126 315.041,-126 315.041,-90 369.041,-90 369.041,-126\"/>\n", + "<text text-anchor=\"middle\" x=\"342.041\" y=\"-103.8\" font-family=\"Times,serif\" font-size=\"14.00\">[a,b]</text>\n", + "</g>\n", + "<!-- [a,b]->[a,b,c] -->\n", + "<g id=\"edge12\" class=\"edge\"><title>[a,b]->[a,b,c]</title>\n", + "<path fill=\"none\" stroke=\"firebrick\" d=\"M342.041,-89.614C342.041,-77.2403 342.041,-60.3686 342.041,-46.2198\"/>\n", + "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"345.541,-46.0504 342.041,-36.0504 338.541,-46.0504 345.541,-46.0504\"/>\n", + "<text text-anchor=\"middle\" x=\"359.145\" y=\"-58.8\" font-family=\"Times,serif\" font-size=\"14.00\">präfix</text>\n", + "</g>\n", + "<!-- [a,b]->[a,b] -->\n", + "<g id=\"edge14\" class=\"edge\"><title>[a,b]->[a,b]</title>\n", + "<path fill=\"none\" stroke=\"firebrick\" d=\"M369.282,-116.242C379.065,-116.419 387.041,-113.672 387.041,-108 387.041,-104.544 384.079,-102.173 379.551,-100.889\"/>\n", + "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"379.605,-97.3739 369.282,-99.7581 378.838,-104.332 379.605,-97.3739\"/>\n", + "<text text-anchor=\"middle\" x=\"404.145\" y=\"-103.8\" font-family=\"Times,serif\" font-size=\"14.00\">präfix</text>\n", + "</g>\n", + "<!-- [a] -->\n", + "<g id=\"node13\" class=\"node\"><title>[a]</title>\n", + "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"457.041,-216 403.041,-216 403.041,-180 457.041,-180 457.041,-216\"/>\n", + "<text text-anchor=\"middle\" x=\"430.041\" y=\"-193.8\" font-family=\"Times,serif\" font-size=\"14.00\">[a]</text>\n", + "</g>\n", + "<!-- [a]->[a,b,c] -->\n", + "<g id=\"edge16\" class=\"edge\"><title>[a]->[a,b,c]</title>\n", + "<path fill=\"none\" stroke=\"firebrick\" d=\"M434.497,-179.653C439.203,-157.582 444.17,-118.865 430.041,-90 419.039,-67.5242 397.174,-49.8272 377.992,-37.7228\"/>\n", + "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"379.788,-34.7189 369.416,-32.5577 376.177,-40.7153 379.788,-34.7189\"/>\n", + "<text text-anchor=\"middle\" x=\"455.145\" y=\"-103.8\" font-family=\"Times,serif\" font-size=\"14.00\">präfix</text>\n", + "</g>\n", + "<!-- [a]->[a,b] -->\n", + "<g id=\"edge18\" class=\"edge\"><title>[a]->[a,b]</title>\n", + "<path fill=\"none\" stroke=\"firebrick\" d=\"M412.655,-179.614C399.432,-166.391 381.073,-148.032 366.389,-133.348\"/>\n", + "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"368.637,-130.647 359.091,-126.05 363.688,-135.596 368.637,-130.647\"/>\n", + "<text text-anchor=\"middle\" x=\"410.145\" y=\"-148.8\" font-family=\"Times,serif\" font-size=\"14.00\">präfix</text>\n", + "</g>\n", + "<!-- [a]->[a] -->\n", + "<g id=\"edge20\" class=\"edge\"><title>[a]->[a]</title>\n", + "<path fill=\"none\" stroke=\"firebrick\" d=\"M457.282,-206.242C467.065,-206.419 475.041,-203.672 475.041,-198 475.041,-194.544 472.079,-192.173 467.551,-190.889\"/>\n", + "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"467.605,-187.374 457.282,-189.758 466.838,-194.332 467.605,-187.374\"/>\n", + "<text text-anchor=\"middle\" x=\"492.145\" y=\"-193.8\" font-family=\"Times,serif\" font-size=\"14.00\">präfix</text>\n", + "</g>\n", + "<!-- [] -->\n", + "<g id=\"node17\" class=\"node\"><title>[]</title>\n", + "<polygon fill=\"#cae1ff\" stroke=\"#cae1ff\" points=\"212.041,-306 158.041,-306 158.041,-270 212.041,-270 212.041,-306\"/>\n", + "<text text-anchor=\"middle\" x=\"185.041\" y=\"-283.8\" font-family=\"Times,serif\" font-size=\"14.00\">[]</text>\n", + "</g>\n", + "<!-- []->[a,b,c] -->\n", + "<g id=\"edge22\" class=\"edge\"><title>[]->[a,b,c]</title>\n", + "<path fill=\"none\" stroke=\"firebrick\" d=\"M157.63,-282.904C99.3364,-272.892 -28.8745,-243.23 6.04098,-180 67.136,-69.3606 230.704,-33.8217 304.731,-23.1954\"/>\n", + "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"305.543,-26.6173 314.981,-21.8024 304.6,-19.6811 305.543,-26.6173\"/>\n", + "<text text-anchor=\"middle\" x=\"47.1455\" y=\"-148.8\" font-family=\"Times,serif\" font-size=\"14.00\">präfix</text>\n", + "</g>\n", + "<!-- []->[c] -->\n", + "<g id=\"edge24\" class=\"edge\"><title>[]->[c]</title>\n", + "<path fill=\"none\" stroke=\"firebrick\" d=\"M157.781,-276.366C142.874,-270.09 124.341,-261.523 108.832,-252 94.8927,-243.441 80.5428,-232.396 68.734,-222.606\"/>\n", + "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"70.899,-219.854 61.0008,-216.075 66.3823,-225.202 70.899,-219.854\"/>\n", + "<text text-anchor=\"middle\" x=\"126.145\" y=\"-238.8\" font-family=\"Times,serif\" font-size=\"14.00\">präfix</text>\n", + "</g>\n", + "<!-- []->[b,c] -->\n", + "<g id=\"edge26\" class=\"edge\"><title>[]->[b,c]</title>\n", + "<path fill=\"none\" stroke=\"firebrick\" d=\"M178.998,-269.755C174.353,-255.537 168.321,-234.734 165.832,-216 163.724,-200.139 163.724,-195.861 165.832,-180 167.796,-165.218 171.966,-149.147 175.92,-136.04\"/>\n", + "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"179.339,-136.834 178.998,-126.245 172.661,-134.735 179.339,-136.834\"/>\n", + "<text text-anchor=\"middle\" x=\"183.145\" y=\"-193.8\" font-family=\"Times,serif\" font-size=\"14.00\">präfix</text>\n", + "</g>\n", + "<!-- []->[b] -->\n", + "<g id=\"edge28\" class=\"edge\"><title>[]->[b]</title>\n", + "<path fill=\"none\" stroke=\"firebrick\" d=\"M195.117,-269.614C202.499,-256.876 212.643,-239.372 220.985,-224.979\"/>\n", + "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"224.173,-226.457 226.159,-216.05 218.117,-222.947 224.173,-226.457\"/>\n", + "<text text-anchor=\"middle\" x=\"232.145\" y=\"-238.8\" font-family=\"Times,serif\" font-size=\"14.00\">präfix</text>\n", + "</g>\n", + "<!-- []->[a,b] -->\n", + "<g id=\"edge30\" class=\"edge\"><title>[]->[a,b]</title>\n", + "<path fill=\"none\" stroke=\"firebrick\" d=\"M212.058,-281C244.137,-272.383 296.724,-253.261 324.041,-216 340.867,-193.049 344.103,-159.922 343.928,-136.623\"/>\n", + "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"347.419,-136.266 343.629,-126.373 340.422,-136.47 347.419,-136.266\"/>\n", + "<text text-anchor=\"middle\" x=\"356.145\" y=\"-193.8\" font-family=\"Times,serif\" font-size=\"14.00\">präfix</text>\n", + "</g>\n", + "<!-- []->[a] -->\n", + "<g id=\"edge32\" class=\"edge\"><title>[]->[a]</title>\n", + "<path fill=\"none\" stroke=\"firebrick\" d=\"M212.234,-285.824C248.626,-283.354 314.445,-275.699 365.041,-252 380.147,-244.924 394.75,-233.568 406.275,-223.178\"/>\n", + "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"408.818,-225.592 413.731,-216.205 404.036,-220.48 408.818,-225.592\"/>\n", + "<text text-anchor=\"middle\" x=\"409.145\" y=\"-238.8\" font-family=\"Times,serif\" font-size=\"14.00\">präfix</text>\n", + "</g>\n", + "<!-- []->[] -->\n", + "<g id=\"edge34\" class=\"edge\"><title>[]->[]</title>\n", + "<path fill=\"none\" stroke=\"firebrick\" d=\"M212.282,-296.242C222.065,-296.419 230.041,-293.672 230.041,-288 230.041,-284.544 227.079,-282.173 222.551,-280.889\"/>\n", + "<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"222.605,-277.374 212.282,-279.758 221.838,-284.332 222.605,-277.374\"/>\n", + "<text text-anchor=\"middle\" x=\"247.145\" y=\"-283.8\" font-family=\"Times,serif\" font-size=\"14.00\">präfix</text>\n", + "</g>\n", + "</g>\n", + "</svg>" + ], + "text/plain": [ + "<Dot visualization: expr_as_graph [TWTW={[],[a],[a,b],[b],[b,c],[c],[a,b,c]}(\"präfix\",{x,y|(x,y):präfix & y:TW})]>" + ] + }, + "execution_count": 55, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + ":dot expr_as_graph (\"präfix\",{x,y | x |-> y : präfix & y : TW })" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [] + }, + { + "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 +}