Skip to content
Snippets Groups Projects
Commit 90b34bf6 authored by Chris's avatar Chris
Browse files

Notebook zu Abschlusseigenschaften erstellt

parent ead07adb
No related branches found
No related tags found
1 merge request!1Master
%% Cell type:markdown id: tags:
# Abschlusseigenschaften regulärer Sprachen
Abschlusseigenschaften sind ein weiteres nützliches Werkzeug um verschiedene Sprachklassen zu charakterisieren.
Damit kann man untersuchen, ob eine Sprache zu einer Sprachklasse gehört oder nicht.
Die regulären Sprachen sind abgeschlossen unter:
* Vereinigung A ∪ B
* Komplement A̅
* Schnitt A ∩ B
* Differenz A/B
* Konkatenation AB
* Iteration A*
* Spiegelung sp(A)
In den Folien wird diese Aussage zwar aufgestellt, aber nicht bewiesen.
Hier schauen wir uns für einige Operationen Beweisideen an konkreten Beispielen an.
%% Cell type:markdown id: tags:
Zuerst betrachten wir die Vereinigung.
Zu jeder regulären Sprache kann man auch einen NFA angeben.
Wenn $M_1=(Σ, Z1, δ1, S1, F1)$ und $M_2=(Σ, Z2, δ2, S2, F2)$ zwei NFAs sind, dann lässt sich ein Vereinigungs-NFA $M=(Σ, Z1 ∪ Z2, δ1∪δ2, S1∪S2, F1∪F2)$ erstellen, so dass $L(M) = L(M_1) ∪ L(M_2)$. Man erhält M, indem man alle Mengen der Tupel von $M_1$ und $M_2$ paarweise vereinigt (analog zum Beweis des Satzes von Kleene Folie 52).
%% Cell type:code id: tags:
``` prob
::load
MACHINE NFA
SETS
Z = {z10,z11,z12,z13, z20,z21,z22}
CONSTANTS Σ, M, S, F, δ,
M1, Z1, δ1, S1, F1,
M2, Z2, δ2, S2, F2
PROPERTIES
Σ = {0,1} ∧
Z1 ∩ Z2 = ∅
// Der Automat M1 von Folie 21 (L(M1)={u1v|u∈{0,1}* ∧ v∈{0,1}}):
M1=(Σ, Z1, δ1, S1, F1) ∧
Z1 ⊆ Z ∧
F1 ⊆ Z1 ∧ S1 ⊆ Z1 ∧
δ1 ∈ (Z1×Σ) → ℙ(Z1)
Z1 = {z10,z11,z12,z13} ∧
S1 = {z10} ∧ F1 = {z12} ∧
δ1 = { (z10,0)↦{z10}, (z10,1)↦{z10,z11},
(z11,0)↦{z12}, (z11,1)↦{z12},
(z12,0)↦{z13}, (z12,1)↦{z13},
(z13,0)↦{z13}, (z13,1)↦{z13} }
// Der Automat M2 von Folie 28 (L(M2)={u1|u∈{0,1}*}):
M2=(Σ, Z2, δ2, S2, F2) ∧
Z2 ⊆ Z ∧
F2 ⊆ Z2 ∧ S2 ⊆ Z2 ∧
δ2 ∈ (Z2×Σ) → ℙ(Z2)
Z2 = {z20,z21,z22} ∧
S2 = {z20} ∧ F2 = {z21} ∧
δ2 = { (z20,0)↦{z20}, (z20,1)↦{z20,z21},
(z21,0)↦{z22}, (z21,1)↦{z22},
(z22,0)↦{z22}, (z22,1)↦{z22}}
//Der Vereinigungsautomat M:
M=(Σ, Z, δ, S, F) ∧
Z= Z1 ∪ Z2 ∧
δ = δ1 ∪ δ2 ∧
S = S1 ∪ S2 ∧
F = F1 ∪ F2
DEFINITIONS // Für den Zustandsgraphen:
CUSTOM_GRAPH_NODES1 == rec(shape:"doublecircle",nodes:F); // Endzustände
CUSTOM_GRAPH_NODES2 == rec(shape:"circle",nodes:Z\F); // andere Zustände
CUSTOM_GRAPH_NODES3 == rec(shape:"none",color:"white",style:"none",nodes:{""});
CUSTOM_GRAPH_EDGES1 == rec(color:"green",label:"0",edges:{x,y|y∈δ(x,0) ∧ y∉δ(x,1)});
CUSTOM_GRAPH_EDGES2 == rec(color:"green",label:"1",edges:{x,y|y∈δ(x,1) ∧ y∉δ(x,0)});
CUSTOM_GRAPH_EDGES3 == rec(color:"green",label:"0, 1",edges:{x,y|y∈δ(x,0) ∧ y∈δ(x,1)});
CUSTOM_GRAPH_EDGES4 == rec(color:"black",label:"",edges:{""}*S) // Kanten für Startknoten
END
```
%% Output
Loaded machine: NFA
%% Cell type:code id: tags:
``` prob
:constants
```
%% Output
Machine constants set up using operation 0: $setup_constants()
%% Cell type:code id: tags:
``` prob
:dot custom_graph
```
%% Output
<Dot visualization: custom_graph []>
%% Cell type:markdown id: tags:
Eine weitere Eigenschaft, die man leicht zeigen kann ist, dass das Komplement einer Sprache $L$ regulär ist. Sei $M=(Σ, Z, δ, z0, F)$ ein DFA mit $L(M)=L$. Dann gilt für $M'=(Σ, Z, δ, z0, Z/F)$, dass $L(M')= \overline{L}$. Dies kann man auch mit folgender Machiene darstellen:
%% Cell type:code id: tags:
``` prob
::load
MACHINE DFA
SETS
Z = {z0,z1,z2,z3}
CONSTANTS Σ, M, δ, F, M2, z_start
PROPERTIES
M = (Σ, Z, δ, z_start, F) ∧
M2 = (Σ, Z, δ, z_start, Z\F) ∧
z_start ∈ Z ∧
F ⊆ Z ∧
δ ∈ (Z×Σ) → Z ∧
Σ = {0,1}
DEFINITIONS // Für den Zustandsgraphen:
CUSTOM_GRAPH_NODES1 == rec(shape:"doublecircle",nodes:Z\F); // Endzustände von M2
CUSTOM_GRAPH_NODES2 == rec(shape:"circle",nodes:F); // andere Zustände von M2
CUSTOM_GRAPH_NODES3 == rec(shape:"none",color:"white",style:"none",nodes:{""});
CUSTOM_GRAPH_EDGES1 == rec(color:"red",label:"0",edges:{a,b|(a,0)|->b:δ});
CUSTOM_GRAPH_EDGES2 == rec(color:"green",label:"1",edges:{a,b|(a,1)|->b:δ});
CUSTOM_GRAPH_EDGES3 == rec(color:"black",label:"",edges:{"" |-> z_start}) // Kante für den Startknoten
END
```
%% Output
Loaded machine: DFA
%% Cell type:markdown id: tags:
Diese Maschiene hat die feste Zustandsmenge Z={z0,z1,z2,z3} und das Alphabet Σ = {0,1}, aber die restlichen Elemente werden der Anweisung ```:constants``` übergeben. Somit kann das Komplement eines beliebigen DFAs erzeugt werden.
%% Cell type:code id: tags:
``` prob
:constants M=({0,1}, //Σ
{z0,z1,z2,z3}, //Z
{(z0,0)↦z1, (z0,1)↦z3,
(z1,0)↦z3, (z1,1)↦z2,
(z2,0)↦z2, (z2,1)↦z2,
(z3,0)↦z3, (z3,1)↦z3 }, //δ
z0, {z0, z2}) //z0, F
```
%% Output
Machine constants set up using operation 0: $setup_constants()
%% Cell type:code id: tags:
``` prob
:dot custom_graph
```
%% Output
<Dot visualization: custom_graph []>
%% Cell type:markdown id: tags:
Als nächstes befassen wir uns mit der Konkatenation zweier Sprachen. Um dies zu erreichen schaltet man 2 NFAs hintereinander.
%% Cell type:code id: tags:
``` prob
::load
MACHINE NFA
SETS
Z = {z10,z11, z12, z20,z21,z22}
CONSTANTS Σ, S, F, δ,
Z1, S1, F1, δ1,
Z2, S2, F2, δ2
PROPERTIES
Σ = {0,1}
Z1 ⊆ Z ∧ Z1 = {z10,z11,z12} ∧
F1 ⊆ Z1 ∧ S1 ⊆ Z1 ∧
δ1 ∈ (Z1×Σ) → ℙ(Z1)
// Der Automat M1 (L(M1)={w| |w|=0 ∨ w=u0 mit u∈{0,1}*}):
S1 = {z10} ∧ F1 = {z10, z12} ∧
δ1 = { (z10,0)↦{z12}, (z10,1)↦{z11},
(z11,0)↦{z12}, (z11,1)↦{z11},
(z12,0)↦{z12}, (z12,1)↦{z11}} ∧
Z2 ⊆ Z ∧ Z2 = {z20,z21,z22} ∧
F2 ⊆ Z2 ∧ S2 ⊆ Z2 ∧
δ2 ∈ (Z2×Σ) → ℙ(Z2)
// Der Automat M2 (L(M2)={1^n|n∈ℕ_0}):
S2 = {z20} ∧ F2 = {z20, z21} ∧
δ2 = { (z20,0)↦{z22}, (z20,1)↦{z21},
(z21,0)↦{z22}, (z21,1)↦{z21},
(z22,0)↦{z22}, (z22,1)↦{z22}} ∧
//Die Regeln von Folie 51:
Z1 ∩ Z2 = ∅ ∧
Z= Z1 ∪ Z2 ∧
S = S1 ∪ ran((S1∩F1)*S2)
∧ F = F2 ∪ ran((S2∩F2)*F1)
∧ δ = {x | x∈(Z*INTEGER)*POW(Z) ∧
∃zustand,symbol,menge.(x=(zustand, symbol)↦menge ∧ (
(zustand∈Z1 ∧ menge = δ1(zustand,symbol) ∧ δ1(zustand,symbol)∩F1= ∅) ∨
(zustand∈Z1 ∧ menge = δ1(zustand,symbol) ∪ S2 ∧ δ1(zustand,symbol)∩F1 ≠ ∅) ∨
(zustand∈Z2 ∧ menge = δ2(zustand,symbol))))}
DEFINITIONS // Für den Zustandsgraphen:
CUSTOM_GRAPH_NODES1 == rec(shape:"doublecircle",nodes:F); // Endzustände
CUSTOM_GRAPH_NODES2 == rec(shape:"circle",nodes:Z\F); // andere Zustände
CUSTOM_GRAPH_NODES3 == rec(shape:"none",color:"white",style:"none",nodes:{""});
CUSTOM_GRAPH_EDGES1 == rec(color:"green",label:"0",edges:{x,y|y∈δ(x,0) ∧ y∉δ(x,1)});
CUSTOM_GRAPH_EDGES2 == rec(color:"green",label:"1",edges:{x,y|y∈δ(x,1) ∧ y∉δ(x,0)});
CUSTOM_GRAPH_EDGES3 == rec(color:"green",label:"0, 1",edges:{x,y|y∈δ(x,0) ∧ y∈δ(x,1)});
CUSTOM_GRAPH_EDGES4 == rec(color:"black",label:"",edges:{""}*S) // Kanten für Startknoten
END
```
%% Output
Loaded machine: NFA
%% Cell type:code id: tags:
``` prob
:constants
```
%% Output
Machine constants set up using operation 0: $setup_constants()
%% Cell type:code id: tags:
``` prob
:dot custom_graph
```
%% Output
<Dot visualization: custom_graph []>
%% Cell type:markdown id: tags:
Um zu zeigen, dass die Iteration einer regulären Sprache wieder regulär ist, bilden wir zu einem NFA den Rückkopplungsautomaten.
%% Cell type:code id: tags:
``` prob
::load
MACHINE NFA
SETS
Z = {z10,z11, z12, z}
CONSTANTS M1, M2, M,
Σ, δ,
Z1, S1, F1, δ1,
Z2, S2, F2, δ2
PROPERTIES
Σ = {0,1}
M1 = (Σ, Z1, δ1, S1, F1)∧
Z1 ⊆ Z ∧ Z1 = {z10,z11,z12} ∧
F1 ⊆ Z1 ∧ S1 ⊆ Z1 ∧
δ1 ∈ (Z1×Σ) → ℙ(Z1)
// Der Automat M1 (L(M1)={w| |w|=0 ∨ w=u0 mit u∈{0,1}*}):
S1 = {z10} ∧ F1 = {z10, z12} ∧
δ1 = { (z10,0)↦{z12}, (z10,1)↦{z11},
(z11,0)↦{z12}, (z11,1)↦{z11},
(z12,0)↦{z12}, (z12,1)↦{z11}} ∧
Z2 ⊆ Z ∧
F2 ⊆ Z2 ∧ S2 ⊆ Z2 ∧
δ2 ∈ (Z2×Σ) → ℙ(Z2)
//Die Regeln von Folie 53
Z2 = IF S1∩F1 ≠ ∅ THEN Z1 ELSE Z1∪{z} END ∧
S2 = IF S1∩F1 ≠ ∅ THEN S1 ELSE S1∪{z} END ∧
F2 = IF S1∩F1 ≠ ∅ THEN F1 ELSE F1∪{z} END ∧
M2 = (Σ, Z2, δ1, S2, F2) ∧
//Die Regeln von Folie 54:
δ = {x | x:(Z*INTEGER)*POW(Z) ∧
∃zustand,symbol,menge.(x=(zustand, symbol)↦menge ∧ (
(zustand∈Z2 ∧ menge = δ1(zustand,symbol) ∧ δ1(zustand,symbol)∩F2= ∅) ∨
(zustand∈Z2 ∧ menge = δ1(zustand,symbol) ∪ S2 ∧ δ1(zustand,symbol)∩F2 ≠ ∅)))} ∧
M = (Σ, Z2, δ, S2, F2)
DEFINITIONS // Für den Zustandsgraphen:
CUSTOM_GRAPH_NODES1 == rec(shape:"doublecircle",nodes:F2); // Endzustände
CUSTOM_GRAPH_NODES2 == rec(shape:"circle",nodes:Z2\F2); // andere Zustände
CUSTOM_GRAPH_NODES3 == rec(shape:"none",color:"white",style:"none",nodes:{""});
CUSTOM_GRAPH_EDGES1 == rec(color:"green",label:"0",edges:{x,y|{(x,0),(x,1)} <:dom(δ) ∧ y∈δ(x,0) ∧ y∉δ(x,1)});
CUSTOM_GRAPH_EDGES2 == rec(color:"green",label:"1",edges:{x,y|{(x,0),(x,1)} <:dom(δ) ∧ y∈δ(x,1) ∧ y∉δ(x,0)});
CUSTOM_GRAPH_EDGES3 == rec(color:"green",label:"0, 1",edges:{x,y|{(x,0),(x,1)} <:dom(δ) ∧ y∈δ(x,0) ∧ y∈δ(x,1)});
CUSTOM_GRAPH_EDGES4 == rec(color:"black",label:"",edges:{""}*S2) // Kanten für Startknoten
END
```
%% Output
Loaded machine: NFA
%% Cell type:code id: tags:
``` prob
:constants
```
%% Output
Machine constants set up using operation 0: $setup_constants()
%% Cell type:code id: tags:
``` prob
:dot custom_graph
```
%% Output
<Dot visualization: custom_graph []>
%% Cell type:markdown id: tags:
Im folgenden schauen wir uns die Differenz zweier Sprachen L1-L2 genauer an.
Das Vorgehen ist hierbei, dass man zwei NFAs parallel ausführt und die Endzustandsmenge so wählt, dass man in einem Endzustand des ersten, aber nicht des zweiten NFAs landet.
%% Cell type:code id: tags:
``` prob
::load
MACHINE NFA
SETS
Z = {z10,z11, z12, z20,z21,z22}
CONSTANTS Σ, Z_gesamt, S, F, δ, f,
Z1, S1, F1, δ1,
Z2, S2, F2, δ2
PROPERTIES
Σ = {0,1}
Z1 ⊆ Z ∧ Z1 = {z10,z11,z12} ∧
F1 ⊆ Z1 ∧ S1 ⊆ Z1 ∧
δ1 ∈ (Z1×Σ) → ℙ(Z1)
// Der Automat M1 (L(M1)={w| |w|=0 ∨ w=u0 mit u∈{0,1}*}):
S1 = {z10} ∧ F1 = {z10, z12} ∧
δ1 = { (z10,0)↦{z12}, (z10,1)↦{z11},
(z11,0)↦{z12}, (z11,1)↦{z11},
(z12,0)↦{z12}, (z12,1)↦{z11}} ∧
Z2 ⊆ Z ∧ Z2 = {z20,z21,z22} ∧
F2 ⊆ Z2 ∧ S2 ⊆ Z2 ∧
δ2 ∈ (Z2×Σ) → ℙ(Z2)
// Der Automat M2 (L(M2)={1^n|n∈ℕ_0}):
S2 = {z20, z21} ∧ F2 = {z20, z21} ∧
δ2 = { (z20,0)↦{z22}, (z20,1)↦{z21},
(z21,0)↦{z22}, (z21,1)↦{z21},
(z22,0)↦{z22}, (z22,1)↦{z22}} ∧
//TODO Referenz auf Buch einbauen!
Z1 ∩ Z2 = ∅ ∧
Z= Z1 ∪ Z2 ∧
Z_gesamt = {x | ∃a,b.(a∈Z1 ∧ b∈Z2 ∧ x=(a, b))}∧
S = S1*S2 ∧
F = F1*(Z2\F2) ∧
δ = {x | x∈((Z*Z)*INTEGER)*POW(Z_gesamt) ∧
∃zustand1,zustand2,symbol,menge.(
x=((zustand1, zustand2), symbol)↦menge ∧
zustand1∈Z1 ∧ zustand2∈Z2 ∧ symbol∈Σ ∧
menge = δ1(zustand1, symbol)*δ2(zustand2, symbol))}
∧ f ∈ seq(Z_gesamt) ∧ ran(f) = Z_gesamt
DEFINITIONS // Für den Zustandsgraphen:
ANIMATION_FUNCTION1 == {r,c,i| r∈dom(f) ∧ c=0 ∧ i=f(r)};
ANIMATION_FUNCTION2 == {(0,0,"Zustand"),(0,1,"δ(Zustand,0)"),(0,2,"δ(Zustand,1)")};
ANIMATION_FUNCTION3 == {r,c,i| r∈dom(f) ∧ c=1 ∧ i=δ(f(r), 0)};
ANIMATION_FUNCTION4 == {r,c,i| r∈dom(f) ∧ c=2 ∧ i=δ(f(r), 1)};
END
```
%% Output
Loaded machine: NFA
%% Cell type:code id: tags:
``` prob
:constants
```
%% Output
Machine constants set up using operation 0: $setup_constants()
%% Cell type:code id: tags:
``` prob
:init
```
%% Output
Machine initialised using operation 1: $initialise_machine()
%% Cell type:code id: tags:
``` prob
:show
```
%% Output
<table style="font-family:monospace"><tbody>
<tr>
<td style="padding:10px">Zustand</td>
<td style="padding:10px">δ(Zustand,0)</td>
<td style="padding:10px">δ(Zustand,1)</td>
</tr>
<tr>
<td style="padding:10px">(z10|->z20)</td>
<td style="padding:10px">{(z12|->z22)}</td>
<td style="padding:10px">{(z11|->z21)}</td>
</tr>
<tr>
<td style="padding:10px">(z10|->z21)</td>
<td style="padding:10px">{(z12|->z22)}</td>
<td style="padding:10px">{(z11|->z21)}</td>
</tr>
<tr>
<td style="padding:10px">(z10|->z22)</td>
<td style="padding:10px">{(z12|->z22)}</td>
<td style="padding:10px">{(z11|->z22)}</td>
</tr>
<tr>
<td style="padding:10px">(z11|->z20)</td>
<td style="padding:10px">{(z12|->z22)}</td>
<td style="padding:10px">{(z11|->z21)}</td>
</tr>
<tr>
<td style="padding:10px">(z11|->z21)</td>
<td style="padding:10px">{(z12|->z22)}</td>
<td style="padding:10px">{(z11|->z21)}</td>
</tr>
<tr>
<td style="padding:10px">(z11|->z22)</td>
<td style="padding:10px">{(z12|->z22)}</td>
<td style="padding:10px">{(z11|->z22)}</td>
</tr>
<tr>
<td style="padding:10px">(z12|->z20)</td>
<td style="padding:10px">{(z12|->z22)}</td>
<td style="padding:10px">{(z11|->z21)}</td>
</tr>
<tr>
<td style="padding:10px">(z12|->z21)</td>
<td style="padding:10px">{(z12|->z22)}</td>
<td style="padding:10px">{(z11|->z21)}</td>
</tr>
<tr>
<td style="padding:10px">(z12|->z22)</td>
<td style="padding:10px">{(z12|->z22)}</td>
<td style="padding:10px">{(z11|->z22)}</td>
</tr>
</tbody></table>
<Animation function visualisation>
%% Cell type:markdown id: tags:
Indem man die Endzustände so wählt, dass man in einem Enzustand beider NFAs landet, kann man auch zeigen, dass der Schnitt zweier regulärer Sprachen regulär ist.
%% Cell type:code id: tags:
``` prob
::load
MACHINE NFA
SETS
Z = {z10,z11, z12, z20,z21,z22}
CONSTANTS Σ, Z_gesamt, S, F, δ, f,
Z1, S1, F1, δ1,
Z2, S2, F2, δ2
PROPERTIES
Σ = {0,1}
Z1 ⊆ Z ∧ Z1 = {z10,z11,z12} ∧
F1 ⊆ Z1 ∧ S1 ⊆ Z1 ∧
δ1 ∈ (Z1×Σ) → ℙ(Z1)
// Der Automat M1 (L(M1)={w| |w|=0 ∨ w=u0 mit u∈{0,1}*}):
S1 = {z10} ∧ F1 = {z10, z12} ∧
δ1 = { (z10,0)↦{z12}, (z10,1)↦{z11},
(z11,0)↦{z12}, (z11,1)↦{z11},
(z12,0)↦{z12}, (z12,1)↦{z11}} ∧
Z2 ⊆ Z ∧ Z2 = {z20,z21,z22} ∧
F2 ⊆ Z2 ∧ S2 ⊆ Z2 ∧
δ2 ∈ (Z2×Σ) → ℙ(Z2)
// Der Automat M2 (L(M2)={1^n|n∈ℕ_0}):
S2 = {z20, z21} ∧ F2 = {z20, z21} ∧
δ2 = { (z20,0)↦{z22}, (z20,1)↦{z21},
(z21,0)↦{z22}, (z21,1)↦{z21},
(z22,0)↦{z22}, (z22,1)↦{z22}} ∧
//Konstruktion analog zu TODO Referenz auf Buch
Z1 ∩ Z2 = ∅ ∧
Z= Z1 ∪ Z2 ∧
Z_gesamt = {x | ∃a,b.(a∈Z1 ∧ b∈Z2 ∧ x=(a, b))}∧
S = S1*S2 ∧
F = F1*F2 ∧
δ = {x | x∈((Z*Z)*INTEGER)*POW(Z_gesamt) ∧
∃zustand1,zustand2,symbol,menge.(
x=((zustand1, zustand2), symbol)↦menge ∧
zustand1∈Z1 ∧ zustand2∈Z2 ∧ symbol∈Σ ∧
menge = δ1(zustand1, symbol)*δ2(zustand2, symbol))}
∧ f ∈ seq(Z_gesamt) ∧ ran(f) = Z_gesamt
DEFINITIONS // Für den Zustandsgraphen:
"LibraryStrings.def";
ANIMATION_FUNCTION1 == {r,c,i| r∈dom(f) ∧ c=0 ∧ i=f(r)};
ANIMATION_FUNCTION2 == {(0,0,"Zustand"),(0,1,"δ(Zustand,0)"),(0,2,"δ(Zustand,1)")};
ANIMATION_FUNCTION3 == {r,c,i| r∈dom(f) ∧ c=1 ∧ i=δ(f(r), 0)};
ANIMATION_FUNCTION4 == {r,c,i| r∈dom(f) ∧ c=2 ∧ i=δ(f(r), 1)};
END
```
%% Output
Loaded machine: NFA
%% Cell type:code id: tags:
``` prob
:constants
```
%% Output
Machine constants set up using operation 0: $setup_constants()
%% Cell type:code id: tags:
``` prob
:init
```
%% Output
Machine initialised using operation 1: $initialise_machine()
%% Cell type:code id: tags:
``` prob
:show
```
%% Output
<table style="font-family:monospace"><tbody>
<tr>
<td style="padding:10px">Zustand</td>
<td style="padding:10px">δ(Zustand,0)</td>
<td style="padding:10px">δ(Zustand,1)</td>
</tr>
<tr>
<td style="padding:10px">(z10|->z20)</td>
<td style="padding:10px">{(z12|->z22)}</td>
<td style="padding:10px">{(z11|->z21)}</td>
</tr>
<tr>
<td style="padding:10px">(z10|->z21)</td>
<td style="padding:10px">{(z12|->z22)}</td>
<td style="padding:10px">{(z11|->z21)}</td>
</tr>
<tr>
<td style="padding:10px">(z10|->z22)</td>
<td style="padding:10px">{(z12|->z22)}</td>
<td style="padding:10px">{(z11|->z22)}</td>
</tr>
<tr>
<td style="padding:10px">(z11|->z20)</td>
<td style="padding:10px">{(z12|->z22)}</td>
<td style="padding:10px">{(z11|->z21)}</td>
</tr>
<tr>
<td style="padding:10px">(z11|->z21)</td>
<td style="padding:10px">{(z12|->z22)}</td>
<td style="padding:10px">{(z11|->z21)}</td>
</tr>
<tr>
<td style="padding:10px">(z11|->z22)</td>
<td style="padding:10px">{(z12|->z22)}</td>
<td style="padding:10px">{(z11|->z22)}</td>
</tr>
<tr>
<td style="padding:10px">(z12|->z20)</td>
<td style="padding:10px">{(z12|->z22)}</td>
<td style="padding:10px">{(z11|->z21)}</td>
</tr>
<tr>
<td style="padding:10px">(z12|->z21)</td>
<td style="padding:10px">{(z12|->z22)}</td>
<td style="padding:10px">{(z11|->z21)}</td>
</tr>
<tr>
<td style="padding:10px">(z12|->z22)</td>
<td style="padding:10px">{(z12|->z22)}</td>
<td style="padding:10px">{(z11|->z22)}</td>
</tr>
</tbody></table>
<Animation function visualisation>
%% Cell type:markdown id: tags:
Zuletzt bleibt noch die Spiegelung einer Sprache. Um dies zu erreichen erstellen wir aus einem DFA einen NFA.
%% Cell type:code id: tags:
``` prob
::load
MACHINE DFA
SETS
Z = {z0,z1,z2,z3}
CONSTANTS Σ, M, δ, δ2, F, M2, z_start
PROPERTIES
M = (Σ, Z, δ, z_start, F) ∧
M2 = (Σ, Z, δ2, F, {z_start}) ∧
z_start ∈ Z ∧
F ⊆ Z ∧
δ ∈ (Z×Σ) → Z ∧
δ2 ∈ (Z×Σ) <-> ℙ(Z) ∧
δ2 = {x |∃a,s,s2.(x=(s2, a, {s}) ∧ a∈Σ ∧ s∈Z ∧ s2∈Z ∧ δ(s,a) = s2)} ∧
Σ = {0,1}
DEFINITIONS // Für den Zustandsgraphen:
CUSTOM_GRAPH_NODES1 == rec(shape:"doublecircle",nodes:{z_start}); // Endzustände
CUSTOM_GRAPH_NODES2 == rec(shape:"circle",nodes:Z\{z_start}); // andere Zustände
CUSTOM_GRAPH_NODES3 == rec(shape:"none",color:"white",style:"none",nodes:{""});
CUSTOM_GRAPH_EDGES1 == rec(color:"green",label:"0",edges:{x,z| ∃y.(y∈δ2[{(x,0)}] ∧ y∉δ2[{(x,1)}] ∧ z:y)});
CUSTOM_GRAPH_EDGES2 == rec(color:"green",label:"1",edges:{x,z| ∃y.(y∈δ2[{(x,1)}] ∧ y∉δ2[{(x,0)}] ∧ z:y)});
CUSTOM_GRAPH_EDGES3 == rec(color:"green",label:"0, 1",edges:{x,z| ∃y.(y∈δ2[{(x,0)}] ∧ y∈δ2[{(x,1)}] ∧ z:y)});
CUSTOM_GRAPH_EDGES4 == rec(color:"black",label:"",edges:{""}*F) // Kanten für Startknoten
END
```
%% Output
Loaded machine: DFA
%% Cell type:code id: tags:
``` prob
:constants M=({0,1}, //Σ
{z0,z1,z2,z3}, //Z
{(z0,0)↦z1, (z0,1)↦z3,
(z1,0)↦z3, (z1,1)↦z2,
(z2,0)↦z2, (z2,1)↦z2,
(z3,0)↦z3, (z3,1)↦z3 }, //δ
z0, {z0, z2}) //z0, F
```
%% Output
Machine constants set up using operation 0: $setup_constants()
%% Cell type:code id: tags:
``` prob
:dot custom_graph
```
%% Output
<Dot visualization: custom_graph []>
%% Cell type:code id: tags:
``` prob
δ2
```
%% Output
$\{(\mathit{z1}\mapsto 0\mapsto\{\mathit{z0}\}),(\mathit{z2}\mapsto 0\mapsto\{\mathit{z2}\}),(\mathit{z2}\mapsto 1\mapsto\{\mathit{z1}\}),(\mathit{z2}\mapsto 1\mapsto\{\mathit{z2}\}),(\mathit{z3}\mapsto 0\mapsto\{\mathit{z1}\}),(\mathit{z3}\mapsto 0\mapsto\{\mathit{z3}\}),(\mathit{z3}\mapsto 1\mapsto\{\mathit{z0}\}),(\mathit{z3}\mapsto 1\mapsto\{\mathit{z3}\})\}$
{(z1↦0↦{z0}),(z2↦0↦{z2}),(z2↦1↦{z1}),(z2↦1↦{z2}),(z3↦0↦{z1}),(z3↦0↦{z3}),(z3↦1↦{z0}),(z3↦1↦{z3})}
%% Cell type:code id: tags:
``` prob
{x,z| ∃y.(y∈δ2[{(x,0)}] ∧ y∉δ2[{(x,1)}] ∧ z:y)}
```
%% Output
$\{(\mathit{z1}\mapsto \mathit{z0}),(\mathit{z3}\mapsto \mathit{z1})\}$
{(z1↦z0),(z3↦z1)}
%% Cell type:code id: tags:
``` prob
δ2[{(z1,0)}]
```
%% Output
$\{\{\mathit{z0}\}\}$
{{z0}}
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment