{
"cells": [
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Formale Sprachen\n",
"\n",
"Dieses Notebook begleitet Vorlesung 3 und erläutert die grundlegenden Definitionen der formalen Sprachen."
]
},
{
"cell_type": "code",
"execution_count": 67,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"Loaded machine: Alphabet"
]
},
"execution_count": 67,
"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": 70,
"metadata": {},
"outputs": [
{
"data": {
"text/markdown": [
"$\\mathit{TRUE}$"
],
"text/plain": [
"TRUE"
]
},
"execution_count": 70,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"[a,b,c] ∈ seq(Σ)"
]
},
{
"cell_type": "code",
"execution_count": 71,
"metadata": {},
"outputs": [
{
"data": {
"text/markdown": [
"$\\mathit{TRUE}$"
],
"text/plain": [
"TRUE"
]
},
"execution_count": 71,
"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": 72,
"metadata": {},
"outputs": [
{
"data": {
"text/markdown": [
"$3$"
],
"text/plain": [
"3"
]
},
"execution_count": 72,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"size([a,b,c])"
]
},
{
"cell_type": "code",
"execution_count": 73,
"metadata": {},
"outputs": [
{
"data": {
"text/markdown": [
"$4$"
],
"text/plain": [
"4"
]
},
"execution_count": 73,
"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": 74,
"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": 74,
"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": 75,
"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": 75,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"Sprachen = {L | L ⊆ seq(Σ)}"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"In folgender B Maschine werden wir ein paar Sprachen und Wörter definieren:"
]
},
{
"cell_type": "code",
"execution_count": 77,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"Loaded machine: Alphabet"
]
},
"execution_count": 77,
"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,c] ∧\n",
" L₁ = {w₁,w₂} ∧\n",
" L₂ = {w₂, [a,a,a] }\n",
"END"
]
},
{
"cell_type": "code",
"execution_count": 78,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"Machine constants set up using operation 0: $setup_constants()"
]
},
"execution_count": 78,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
":constants"
]
},
{
"cell_type": "code",
"execution_count": 79,
"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": 79,
"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": 80,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"Preference changed: PP_SEQUENCES = TRUE\n"
]
},
"execution_count": 80,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
":pref PP_SEQUENCES=TRUE"
]
},
{
"cell_type": "code",
"execution_count": 81,
"metadata": {},
"outputs": [
{
"data": {
"text/markdown": [
"$[a,\\mathit{a},\\mathit{b},c]$"
],
"text/plain": [
"[a,a,b,c]"
]
},
"execution_count": 81,
"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": 82,
"metadata": {},
"outputs": [
{
"data": {
"text/markdown": [
"$[c,c]$"
],
"text/plain": [
"[c,c]"
]
},
"execution_count": 82,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"w₂"
]
},
{
"cell_type": "code",
"execution_count": 83,
"metadata": {},
"outputs": [
{
"data": {
"text/markdown": [
"$\\{[c,c],[a,\\mathit{a},\\mathit{b},c]\\}$"
],
"text/plain": [
"{[c,c],[a,a,b,c]}"
]
},
"execution_count": 83,
"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": 84,
"metadata": {},
"outputs": [
{
"data": {
"text/markdown": [
"$\\mathit{TRUE}$\n",
"\n",
"**Solution:**\n",
"* $\\mathit{LeereSprache} = []$"
],
"text/plain": [
"TRUE\n",
"\n",
"Solution:\n",
"\tLeereSprache = []"
]
},
"execution_count": 84,
"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": 85,
"metadata": {},
"outputs": [
{
"data": {
"text/markdown": [
"$2$"
],
"text/plain": [
"2"
]
},
"execution_count": 85,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"card(L₁)"
]
},
{
"cell_type": "code",
"execution_count": 86,
"metadata": {},
"outputs": [
{
"data": {
"text/markdown": [
"$1$"
],
"text/plain": [
"1"
]
},
"execution_count": 86,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"card( {ε} )"
]
},
{
"cell_type": "code",
"execution_count": 87,
"metadata": {},
"outputs": [
{
"data": {
"text/markdown": [
"$0$"
],
"text/plain": [
"0"
]
},
"execution_count": 87,
"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": 88,
"metadata": {},
"outputs": [
{
"data": {
"text/markdown": [
"$\\{[c,c],[a,\\mathit{a},\\mathit{b},c]\\}$"
],
"text/plain": [
"{[c,c],[a,a,b,c]}"
]
},
"execution_count": 88,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"L₁"
]
},
{
"cell_type": "code",
"execution_count": 90,
"metadata": {},
"outputs": [
{
"data": {
"text/markdown": [
"$\\{[c,c],[a,\\mathit{a},a]\\}$"
],
"text/plain": [
"{[c,c],[a,a,a]}"
]
},
"execution_count": 90,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"L₂"
]
},
{
"cell_type": "code",
"execution_count": 91,
"metadata": {},
"outputs": [
{
"data": {
"text/markdown": [
"$\\{[c,c],[a,\\mathit{a},a],[a,\\mathit{a},\\mathit{b},c]\\}$"
],
"text/plain": [
"{[c,c],[a,a,a],[a,a,b,c]}"
]
},
"execution_count": 91,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"L₁ ∪ L₂"
]
},
{
"cell_type": "code",
"execution_count": 92,
"metadata": {},
"outputs": [
{
"data": {
"text/markdown": [
"$\\{[c,c],[a,\\mathit{a},a],[a,\\mathit{a},\\mathit{b},c]\\}$"
],
"text/plain": [
"{[c,c],[a,a,a],[a,a,b,c]}"
]
},
"execution_count": 92,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"{x| x∈seq(Σ) ∧ (x∈L₁ ∨ x∈L₂)}"
]
},
{
"cell_type": "code",
"execution_count": 93,
"metadata": {},
"outputs": [
{
"data": {
"text/markdown": [
"$\\{[c,c]\\}$"
],
"text/plain": [
"{[c,c]}"
]
},
"execution_count": 93,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"L₁ ∩ L₂"
]
},
{
"cell_type": "code",
"execution_count": 94,
"metadata": {},
"outputs": [
{
"data": {
"text/markdown": [
"$\\{[c,c]\\}$"
],
"text/plain": [
"{[c,c]}"
]
},
"execution_count": 94,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"{x| x∈seq(Σ) ∧ (x∈L₁ ∧ x∈L₂)}"
]
},
{
"cell_type": "code",
"execution_count": 95,
"metadata": {},
"outputs": [
{
"data": {
"text/markdown": [
"$\\{[a,\\mathit{a},\\mathit{b},c]\\}$"
],
"text/plain": [
"{[a,a,b,c]}"
]
},
"execution_count": 95,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"L₁ \\ L₂"
]
},
{
"cell_type": "code",
"execution_count": 96,
"metadata": {},
"outputs": [
{
"data": {
"text/markdown": [
"$\\{[a,\\mathit{a},a]\\}$"
],
"text/plain": [
"{[a,a,a]}"
]
},
"execution_count": 96,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"L₂ \\ L₁"
]
},
{
"cell_type": "code",
"execution_count": 97,
"metadata": {},
"outputs": [
{
"data": {
"text/markdown": [
"$\\mathit{TRUE}$\n",
"\n",
"**Solution:**\n",
"* $\\mathit{Komplement} = (\\mathit{seq}(Σ) - \\{[c,c],[a,\\mathit{a},\\mathit{b},c]\\})$"
],
"text/plain": [
"TRUE\n",
"\n",
"Solution:\n",
"\tKomplement = (seq(Σ) − {[c,c],[a,a,b,c]})"
]
},
"execution_count": 97,
"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": 101,
"metadata": {},
"outputs": [
{
"data": {
"text/markdown": [
"$[a,\\mathit{a},\\mathit{b},c]$"
],
"text/plain": [
"[a,a,b,c]"
]
},
"execution_count": 101,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"w₁"
]
},
{
"cell_type": "code",
"execution_count": 102,
"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": 102,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"w₁^w₁"
]
},
{
"cell_type": "code",
"execution_count": 103,
"metadata": {},
"outputs": [
{
"data": {
"text/markdown": [
"$[a,\\mathit{a},\\mathit{b},c]$"
],
"text/plain": [
"[a,a,b,c]"
]
},
"execution_count": 103,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"w₁^ε"
]
},
{
"cell_type": "code",
"execution_count": 104,
"metadata": {},
"outputs": [
{
"data": {
"text/markdown": [
"$[a,\\mathit{a},\\mathit{b},c]$"
],
"text/plain": [
"[a,a,b,c]"
]
},
"execution_count": 104,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"ε^w₁"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Die Verkettung von Sprachen:"
]
},
{
"cell_type": "code",
"execution_count": 105,
"metadata": {},
"outputs": [
{
"data": {
"text/markdown": [
"$\\{[c,c],[a,\\mathit{a},\\mathit{b},c]\\}$"
],
"text/plain": [
"{[c,c],[a,a,b,c]}"
]
},
"execution_count": 105,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"L₁"
]
},
{
"cell_type": "code",
"execution_count": 106,
"metadata": {},
"outputs": [
{
"data": {
"text/markdown": [
"$\\{[c,c],[a,\\mathit{a},a]\\}$"
],
"text/plain": [
"{[c,c],[a,a,a]}"
]
},
"execution_count": 106,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"L₂"
]
},
{
"cell_type": "code",
"execution_count": 107,
"metadata": {},
"outputs": [
{
"data": {
"text/markdown": [
"$\\{[c,\\mathit{c},\\mathit{c},c],[c,\\mathit{c},\\mathit{a},\\mathit{a},a],[a,\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{c},c],[a,\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{a},\\mathit{a},a]\\}$"
],
"text/plain": [
"{[c,c,c,c],[c,c,a,a,a],[a,a,b,c,c,c],[a,a,b,c,a,a,a]}"
]
},
"execution_count": 107,
"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.\n",
"Dies ist die Sprache $L_1^2$:"
]
},
{
"cell_type": "code",
"execution_count": 114,
"metadata": {},
"outputs": [
{
"data": {
"text/markdown": [
"$\\{[c,\\mathit{c},\\mathit{c},c],[c,\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},c],[a,\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{c},c],[a,\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},c]\\}$"
],
"text/plain": [
"{[c,c,c,c],[c,c,a,a,b,c],[a,a,b,c,c,c],[a,a,b,c,a,a,b,c]}"
]
},
"execution_count": 114,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
":let L1_2 {w | ∃(a,b).(a∈L₁ ∧ b∈L₁ ∧ w = a^b)}"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Man kann eine Sprache auch mehrfach mit sich selber verketten.\n",
"Dies sind die Sprachen $L_1^3$ und $L_1^4$:"
]
},
{
"cell_type": "code",
"execution_count": 118,
"metadata": {},
"outputs": [
{
"data": {
"text/markdown": [
"$\\{[c,\\mathit{c},\\mathit{c},\\mathit{c},\\mathit{c},c],[c,\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{c},c],[a,\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{c},\\mathit{c},\\mathit{c},c],[c,\\mathit{c},\\mathit{c},\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},c],[a,\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{c},c],[c,\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},c],[a,\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{c},\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},c],[a,\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},c]\\}$"
],
"text/plain": [
"{[c,c,c,c,c,c],[c,c,a,a,b,c,c,c],[a,a,b,c,c,c,c,c],[c,c,c,c,a,a,b,c],[a,a,b,c,a,a,b,c,c,c],[c,c,a,a,b,c,a,a,b,c],[a,a,b,c,c,c,a,a,b,c],[a,a,b,c,a,a,b,c,a,a,b,c]}"
]
},
"execution_count": 118,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
":let L1_3 {w | ∃(a,b).(a∈L₁ ∧ b∈L1_2 ∧ w = a^b)}"
]
},
{
"cell_type": "code",
"execution_count": 119,
"metadata": {},
"outputs": [
{
"data": {
"text/markdown": [
"$\\{[c,\\mathit{c},\\mathit{c},\\mathit{c},\\mathit{c},\\mathit{c},\\mathit{c},c],[c,\\mathit{c},\\mathit{c},\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{c},c],[c,\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{c},\\mathit{c},\\mathit{c},c],[a,\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{c},\\mathit{c},\\mathit{c},\\mathit{c},\\mathit{c},c],[c,\\mathit{c},\\mathit{c},\\mathit{c},\\mathit{c},\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},c],[a,\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{c},\\mathit{c},\\mathit{c},c],[c,\\mathit{c},\\mathit{c},\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},c],[c,\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{c},\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},c],[c,\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{c},c],[a,\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{c},\\mathit{c},\\mathit{c},\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},c],[a,\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{c},\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{c},c],[c,\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},c],[a,\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{c},\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},c],[a,\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{c},\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},c],[a,\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{c},c],[a,\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},\\mathit{c},\\mathit{a},\\mathit{a},\\mathit{b},c]\\}$"
],
"text/plain": [
"{[c,c,c,c,c,c,c,c],[c,c,c,c,a,a,b,c,c,c],[c,c,a,a,b,c,c,c,c,c],[a,a,b,c,c,c,c,c,c,c],[c,c,c,c,c,c,a,a,b,c],[a,a,b,c,a,a,b,c,c,c,c,c],[c,c,c,c,a,a,b,c,a,a,b,c],[c,c,a,a,b,c,c,c,a,a,b,c],[c,c,a,a,b,c,a,a,b,c,c,c],[a,a,b,c,c,c,c,c,a,a,b,c],[a,a,b,c,c,c,a,a,b,c,c,c],[c,c,a,a,b,c,a,a,b,c,a,a,b,c],[a,a,b,c,c,c,a,a,b,c,a,a,b,c],[a,a,b,c,a,a,b,c,c,c,a,a,b,c],[a,a,b,c,a,a,b,c,a,a,b,c,c,c],[a,a,b,c,a,a,b,c,a,a,b,c,a,a,b,c]}"
]
},
"execution_count": 119,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
":let L1_4 {w | ∃(a,b).(a∈L₁ ∧ b∈L1_3 ∧ w = a^b)}"
]
},
{
"cell_type": "code",
"execution_count": 129,
"metadata": {},
"outputs": [],
"source": [
":unlet L1_2"
]
},
{
"cell_type": "code",
"execution_count": 130,
"metadata": {},
"outputs": [],
"source": [
":unlet L1_3"
]
},
{
"cell_type": "code",
"execution_count": 131,
"metadata": {},
"outputs": [],
"source": [
":unlet L1_4"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Die Spiegelung eines Wortes kann im Notebook mit dem ```rev``` Operator verwirklicht werden:"
]
},
{
"cell_type": "code",
"execution_count": 132,
"metadata": {},
"outputs": [
{
"data": {
"text/markdown": [
"$[c,\\mathit{b},\\mathit{a},a]$"
],
"text/plain": [
"[c,b,a,a]"
]
},
"execution_count": 132,
"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": 133,
"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": 133,
"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": 134,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"Loaded machine: Alphabet"
]
},
"execution_count": 134,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"::load\n",
"MACHINE Alphabet\n",
"SETS Sigma = {a,b,c}\n",
"CONSTANTS ε, Sprachen, w₁, w₂, L₁, L₂\n",
"ABSTRACT_CONSTANTS\n",
" teilwort, präfix\n",
"PROPERTIES \n",
" ε ∈ seq(Sigma) ∧ size(ε) = 0 ∧\n",
" Sprachen = {L | L ⊆ seq(Sigma)}∧\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(Sigma) & vt∈seq(Sigma) ∧ ∃(vt1,vt2).(vt1^ut^vt2 = vt)} ∧\n",
" präfix = {up,vp | up∈seq(Sigma) & vp∈seq(Sigma) ∧ ∃(wp).(up^wp = vp)}\n",
"DEFINITIONS SET_PREF_PP_SEQUENCES == TRUE\n",
"END"
]
},
{
"cell_type": "code",
"execution_count": 135,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"Machine constants set up using operation 0: $setup_constants()"
]
},
"execution_count": 135,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
":constants"
]
},
{
"cell_type": "code",
"execution_count": 136,
"metadata": {},
"outputs": [
{
"data": {
"text/markdown": [
"$\\mathit{TRUE}$"
],
"text/plain": [
"TRUE"
]
},
"execution_count": 136,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"[a,a] ↦ [c,b,a,a,b] ∈ teilwort"
]
},
{
"cell_type": "code",
"execution_count": 137,
"metadata": {},
"outputs": [
{
"data": {
"text/markdown": [
"$\\mathit{FALSE}$"
],
"text/plain": [
"FALSE"
]
},
"execution_count": 137,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"[a,a,a] ↦ [c,b,a,a,b] ∈ teilwort"
]
},
{
"cell_type": "code",
"execution_count": 138,
"metadata": {},
"outputs": [
{
"data": {
"text/markdown": [
"$\\mathit{TRUE}$"
],
"text/plain": [
"TRUE"
]
},
"execution_count": 138,
"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": 139,
"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": 139,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"{x| x ↦ [c,b,a,a,b] ∈ präfix}"
]
},
{
"cell_type": "code",
"execution_count": 140,
"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": 140,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"{x| x ↦ [c,b,a,a,b] ∈ teilwort}"
]
},
{
"cell_type": "code",
"execution_count": 141,
"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": 141,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
":let TW {x| x ↦ [a,b,c] ∈ teilwort}"
]
},
{
"cell_type": "code",
"execution_count": 142,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"Preference changed: DOT_DECOMPOSE_NODES = FALSE\n"
]
},
"execution_count": 142,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
":pref DOT_DECOMPOSE_NODES=FALSE"
]
},
{
"cell_type": "code",
"execution_count": 143,
"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": 143,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
":dot expr_as_graph (\"tw\",{x,y | x |-> y : teilwort & y : TW })"
]
},
{
"cell_type": "code",
"execution_count": 144,
"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": 144,
"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": 145,
"metadata": {},
"outputs": [],
"source": [
":unlet TW"
]
},
{
"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
}