Skip to content
Snippets Groups Projects
Commit 177ff99d authored by dgelessus's avatar dgelessus
Browse files

Minor updates to FormaleSprachen.ipynb

parent 04c43b29
No related branches found
No related tags found
No related merge requests found
Show whitespace changes
Inline Side-by-side
info4/kapitel-1/FormaleSprachen.ipynb
+ 356
− 324
View file @ 177ff99d
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
## Formale Sprachen ## Formale Sprachen
Dieses Notebook begleitet Vorlesung 3 und erläutert die grundlegenden Definitionen der formalen Sprachen. Dieses Notebook begleitet Vorlesung 3 und erläutert die grundlegenden Definitionen der formalen Sprachen.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
::load ::load
MACHINE Alphabet MACHINE Alphabet
SETS Σ = {a,b,c} SETS Σ = {a,b,c}
END END
``` ```
%% Output %% Output
Loaded machine: Alphabet Loaded machine: Alphabet
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Ein Wort ist eine endliche Folge von Elementen aus dem Alphabet. Ein Wort ist eine endliche Folge von Elementen aus dem Alphabet.
Im Skript schreiben wir $w \in \Sigma^{*}$; hier im Notebook schreiben wir Im Skript schreiben wir $w \in \Sigma^{*}$; hier im Notebook schreiben wir
$w \in seq(\Sigma)$. $w \in \mathrm{seq}(\Sigma)$.
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$. 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$.
Also aus $abc \in \Sigma^*$ wird dies: Also aus $abc \in \Sigma^*$ wird dies:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
[a,b,c] ∈ seq(Σ) [a,b,c] ∈ seq(Σ)
``` ```
%% Output %% Output
$\mathit{TRUE}$ $\mathit{TRUE}$
TRUE TRUE
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
[a,a,b,c] ∈ seq(Σ) [a,a,b,c] ∈ seq(Σ)
``` ```
%% Output %% Output
$\mathit{TRUE}$ $\mathit{TRUE}$
TRUE TRUE
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Die Länge eines Wortes $w$ ist die Anzahl der Symbole in $w$. Im Skript schreiben wir $|w|$, im Notebook benutzen wir ```size(w)```: Die Länge eines Wortes $w$ ist die Anzahl der Symbole in $w$. Im Skript schreiben wir $|w|$, im Notebook benutzen wir $\mathrm{size}(w)$:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
size([a,b,c]) size([a,b,c])
``` ```
%% Output %% Output
$3$ $3$
3 3
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
size([a,a,b,c]) size([a,a,b,c])
``` ```
%% Output %% Output
$4$ $4$
4 4
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Das leere Wort ist das eindeutig bestimmte Wort der Laenge 0: Das leere Wort ist das eindeutig bestimmte Wort der Laenge 0:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
ε ∈ seq(Σ) ∧ size(ε) = 0 ε ∈ seq(Σ) ∧ size(ε) = 0
``` ```
%% Output %% Output
$\renewcommand{\emptyset}{\mathord\varnothing}\mathit{TRUE}$ $\renewcommand{\emptyset}{\mathord\varnothing}\mathit{TRUE}$
**Solution:** **Solution:**
* $ε = \emptyset$ * $\mathit{ε} = \emptyset$
TRUE TRUE
Solution: Solution:
ε = ∅ ε = ∅
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
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. Leider ist in der B-Sprache das Symbol $\lambda$ schon vergeben (zur Definition von Funktionen). Deshalb müssen wir in einer weiteren Abweichung vom Skript Epsilon verwenden.
Eine formale Sprache ist eine jede Teilmenge von $\Sigma^*$. Eine formale Sprache ist eine jede Teilmenge von $\Sigma^*$.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
Sprachen = {L | L ⊆ seq(Σ)} Sprachen = {L | L ⊆ seq(Σ)}
``` ```
%% Output %% Output
$\mathit{TRUE}$ $\mathit{TRUE}$
**Solution:** **Solution:**
* $\mathit{Sprachen} = \{\mathit{L}\mid \mathit{L} \subseteq \mathit{seq}(Σ)\}$ * $\mathit{Sprachen} = \{\mathit{L}\mid\mathit{L} \subseteq \mathit{seq}(\mathit{Σ})\}$
TRUE TRUE
Solution: Solution:
Sprachen = {L∣L ⊆ seq(Σ)} Sprachen = {L∣L ⊆ seq(Σ)}
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
In folgender B Maschine werden wir ein paar Sprachen und Wörter definieren: In folgender B-Maschine werden wir ein paar Sprachen und Wörter definieren:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
::load ::load
MACHINE Alphabet MACHINE Alphabet
SETS Σ = {a,b,c} SETS Σ = {a,b,c}
CONSTANTS ε, Sprachen, w₁, w₂, L₁, L₂ CONSTANTS ε, Sprachen, w₁, w₂, L₁, L₂
PROPERTIES PROPERTIES
ε ∈ seq(Σ) ∧ size(ε) = 0 ∧ ε ∈ seq(Σ) ∧ size(ε) = 0 ∧
Sprachen = {L | L ⊆ seq(Σ)}∧ Sprachen = {L | L ⊆ seq(Σ)} ∧
w₁ = [a,a,b,c] ∧ w₁ = [a,a,b,c] ∧
w₂ = [c,c] ∧ w₂ = [c,c] ∧
L₁ = {w₁,w₂} ∧ L₁ = {w₁,w₂} ∧
L₂ = {w₂, [a,a,a] } L₂ = {w₂, [a,a,a]}
END END
``` ```
%% Output %% Output
Loaded machine: Alphabet Loaded machine: Alphabet
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:constants :constants
``` ```
%% Output %% Output
Machine constants set up using operation 0: $setup_constants() Executed operation: SETUP_CONSTANTS()
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
w₁ w₁
``` ```
%% Output %% Output
$\{(1\mapsto \mathit{a}),(2\mapsto \mathit{a}),(3\mapsto \mathit{b}),(4\mapsto \mathit{c})\}$ $\{(1\mapsto\mathit{a}),(2\mapsto\mathit{a}),(3\mapsto\mathit{b}),(4\mapsto\mathit{c})\}$
{(1↦a),(2↦a),(3↦b),(4↦c)} {(1↦a),(2↦a),(3↦b),(4↦c)}
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
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: 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 id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:pref PP_SEQUENCES=TRUE :pref PP_SEQUENCES=TRUE
``` ```
%% Output %% Output
Preference changed: PP_SEQUENCES = TRUE Preference changed: PP_SEQUENCES = TRUE
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
w₁ w₁
``` ```
%% Output %% Output
$[a,\mathit{a},\mathit{b},c]$ $[\mathit{a},\mathit{a},\mathit{b},\mathit{c}]$
[a,a,b,c] [a,a,b,c]
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Hier wird die Schreibweise von B für Folgen verwendet. Diese kann man auch so im Notebook eingeben. Hier wird die Schreibweise von B für Folgen verwendet. Diese kann man auch so im Notebook eingeben.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
w₂ w₂
``` ```
%% Output %% Output
$[c,c]$ $[\mathit{c},\mathit{c}]$
[c,c] [c,c]
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
L₁ L₁
``` ```
%% Output %% Output
$\{[c,c],[a,\mathit{a},\mathit{b},c]\}$ $\{[\mathit{c},\mathit{c}],[\mathit{a},\mathit{a},\mathit{b},\mathit{c}]\}$
{[c,c],[a,a,b,c]} {[c,c],[a,a,b,c]}
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Die Leere Sprache ist die Sprache die keine Wörter enthält, sie ist unterschiedlich von der Sprache die nur das leere Wort beinhaltet: 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 id: tags: %% Cell type:code id: tags:
``` prob ``` prob
LeereSprache = ∅ ∧ LeereSprache ≠ {ε} LeereSprache = ∅ ∧ LeereSprache ≠ {ε}
``` ```
%% Output %% Output
$\mathit{TRUE}$ $\mathit{TRUE}$
**Solution:** **Solution:**
* $\mathit{LeereSprache} = []$ * $\mathit{LeereSprache} = []$
TRUE TRUE
Solution: Solution:
LeereSprache = [] LeereSprache = []
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Die Kardinalität einer Sprache L ist die Anzahl der Wörter von L. Die Kardinalität einer Sprache L ist die Anzahl der Wörter von L.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
card(L₁) card(L₁)
``` ```
%% Output %% Output
$2$ $2$
2 2
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
card( {ε} ) card({ε})
``` ```
%% Output %% Output
$1$ $1$
1 1
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
card( ∅ ) card(∅)
``` ```
%% Output %% Output
$0$ $0$
0 0
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Die Mengeoperatoren (Vereinigung, Schnitt, Differenz) kann man auch auf Sprachen anwenden: Die Mengeoperatoren (Vereinigung, Schnitt, Differenz) kann man auch auf Sprachen anwenden:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
L₁ L₁
``` ```
%% Output %% Output
$\{[c,c],[a,\mathit{a},\mathit{b},c]\}$ $\{[\mathit{c},\mathit{c}],[\mathit{a},\mathit{a},\mathit{b},\mathit{c}]\}$
{[c,c],[a,a,b,c]} {[c,c],[a,a,b,c]}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
L₂ L₂
``` ```
%% Output %% Output
$\{[c,c],[a,\mathit{a},a]\}$ $\{[\mathit{c},\mathit{c}],[\mathit{a},\mathit{a},\mathit{a}]\}$
{[c,c],[a,a,a]} {[c,c],[a,a,a]}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
L₁ ∪ L₂ L₁ ∪ L₂
``` ```
%% Output %% Output
$\{[c,c],[a,\mathit{a},a],[a,\mathit{a},\mathit{b},c]\}$ $\{[\mathit{c},\mathit{c}],[\mathit{a},\mathit{a},\mathit{a}],[\mathit{a},\mathit{a},\mathit{b},\mathit{c}]\}$
{[c,c],[a,a,a],[a,a,b,c]} {[c,c],[a,a,a],[a,a,b,c]}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
{x| x∈seq(Σ) ∧ (x∈L₁ ∨ x∈L₂)} {x | x∈seq(Σ) ∧ (x∈L₁ ∨ x∈L₂)}
``` ```
%% Output %% Output
$\{[c,c],[a,\mathit{a},a],[a,\mathit{a},\mathit{b},c]\}$ $\{[\mathit{c},\mathit{c}],[\mathit{a},\mathit{a},\mathit{a}],[\mathit{a},\mathit{a},\mathit{b},\mathit{c}]\}$
{[c,c],[a,a,a],[a,a,b,c]} {[c,c],[a,a,a],[a,a,b,c]}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
L₁ ∩ L₂ L₁ ∩ L₂
``` ```
%% Output %% Output
$\{[c,c]\}$ $\{[\mathit{c},\mathit{c}]\}$
{[c,c]} {[c,c]}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
{x| x∈seq(Σ) ∧ (x∈L₁ ∧ x∈L₂)} {x | x∈seq(Σ) ∧ (x∈L₁ ∧ x∈L₂)}
``` ```
%% Output %% Output
$\{[c,c]\}$ $\{[\mathit{c},\mathit{c}]\}$
{[c,c]} {[c,c]}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
L₁ \ L₂ L₁ \ L₂
``` ```
%% Output %% Output
$\{[a,\mathit{a},\mathit{b},c]\}$ $\{[\mathit{a},\mathit{a},\mathit{b},\mathit{c}]\}$
{[a,a,b,c]} {[a,a,b,c]}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
L₂ \ L₁ L₂ \ L₁
``` ```
%% Output %% Output
$\{[a,\mathit{a},a]\}$ $\{[\mathit{a},\mathit{a},\mathit{a}]\}$
{[a,a,a]} {[a,a,a]}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
Komplement = seq(Σ) \ L₁ ∧ Komplement = seq(Σ) \ L₁ ∧
[a,a,b,c] ∉ Komplement ∧ [a,a,b,c] ∉ Komplement ∧
[a,a,c,c] ∈ Komplement [a,a,c,c] ∈ Komplement
``` ```
%% Output %% Output
$\mathit{TRUE}$ $\mathit{TRUE}$
**Solution:** **Solution:**
* $\mathit{Komplement} = (\mathit{seq}(Σ) - \{[c,c],[a,\mathit{a},\mathit{b},c]\})$ * $\mathit{Komplement} = (\mathit{seq}(\mathit{Σ}) - \{[\mathit{c},\mathit{c}],[\mathit{a},\mathit{a},\mathit{b},\mathit{c}]\})$
TRUE TRUE
Solution: Solution:
Komplement = (seq(Σ) − {[c,c],[a,a,b,c]}) Komplement = (seq(Σ) − {[c,c],[a,a,b,c]})
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Konkatenation von Wörtern wird in B mit ^ geschrieben: Konkatenation von Wörtern wird in B mit ^ geschrieben:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
w₁ w₁
``` ```
%% Output %% Output
$[a,\mathit{a},\mathit{b},c]$ $[\mathit{a},\mathit{a},\mathit{b},\mathit{c}]$
[a,a,b,c] [a,a,b,c]
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
w₁^w₁ w₁^w₁
``` ```
%% Output %% Output
$[a,\mathit{a},\mathit{b},\mathit{c},\mathit{a},\mathit{a},\mathit{b},c]$ $[\mathit{a},\mathit{a},\mathit{b},\mathit{c},\mathit{a},\mathit{a},\mathit{b},\mathit{c}]$
[a,a,b,c,a,a,b,c] [a,a,b,c,a,a,b,c]
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
w₁^ε w₁^ε
``` ```
%% Output %% Output
$[a,\mathit{a},\mathit{b},c]$ $[\mathit{a},\mathit{a},\mathit{b},\mathit{c}]$
[a,a,b,c] [a,a,b,c]
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
ε^w₁ ε^w₁
``` ```
%% Output %% Output
$[a,\mathit{a},\mathit{b},c]$ $[\mathit{a},\mathit{a},\mathit{b},\mathit{c}]$
[a,a,b,c] [a,a,b,c]
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Die Verkettung von Sprachen: Die Verkettung von Sprachen:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
L₁ L₁
``` ```
%% Output %% Output
$\{[c,c],[a,\mathit{a},\mathit{b},c]\}$ $\{[\mathit{c},\mathit{c}],[\mathit{a},\mathit{a},\mathit{b},\mathit{c}]\}$
{[c,c],[a,a,b,c]} {[c,c],[a,a,b,c]}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
L₂ L₂
``` ```
%% Output %% Output
$\{[c,c],[a,\mathit{a},a]\}$ $\{[\mathit{c},\mathit{c}],[\mathit{a},\mathit{a},\mathit{a}]\}$
{[c,c],[a,a,a]} {[c,c],[a,a,a]}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
{w | ∃(a,b).(a∈L₁ ∧ b∈L₂ ∧ w = a^b)} {w | ∃(a,b).(a∈L₁ ∧ b∈L₂ ∧ w = a^b)}
``` ```
%% Output %% Output
$\{[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]\}$ $\{[\mathit{c},\mathit{c},\mathit{c},\mathit{c}],[\mathit{c},\mathit{c},\mathit{a},\mathit{a},\mathit{a}],[\mathit{a},\mathit{a},\mathit{b},\mathit{c},\mathit{c},\mathit{c}],[\mathit{a},\mathit{a},\mathit{b},\mathit{c},\mathit{a},\mathit{a},\mathit{a}]\}$
{[c,c,c,c],[c,c,a,a,a],[a,a,b,c,c,c],[a,a,b,c,a,a,a]} {[c,c,c,c],[c,c,a,a,a],[a,a,b,c,c,c],[a,a,b,c,a,a,a]}
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Man kann eine Sprache auch mit sich selber verketten. Man kann eine Sprache auch mit sich selber verketten.
Dies ist die Sprache $L_1^2$: Dies ist die Sprache $L_1^2$:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:let L1_2 {w | ∃(a,b).(a∈L₁ ∧ b∈L₁ ∧ w = a^b)} :let L1_2 {w | ∃(a,b).(a∈L₁ ∧ b∈L₁ ∧ w = a^b)}
``` ```
%% Output %% Output
$\{[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]\}$ $\{[\mathit{c},\mathit{c},\mathit{c},\mathit{c}],[\mathit{c},\mathit{c},\mathit{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},\mathit{c},\mathit{a},\mathit{a},\mathit{b},\mathit{c}]\}$
{[c,c,c,c],[c,c,a,a,b,c],[a,a,b,c,c,c],[a,a,b,c,a,a,b,c]} {[c,c,c,c],[c,c,a,a,b,c],[a,a,b,c,c,c],[a,a,b,c,a,a,b,c]}
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Man kann eine Sprache auch mehrfach mit sich selber verketten. Man kann eine Sprache auch mehrfach mit sich selber verketten.
Dies sind die Sprachen $L_1^3$ und $L_1^4$: Dies sind die Sprachen $L_1^3$ und $L_1^4$:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:let L1_3 {w | ∃(a,b).(a∈L₁ ∧ b∈L1_2 ∧ w = a^b)} :let L1_3 {w | ∃(a,b).(a∈L₁ ∧ b∈L1_2 ∧ w = a^b)}
``` ```
%% Output %% Output
$\{[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]\}$ $\{[\mathit{c},\mathit{c},\mathit{c},\mathit{c},\mathit{c},\mathit{c}],[\mathit{c},\mathit{c},\mathit{a},\mathit{a},\mathit{b},\mathit{c},\mathit{c},\mathit{c}],[\mathit{a},\mathit{a},\mathit{b},\mathit{c},\mathit{c},\mathit{c},\mathit{c},\mathit{c}],[\mathit{c},\mathit{c},\mathit{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},\mathit{c},\mathit{c},\mathit{c}],[\mathit{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},\mathit{c},\mathit{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},\mathit{c},\mathit{a},\mathit{a},\mathit{b},\mathit{c}]\}$
{[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]} {[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]}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:let L1_4 {w | ∃(a,b).(a∈L₁ ∧ b∈L1_3 ∧ w = a^b)} :let L1_4 {w | ∃(a,b).(a∈L₁ ∧ b∈L1_3 ∧ w = a^b)}
``` ```
%% Output %% Output
$\{[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]\}$ $\{[\mathit{c},\mathit{c},\mathit{c},\mathit{c},\mathit{c},\mathit{c},\mathit{c},\mathit{c}],[\mathit{c},\mathit{c},\mathit{c},\mathit{c},\mathit{a},\mathit{a},\mathit{b},\mathit{c},\mathit{c},\mathit{c}],[\mathit{c},\mathit{c},\mathit{a},\mathit{a},\mathit{b},\mathit{c},\mathit{c},\mathit{c},\mathit{c},\mathit{c}],[\mathit{a},\mathit{a},\mathit{b},\mathit{c},\mathit{c},\mathit{c},\mathit{c},\mathit{c},\mathit{c},\mathit{c}],[\mathit{c},\mathit{c},\mathit{c},\mathit{c},\mathit{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},\mathit{c},\mathit{c},\mathit{c},\mathit{c},\mathit{c}],[\mathit{c},\mathit{c},\mathit{c},\mathit{c},\mathit{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},\mathit{c},\mathit{c},\mathit{c},\mathit{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},\mathit{c},\mathit{c},\mathit{c}],[\mathit{a},\mathit{a},\mathit{b},\mathit{c},\mathit{c},\mathit{c},\mathit{c},\mathit{c},\mathit{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},\mathit{c},\mathit{c},\mathit{c}],[\mathit{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},\mathit{c}],[\mathit{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},\mathit{c}],[\mathit{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},\mathit{c}],[\mathit{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},\mathit{c}],[\mathit{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},\mathit{c}]\}$
{[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]} {[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]}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:unlet L1_2 :unlet L1_2
``` ```
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:unlet L1_3 :unlet L1_3
``` ```
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:unlet L1_4 :unlet L1_4
``` ```
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Die Spiegelung eines Wortes kann im Notebook mit dem ```rev``` Operator verwirklicht werden: Die Spiegelung eines Wortes kann im Notebook mit dem Operator `rev` verwirklicht werden:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
rev(w₁) rev(w₁)
``` ```
%% Output %% Output
$[c,\mathit{b},\mathit{a},a]$ $[\mathit{c},\mathit{b},\mathit{a},\mathit{a}]$
[c,b,a,a] [c,b,a,a]
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Eine Sprache wird gespiegelt indem jedes Wort gespiegelt wird: Eine Sprache wird gespiegelt indem jedes Wort gespiegelt wird:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
{ws|∃w.(w∈L₁ ∧ ws=rev(w))} {ws|∃w.(w∈L₁ ∧ ws=rev(w))}
``` ```
%% Output %% Output
$\{[c,c],[c,\mathit{b},\mathit{a},a]\}$ $\{[\mathit{c},\mathit{c}],[\mathit{c},\mathit{b},\mathit{a},\mathit{a}]\}$
{[c,c],[c,b,a,a]} {[c,c],[c,b,a,a]}
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Die Teilwort und Präfix Relationen definieren wir in folgender B Maschine: Die Teilwort- und Präfix-Relationen definieren wir in folgender B-Maschine:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
::load ::load
MACHINE Alphabet MACHINE Alphabet
SETS Sigma = {a,b,c} SETS Sigma = {a,b,c}
CONSTANTS ε, Sprachen, w₁, w₂, L₁, L₂ CONSTANTS ε, Sprachen, w₁, w₂, L₁, L₂
ABSTRACT_CONSTANTS ABSTRACT_CONSTANTS
teilwort, präfix teilwort, präfix
PROPERTIES PROPERTIES
ε ∈ seq(Sigma) ∧ size(ε) = 0 ∧ ε ∈ seq(Sigma) ∧ size(ε) = 0 ∧
Sprachen = {L | L ⊆ seq(Sigma)}∧ Sprachen = {L | L ⊆ seq(Sigma)}∧
w₁ = [a,a,b,c] ∧ w₁ = [a,a,b,c] ∧
w₂ = [c,a,b,a] ∧ w₂ = [c,a,b,a] ∧
L₁ = {w₁,w₂} ∧ L₁ = {w₁,w₂} ∧
L₂ = {w₂, [a,a,a] } ∧ L₂ = {w₂, [a,a,a]} ∧
teilwort = {ut,vt | ut∈seq(Sigma) & vt∈seq(Sigma) ∧ ∃(vt1,vt2).(vt1^ut^vt2 = vt)} ∧ teilwort = {ut,vt | ut∈seq(Sigma) & vt∈seq(Sigma) ∧ ∃(vt1,vt2).(vt1^ut^vt2 = vt)} ∧
präfix = {up,vp | up∈seq(Sigma) & vp∈seq(Sigma) ∧ ∃(wp).(up^wp = vp)} präfix = {up,vp | up∈seq(Sigma) & vp∈seq(Sigma) ∧ ∃(wp).(up^wp = vp)}
DEFINITIONS SET_PREF_PP_SEQUENCES == TRUE DEFINITIONS SET_PREF_PP_SEQUENCES == TRUE
END END
``` ```
%% Output %% Output
Loaded machine: Alphabet Loaded machine: Alphabet
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:constants :constants
``` ```
%% Output %% Output
Machine constants set up using operation 0: $setup_constants() Executed operation: SETUP_CONSTANTS()
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
[a,a] ↦ [c,b,a,a,b] ∈ teilwort [a,a] ↦ [c,b,a,a,b] ∈ teilwort
``` ```
%% Output %% Output
$\mathit{TRUE}$ $\mathit{TRUE}$
TRUE TRUE
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
[a,a,a] ↦ [c,b,a,a,b] ∈ teilwort [a,a,a] ↦ [c,b,a,a,b] ∈ teilwort
``` ```
%% Output %% Output
$\mathit{FALSE}$ $\mathit{FALSE}$
FALSE FALSE
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
[c] ↦ [c,b,a,a,b] ∈ präfix [c] ↦ [c,b,a,a,b] ∈ präfix
``` ```
%% Output %% Output
$\mathit{TRUE}$ $\mathit{TRUE}$
TRUE TRUE
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Man kann den Verkettungs Operator mehrfach anwenden: Man kann den Verkettungs Operator mehrfach anwenden:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
{x| x ↦ [c,b,a,a,b] ∈ präfix} {x| x ↦ [c,b,a,a,b] ∈ präfix}
``` ```
%% Output %% Output
$\{[],[c],[c,b],[c,\mathit{b},a],[c,\mathit{b},\mathit{a},a],[c,\mathit{b},\mathit{a},\mathit{a},b]\}$ $\{[],[\mathit{c}],[\mathit{c},\mathit{b}],[\mathit{c},\mathit{b},\mathit{a}],[\mathit{c},\mathit{b},\mathit{a},\mathit{a}],[\mathit{c},\mathit{b},\mathit{a},\mathit{a},\mathit{b}]\}$
{[],[c],[c,b],[c,b,a],[c,b,a,a],[c,b,a,a,b]} {[],[c],[c,b],[c,b,a],[c,b,a,a],[c,b,a,a,b]}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
{x| x ↦ [c,b,a,a,b] ∈ teilwort} {x| x ↦ [c,b,a,a,b] ∈ teilwort}
``` ```
%% Output %% Output
$\{[],[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]\}$ $\{[],[\mathit{a}],[\mathit{a},\mathit{a}],[\mathit{a},\mathit{b}],[\mathit{b}],[\mathit{b},\mathit{a}],[\mathit{c}],[\mathit{c},\mathit{b}],[\mathit{a},\mathit{a},\mathit{b}],[\mathit{b},\mathit{a},\mathit{a}],[\mathit{b},\mathit{a},\mathit{a},\mathit{b}],[\mathit{c},\mathit{b},\mathit{a}],[\mathit{c},\mathit{b},\mathit{a},\mathit{a}],[\mathit{c},\mathit{b},\mathit{a},\mathit{a},\mathit{b}]\}$
{[],[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]} {[],[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]}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:let TW {x| x ↦ [a,b,c] ∈ teilwort} :let TW {x| x ↦ [a,b,c] ∈ teilwort}
``` ```
%% Output %% Output
$\{[],[a],[a,b],[b],[b,c],[c],[a,\mathit{b},c]\}$ $\{[],[\mathit{a}],[\mathit{a},\mathit{b}],[\mathit{b}],[\mathit{b},\mathit{c}],[\mathit{c}],[\mathit{a},\mathit{b},\mathit{c}]\}$
{[],[a],[a,b],[b],[b,c],[c],[a,b,c]} {[],[a],[a,b],[b],[b,c],[c],[a,b,c]}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:pref DOT_DECOMPOSE_NODES=FALSE :pref DOT_DECOMPOSE_NODES=FALSE
``` ```
%% Output %% Output
Preference changed: DOT_DECOMPOSE_NODES = FALSE Preference changed: DOT_DECOMPOSE_NODES = FALSE
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:dot expr_as_graph ("tw",{x,y | x |-> y : teilwort & y : TW }) :dot expr_as_graph ("tw",{x,y | x |-> y : teilwort & y : TW})
``` ```
%% Output %% Output
<Dot visualization: expr_as_graph [TWTW={[],[a],[a,b],[b],[b,c],[c],[a,b,c]}("tw",{x,y|(x,y):teilwort & y:TW})]> <Dot visualization: expr_as_graph [LET TW BE TW={[],[a],[a,b],[b],[b,c],[c],[a,b,c]} IN(
("tw",{x,y | x |-> y : teilwort & y : TW})
)END]>
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:dot expr_as_graph ("präfix",{x,y | x |-> y : präfix & y : TW }) :dot expr_as_graph ("präfix",{x,y | x |-> y : präfix & y : TW})
``` ```
%% Output %% Output
<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})]> <Dot visualization: expr_as_graph [LET TW BE TW={[],[a],[a,b],[b],[b,c],[c],[a,b,c]} IN(
("präfix",{x,y | x |-> y : präfix & y : TW})
)END]>
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:unlet TW :unlet TW
``` ```
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
MACHINE FormaleSprachen MACHINE FormaleSprachen
/* Formulierung in B der Grundbegriffe aus dem Foliensatz 1 von Informatik 4 */ /* Formulierung in B der Grundbegriffe aus dem Foliensatz 1 von Informatik 4 */
/* erstellt von Michael Leuschel, 2014 */ /* erstellt von Michael Leuschel, 2014 */
SETS SETS
Alphabet /* Ein Alphabet ist eine endliche, nichtleere Menge von Buchstaben (oder Symbolen). */ Alphabet /* Ein Alphabet ist eine endliche, nichtleere Menge von Buchstaben (oder Symbolen). */
= {a,b,c} /* Hier als Beispiel {a,b,c} */ = {a,b,c} /* Hier als Beispiel {a,b,c} */
ABSTRACT_CONSTANTS ABSTRACT_CONSTANTS
kat, Worte, Sprachen, kleene, sp, teilwort, praefix kat, Worte, Sprachen, kleene, sp, teilwort, praefix
CONSTANTS CONSTANTS
w1, w2, lambda, w1, w2, lambda,
L1, L2, LeereSprache, KomplementL1, L1L2 L1, L2, LeereSprache, KomplementL1, L1L2
PROPERTIES PROPERTIES
Worte = seq(Alphabet) /* Ein Wort ist eine endliche Folge von Elementen aus dem Alphabet */ Worte = seq(Alphabet) /* Ein Wort ist eine endliche Folge von Elementen aus dem Alphabet */
& &
/* Beispiele */ /* Beispiele */
w1 = [a,a,b,c] & /* in den Folien schreiben wir aabc anstatt [a,a,b,c] */ w1 = [a,a,b,c] & /* in den Folien schreiben wir aabc anstatt [a,a,b,c] */
w1 : Worte & /* w1 ist ein Wort */ w1 : Worte & /* w1 ist ein Wort */
w2 = [c,a,b,a] & w2 = [c,a,b,a] &
w2 : Worte & w2 : Worte &
/* Die Laenge eines Wortes ist die Anzahl der Symbole in w */ /* Die Laenge eines Wortes ist die Anzahl der Symbole in w */
/* Beispiel: */ /* Beispiel: */
size(w1) = 4 & size(w1) = 4 &
/* Das leere Wort ist das eindeutig bestimmte Wort der Laenge 0 */ /* Das leere Wort ist das eindeutig bestimmte Wort der Laenge 0 */
lambda: Worte & size(lambda) = 0 & lambda: Worte & size(lambda) = 0 &
/* Die Menge aller Worte bezeichnen wir mit \Sigma^*. Hier verwenden wir seq(Alphabet) */ /* Die Menge aller Worte bezeichnen wir mit \Sigma^*. Hier verwenden wir seq(Alphabet) */
/* Eine formale Sprache ist eine jede Teilmenge von \Sigma^*. */ /* Eine formale Sprache ist eine jede Teilmenge von \Sigma^*. */
Sprachen = {L | L <: Worte} & Sprachen = {L | L <: Worte} &
/* Beispiel: */ /* Beispiel: */
L1 = {w1,w2} & L1 : Sprachen & L1 = {w1,w2} & L1 : Sprachen &
L2 = {w2, [a,a,a] } & L2 : Sprachen & L2 = {w2, [a,a,a] } & L2 : Sprachen &
/* Die Leere Sprache ist die Sprache die keine Wörter enthält */ /* Die Leere Sprache ist die Sprache die keine Wörter enthält */
LeereSprache = {} & LeereSprache = {} &
/* Beachte: */ /* Beachte: */
LeereSprache /= {lambda} & LeereSprache /= {lambda} &
/* Die Kardinalität einer Sprache L ist die Anzahl der Wörter von L. /* Die Kardinalität einer Sprache L ist die Anzahl der Wörter von L.
Beispiel: */ Beispiel: */
card(L1) = 2 & card({lambda}) = 1 & card(LeereSprache) = 0 & card(L1) = 2 & card({lambda}) = 1 & card(LeereSprache) = 0 &
/* Beispiele für die Vereinigung von Sprachen: */ /* Beispiele für die Vereinigung von Sprachen: */
L1 \/ L2 = {x| x:Worte & (x:L1 or x:L2)} & L1 \/ L2 = {x| x:Worte & (x:L1 or x:L2)} &
/* Beispiele für die Durchchnitt von Sprachen: */ /* Beispiele für die Durchchnitt von Sprachen: */
L1 /\ L2 = {x| x:Worte & x:L1 & x:L2} & L1 /\ L2 = {x| x:Worte & x:L1 & x:L2} &
/* Beispiele für die Differenz von Sprachen: */ /* Beispiele für die Differenz von Sprachen: */
L1 - L2 = {x| x:Worte & x:L1 & x/: L2} & L1 - L2 = {x| x:Worte & x:L1 & x/: L2} &
/* Beispiele für das Komplement von Sprachen: */ /* Beispiele für das Komplement von Sprachen: */
KomplementL1 = Worte - L1 /* kann man auch so schreiben {x| x:Worte & x/: L1} */ & KomplementL1 = Worte - L1 /* kann man auch so schreiben {x| x:Worte & x/: L1} */ &
w1 /: KomplementL1 & [a,a,a] : KomplementL1 & lambda : KomplementL1 & w1 /: KomplementL1 & [a,a,a] : KomplementL1 & lambda : KomplementL1 &
/* Konkatenation von Wörtern wird in B mit ^ geschrieben: */ /* Konkatenation von Wörtern wird in B mit ^ geschrieben: */
w1^w2 = [a,a,b,c,c,a,b,a] & w1^w2 = [a,a,b,c,c,a,b,a] &
w1^lambda = w1 & lambda^w1 = w1 & w1^lambda = w1 & lambda^w1 = w1 &
/* Verkettung von Sprachen */ /* Verkettung von Sprachen */
L1L2 = {w | #(a,b).(a:L1 & b:L2 & w = a^b)} L1L2 = {w | #(a,b).(a:L1 & b:L2 & w = a^b)}
& kat = %(x,y).(x:Worte & y:Worte | x^y) /* Die Konkatenierung als explizite Funktion */ & kat = %(x,y).(x:Worte & y:Worte | x^y) /* Die Konkatenierung als explizite Funktion */
& kat(w1,w2) = [a,a,b,c,c,a,b,a] & kat(w1,w2) = [a,a,b,c,c,a,b,a]
& L1L2 = kat[L1*L2] & L1L2 = kat[L1*L2]
/* Eine rekursive Definition von A^n: */ /* Eine rekursive Definition von A^n: */
& kleene = %(A,n).(A : Sprachen & n=0|{lambda}) \/ & kleene = %(A,n).(A : Sprachen & n=0|{lambda}) \/
%(A,n).(A : Sprachen & n>0| kat[A*kleene(A,n-1)]) %(A,n).(A : Sprachen & n>0| kat[A*kleene(A,n-1)])
& kleene(L1,1) = L1 & kleene(L1,1) = L1
& kleene(L2,1) = L2 & kleene(L2,1) = L2
/* A^* ist momentan schwieriger darstellbar, zumindest so, dass man mit ProB damit /* A^* ist momentan schwieriger darstellbar, zumindest so, dass man mit ProB damit
arbeiten könnte */ arbeiten könnte */
& /* Die Spiegelbildoperation */ /* Die Spiegelbildoperation */
sp = %u.(u:Worte| %i.(i:dom(u)|u(size(u)+1-i))) & sp = %u.(u:Worte| %i.(i:dom(u)|u(size(u)+1-i)))
& sp(w1) = [c,b,a,a] & sp(w1) = [c,b,a,a]
& sp(sp(w1)) = w1 & sp(sp(w1)) = w1
& sp(lambda) = lambda & sp(lambda) = lambda
/* Die Spiegelung einer Sprache bekommt man einfach durch das relational image: */ /* Die Spiegelung einer Sprache bekommt man einfach durch das relational image: */
& sp[L1] = {sp(w1),sp(w2)} & sp[L1] = {sp(w1),sp(w2)}
& sp[sp[L1]] = L1 & sp[sp[L1]] = L1
& sp[sp[L2]] = L2 & sp[sp[L2]] = L2
/* Die Teilwortrelation */ /* Die Teilwortrelation */
& teilwort = {u,v | u:Worte & v:Worte & #(v1,v2).(v1^u^v2 = v)} & teilwort = {u,v | u:Worte & v:Worte & #(v1,v2).(v1^u^v2 = v)}
& [a,a] |-> [c,b,a,a,b] : teilwort & [a,a] |-> [c,b,a,a,b] : teilwort
& [a,a,a] |-> [c,b,a,a,b] /: teilwort & [a,a,a] |-> [c,b,a,a,b] /: teilwort
/* Wir können alle Teilworte durch das relational image der Umkehrrelation berechnen: */ /* Wir können alle Teilworte durch das relational image der Umkehrrelation berechnen: */
& teilwort~[{[a,a,b]}] = { lambda, [a], [b], [a,a],[a,b], [a,a,b] } & teilwort~[{[a,a,b]}] = { lambda, [a], [b], [a,a],[a,b], [a,a,b] }
/* Die Anfangswortrelation */ /* Die Anfangswortrelation */
& praefix = {u,v | u:Worte & v:Worte & #(w).(u^w = v)} & praefix = {u,v | u:Worte & v:Worte & #(w).(u^w = v)}
& [a,a] |-> [c,b,a,a,b] /: praefix & [a,a] |-> [c,b,a,a,b] /: praefix
& [c,b] |-> [c,b,a,a,b] : praefix & [c,b] |-> [c,b,a,a,b] : praefix
/* Wir können alle Präfixe durch das relational image der Umkehrrelation berechnen: */ /* Wir können alle Präfixe durch das relational image der Umkehrrelation berechnen: */
& praefix~[{[a,a,b]}] = { lambda, [a], [a,a], [a,a,b] } & praefix~[{[a,a,b]}] = { lambda, [a], [a,a], [a,a,b] }
ASSERTIONS ASSERTIONS
card(L1L2) = 4 card(L1L2) = 4
DEFINITIONS SET_PREF_PP_SEQUENCES == TRUE
END END
``` ```
%% Output %% Output
Loaded machine: FormaleSprachen Loaded machine: FormaleSprachen
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:constants
```
%% Output
Executed operation: SETUP_CONSTANTS()
%% Cell type:code id: tags:
``` prob
:init :init
``` ```
%% Output %% Output
java.lang.IllegalArgumentException: Executing operation $initialise_machine with predicate 1=1 produced errors: Could not execute operation INITIALISATION in state root Executed operation: INITIALISATION()
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
kleene(L1, 2) kleene(L1, 2)
``` ```
%% Output %% Output
:eval: NOT-INITIALISED $\{[\mathit{c},\mathit{a},\mathit{b},\mathit{a},\mathit{a},\mathit{a},\mathit{b},\mathit{c}],[\mathit{c},\mathit{a},\mathit{b},\mathit{a},\mathit{c},\mathit{a},\mathit{b},\mathit{a}],[\mathit{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},\mathit{a},\mathit{b},\mathit{a}]\}$
{[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]}
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment