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

Referenz eingefügt

parent 63d4f5e1
Branches
No related tags found
1 merge request!1Master
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
# Abschlusseigenschaften regulärer Sprachen # Abschlusseigenschaften regulärer Sprachen
Abschlusseigenschaften sind ein weiteres nützliches Werkzeug um verschiedene Sprachklassen zu charakterisieren. 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. Damit kann man untersuchen, ob eine Sprache zu einer Sprachklasse gehört oder nicht.
Die regulären Sprachen sind abgeschlossen unter: Die regulären Sprachen sind abgeschlossen unter:
* Vereinigung A ∪ B * Vereinigung A ∪ B
* Komplement A̅ * Komplement A̅
* Schnitt A ∩ B * Schnitt A ∩ B
* Differenz A/B * Differenz A/B
* Konkatenation AB * Konkatenation AB
* Iteration A* * Iteration A*
* Spiegelung sp(A) * Spiegelung sp(A)
In den Folien wird diese Aussage zwar aufgestellt, aber nicht bewiesen. In den Folien wird diese Aussage zwar aufgestellt, aber nicht bewiesen.
Hier schauen wir uns für einige Operationen Beweisideen an konkreten Beispielen an. Hier schauen wir uns für einige Operationen Beweisideen an konkreten Beispielen an.
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Zuerst betrachten wir die Vereinigung. Zuerst betrachten wir die Vereinigung.
Zu jeder regulären Sprache kann man auch einen NFA angeben. Zu jeder regulären Sprache kann man auch einen NFA angeben.
Wenn $M_1=(Σ, Z_1, δ_1, S_1, F_1)$ und $M_2=(Σ, Z_2, δ_2, S_2, F_2)$ zwei NFAs sind, dann lässt sich ein Vereinigungs-NFA $M=(Σ, Z_1 ∪ Z_2, δ_1∪δ_2, S_1∪S_2, F_1∪F_2)$ 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). Wenn $M_1=(Σ, Z_1, δ_1, S_1, F_1)$ und $M_2=(Σ, Z_2, δ_2, S_2, F_2)$ zwei NFAs sind, dann lässt sich ein Vereinigungs-NFA $M=(Σ, Z_1 ∪ Z_2, δ_1∪δ_2, S_1∪S_2, F_1∪F_2)$ 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: %% Cell type:code id: tags:
``` prob ``` prob
::load ::load
MACHINE NFA MACHINE NFA
SETS SETS
Z = {z10,z11,z12,z13, z20,z21,z22} Z = {z10,z11,z12,z13, z20,z21,z22}
CONSTANTS Σ, M, δ, S, F, CONSTANTS Σ, M, δ, S, F,
M1, Z1, δ1, S1, F1, M1, Z1, δ1, S1, F1,
M2, Z2, δ2, S2, F2 M2, Z2, δ2, S2, F2
PROPERTIES PROPERTIES
Σ = {0,1} ∧ Σ = {0,1} ∧
Z1 ∩ Z2 = ∅ Z1 ∩ Z2 = ∅
// Der Automat M1 von Folie 21 (L(M1)={u1v|u∈{0,1}* ∧ v∈{0,1}}): // Der Automat M1 von Folie 21 (L(M1)={u1v|u∈{0,1}* ∧ v∈{0,1}}):
M1=(Σ, Z1, δ1, S1, F1) ∧ M1=(Σ, Z1, δ1, S1, F1) ∧
Z1 ⊆ Z ∧ Z1 ⊆ Z ∧
δ1 ∈ (Z1×Σ) → ℙ(Z1) ∧ δ1 ∈ (Z1×Σ) → ℙ(Z1) ∧
S1 ⊆ Z1 ∧ F1 ⊆ Z1 S1 ⊆ Z1 ∧ F1 ⊆ Z1
Z1 = {z10,z11,z12,z13} ∧ Z1 = {z10,z11,z12,z13} ∧
S1 = {z10} ∧ F1 = {z12} ∧ S1 = {z10} ∧ F1 = {z12} ∧
δ1 = { (z10,0)↦{z10}, (z10,1)↦{z10,z11}, δ1 = { (z10,0)↦{z10}, (z10,1)↦{z10,z11},
(z11,0)↦{z12}, (z11,1)↦{z12}, (z11,0)↦{z12}, (z11,1)↦{z12},
(z12,0)↦{z13}, (z12,1)↦{z13}, (z12,0)↦{z13}, (z12,1)↦{z13},
(z13,0)↦{z13}, (z13,1)↦{z13} } (z13,0)↦{z13}, (z13,1)↦{z13} }
// Der Automat M2 von Folie 28 (L(M2)={u1|u∈{0,1}*}): // Der Automat M2 von Folie 28 (L(M2)={u1|u∈{0,1}*}):
M2=(Σ, Z2, δ2, S2, F2) ∧ M2=(Σ, Z2, δ2, S2, F2) ∧
Z2 ⊆ Z ∧ Z2 ⊆ Z ∧
δ2 ∈ (Z2×Σ) → ℙ(Z2) ∧ δ2 ∈ (Z2×Σ) → ℙ(Z2) ∧
S2 ⊆ Z2 ∧ F2 ⊆ Z2 S2 ⊆ Z2 ∧ F2 ⊆ Z2
Z2 = {z20,z21,z22} ∧ Z2 = {z20,z21,z22} ∧
S2 = {z20} ∧ F2 = {z21} ∧ S2 = {z20} ∧ F2 = {z21} ∧
δ2 = { (z20,0)↦{z20}, (z20,1)↦{z20,z21}, δ2 = { (z20,0)↦{z20}, (z20,1)↦{z20,z21},
(z21,0)↦{z22}, (z21,1)↦{z22}, (z21,0)↦{z22}, (z21,1)↦{z22},
(z22,0)↦{z22}, (z22,1)↦{z22}} (z22,0)↦{z22}, (z22,1)↦{z22}}
//Der Vereinigungsautomat M: //Der Vereinigungsautomat M:
M=(Σ, Z, δ, S, F) ∧ M=(Σ, Z, δ, S, F) ∧
Z= Z1 ∪ Z2 ∧ Z= Z1 ∪ Z2 ∧
δ = δ1 ∪ δ2 ∧ δ = δ1 ∪ δ2 ∧
S = S1 ∪ S2 ∧ S = S1 ∪ S2 ∧
F = F1 ∪ F2 F = F1 ∪ F2
DEFINITIONS // Für den Zustandsgraphen: DEFINITIONS // Für den Zustandsgraphen:
CUSTOM_GRAPH_NODES1 == rec(shape:"doublecircle",nodes:F); // Endzustände CUSTOM_GRAPH_NODES1 == rec(shape:"doublecircle",nodes:F); // Endzustände
CUSTOM_GRAPH_NODES2 == rec(shape:"circle",nodes:Z\F); // andere Zustä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_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_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_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_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 CUSTOM_GRAPH_EDGES4 == rec(color:"black",label:"",edges:{""}*S) // Kanten für Startknoten
END END
``` ```
%% Output %% Output
Loaded machine: NFA Loaded machine: NFA
%% 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() Machine constants set up using operation 0: $setup_constants()
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Hier sieht man auf der linken Seite $M_1$, auf der rechten $M_2$ und das gesamte Bild stellt den Vereinigungsautomaten $M$ dar. Hier sieht man auf der linken Seite $M_1$, auf der rechten $M_2$ und das gesamte Bild stellt den Vereinigungsautomaten $M$ dar.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:dot custom_graph :dot custom_graph
``` ```
%% Output %% Output
<Dot visualization: custom_graph []> <Dot visualization: custom_graph []>
%% Cell type:markdown id: tags: %% 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, δ, z_0, F)$ ein DFA mit $L(M)=L$. Dann gilt für $M_2=(Σ, Z, δ, z_0, Z/F)$, dass $L(M_2)= \overline{L}$. Dies kann man auch mit folgender Machiene darstellen: Eine weitere Eigenschaft, die man leicht zeigen kann ist, dass das Komplement einer Sprache $L$ regulär ist. Sei $M=(Σ, Z, δ, z_0, F)$ ein DFA mit $L(M)=L$. Dann gilt für $M_2=(Σ, Z, δ, z_0, Z/F)$, dass $L(M_2)= \overline{L}$. Dies kann man auch mit folgender Machiene darstellen:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
::load ::load
MACHINE DFA MACHINE DFA
SETS SETS
Z = {z0,z1,z2,z3} Z = {z0,z1,z2,z3}
CONSTANTS Σ, M, δ, F, M2, z_start CONSTANTS Σ, M, δ, F, M2, z_start
PROPERTIES PROPERTIES
Σ = {0,1} Σ = {0,1}
M = (Σ, Z, δ, z_start, F) ∧ M = (Σ, Z, δ, z_start, F) ∧
M2 = (Σ, Z, δ, z_start, Z\F) ∧ M2 = (Σ, Z, δ, z_start, Z\F) ∧
δ ∈ (Z×Σ) → Z ∧ δ ∈ (Z×Σ) → Z ∧
z_start ∈ Z ∧ z_start ∈ Z ∧
F ⊆ Z F ⊆ Z
DEFINITIONS // Für den Zustandsgraphen: DEFINITIONS // Für den Zustandsgraphen:
CUSTOM_GRAPH_NODES1 == rec(shape:"doublecircle",nodes:Z\F); // Endzustände von M2 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_NODES2 == rec(shape:"circle",nodes:F); // andere Zustände von M2
CUSTOM_GRAPH_NODES3 == rec(shape:"none",color:"white",style:"none",nodes:{""}); 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_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_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 CUSTOM_GRAPH_EDGES3 == rec(color:"black",label:"",edges:{"" |-> z_start}) // Kante für den Startknoten
END END
``` ```
%% Output %% Output
Loaded machine: DFA Loaded machine: DFA
%% Cell type:markdown id: tags: %% 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. 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: %% Cell type:code id: tags:
``` prob ``` prob
:constants M=({0,1}, //Σ :constants M=({0,1}, //Σ
{z0,z1,z2,z3}, //Z {z0,z1,z2,z3}, //Z
{(z0,0)↦z1, (z0,1)↦z3, {(z0,0)↦z1, (z0,1)↦z3,
(z1,0)↦z3, (z1,1)↦z2, (z1,0)↦z3, (z1,1)↦z2,
(z2,0)↦z2, (z2,1)↦z2, (z2,0)↦z2, (z2,1)↦z2,
(z3,0)↦z3, (z3,1)↦z3 }, //δ (z3,0)↦z3, (z3,1)↦z3 }, //δ
z0, {z0, z2}) //z0, F z0, {z0, z2}) //z0, F
``` ```
%% Output %% Output
Machine constants set up using operation 0: $setup_constants() Machine constants set up using operation 0: $setup_constants()
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Hier sieht man $M_2$, der aus $M$ erzeugt wurde, indem man alle das Komplement der Endzustandsmenge als neue Endzustandsmenge wählt. Hier sieht man $M_2$, der aus $M$ erzeugt wurde, indem man alle das Komplement der Endzustandsmenge als neue Endzustandsmenge wählt.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:dot custom_graph :dot custom_graph
``` ```
%% Output %% Output
<Dot visualization: custom_graph []> <Dot visualization: custom_graph []>
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Als nächstes befassen wir uns mit der Konkatenation zweier Sprachen. Um dies zu erreichen schaltet man 2 NFAs $M_1=(Σ, Z_1, δ_1, S_1, F_1)$ udnd $M_2=(Σ, Z_2, δ_2, S_2, F_2)$ hintereinander. Dies erreicht man, indem man jedes Mal, wenn ein Zustand in $F_1$ erreicht wird zusätzlich auch alle Zustände in $S_2$ erreicht werden. Als nächstes befassen wir uns mit der Konkatenation zweier Sprachen. Um dies zu erreichen schaltet man 2 NFAs $M_1=(Σ, Z_1, δ_1, S_1, F_1)$ udnd $M_2=(Σ, Z_2, δ_2, S_2, F_2)$ hintereinander. Dies erreicht man, indem man jedes Mal, wenn ein Zustand in $F_1$ erreicht wird zusätzlich auch alle Zustände in $S_2$ erreicht werden.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
::load ::load
MACHINE NFA MACHINE NFA
SETS SETS
Z = {z10,z11, z12, z20,z21,z22} Z = {z10,z11, z12, z20,z21,z22}
CONSTANTS Σ, M, δ, S, F, CONSTANTS Σ, M, δ, S, F,
M1, Z1, δ1, S1, F1, M1, Z1, δ1, S1, F1,
M2, Z2, δ2, S2, F2 M2, Z2, δ2, S2, F2
PROPERTIES PROPERTIES
Σ = {0,1} ∧ Σ = {0,1} ∧
Z1 ∩ Z2 = ∅ Z1 ∩ Z2 = ∅
// Der Automat M1 (L(M1)={w| |w|=0 ∨ w=u0 mit u∈{0,1}*}): // Der Automat M1 (L(M1)={w| |w|=0 ∨ w=u0 mit u∈{0,1}*}):
M1=(Σ, Z1, δ1, S1, F1) ∧ M1=(Σ, Z1, δ1, S1, F1) ∧
Z1 ⊆ Z ∧ Z1 = {z10,z11,z12} ∧ Z1 ⊆ Z ∧ Z1 = {z10,z11,z12} ∧
δ1 ∈ (Z1×Σ) → ℙ(Z1) ∧ δ1 ∈ (Z1×Σ) → ℙ(Z1) ∧
S1 ⊆ Z1 ∧ F1 ⊆ Z1 S1 ⊆ Z1 ∧ F1 ⊆ Z1
S1 = {z10} ∧ F1 = {z10, z12} ∧ S1 = {z10} ∧ F1 = {z10, z12} ∧
δ1 = { (z10,0)↦{z12}, (z10,1)↦{z11}, δ1 = { (z10,0)↦{z12}, (z10,1)↦{z11},
(z11,0)↦{z12}, (z11,1)↦{z11}, (z11,0)↦{z12}, (z11,1)↦{z11},
(z12,0)↦{z12}, (z12,1)↦{z11}} ∧ (z12,0)↦{z12}, (z12,1)↦{z11}} ∧
// Der Automat M2 (L(M2)={1^n|n∈ℕ_0}): // Der Automat M2 (L(M2)={1^n|n∈ℕ_0}):
M2 = (Σ, Z2, δ2, S2, F2) ∧ M2 = (Σ, Z2, δ2, S2, F2) ∧
Z2 ⊆ Z ∧ Z2 = {z20,z21,z22} ∧ Z2 ⊆ Z ∧ Z2 = {z20,z21,z22} ∧
δ2 ∈ (Z2×Σ) → ℙ(Z2) ∧ δ2 ∈ (Z2×Σ) → ℙ(Z2) ∧
S2 ⊆ Z2 ∧ F2 ⊆ Z2 S2 ⊆ Z2 ∧ F2 ⊆ Z2
S2 = {z20} ∧ F2 = {z21} ∧ S2 = {z20} ∧ F2 = {z21} ∧
δ2 = { (z20,0)↦{z22}, (z20,1)↦{z21}, δ2 = { (z20,0)↦{z22}, (z20,1)↦{z21},
(z21,0)↦{z22}, (z21,1)↦{z21}, (z21,0)↦{z22}, (z21,1)↦{z21},
(z22,0)↦{z22}, (z22,1)↦{z22}} ∧ (z22,0)↦{z22}, (z22,1)↦{z22}} ∧
//Die Regeln von Folie 51: //Die Regeln von Folie 51:
M = (Σ, Z, δ, S, F) ∧ M = (Σ, Z, δ, S, F) ∧
Z = Z1 ∪ Z2 ∧ Z = Z1 ∪ Z2 ∧
S = S1 ∪ ran((S1∩F1)*S2) ∧ S = S1 ∪ ran((S1∩F1)*S2) ∧
F = F2 ∪ ran((S2∩F2)*F1) ∧ F = F2 ∪ ran((S2∩F2)*F1) ∧
δ = {x | x∈(Z*INTEGER)*POW(Z) ∧ δ = {x | x∈(Z*INTEGER)*POW(Z) ∧
∃zustand,symbol,menge.(x=(zustand, symbol)↦menge ∧ ( ∃zustand,symbol,menge.(x=(zustand, symbol)↦menge ∧ (
(zustand∈Z1 ∧ menge = δ1(zustand,symbol) ∧ δ1(zustand,symbol)∩F1= ∅) ∨ (zustand∈Z1 ∧ menge = δ1(zustand,symbol) ∧ δ1(zustand,symbol)∩F1= ∅) ∨
(zustand∈Z1 ∧ menge = δ1(zustand,symbol) ∪ S2 ∧ δ1(zustand,symbol)∩F1 ≠ ∅) ∨ (zustand∈Z1 ∧ menge = δ1(zustand,symbol) ∪ S2 ∧ δ1(zustand,symbol)∩F1 ≠ ∅) ∨
(zustand∈Z2 ∧ menge = δ2(zustand,symbol))))} (zustand∈Z2 ∧ menge = δ2(zustand,symbol))))}
DEFINITIONS // Für den Zustandsgraphen: DEFINITIONS // Für den Zustandsgraphen:
CUSTOM_GRAPH_NODES1 == rec(shape:"doublecircle",nodes:F); // Endzustände CUSTOM_GRAPH_NODES1 == rec(shape:"doublecircle",nodes:F); // Endzustände
CUSTOM_GRAPH_NODES2 == rec(shape:"circle",nodes:Z\F); // andere Zustä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_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_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_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_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 CUSTOM_GRAPH_EDGES4 == rec(color:"black",label:"",edges:{""}*S) // Kanten für Startknoten
END END
``` ```
%% Output %% Output
Loaded machine: NFA Loaded machine: NFA
%% 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() Machine constants set up using operation 0: $setup_constants()
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:dot custom_graph :dot custom_graph
``` ```
%% Output %% Output
<Dot visualization: custom_graph []> <Dot visualization: custom_graph []>
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Um zu zeigen, dass die Iteration einer regulären Sprache wieder regulär ist, bilden wir zu einem NFA $M=(Σ, Z_1, δ_1, S_1, F_1)$ einen Rückkopplungsautomaten $M_2$. Wir starten damit den $M$ mit sich selbst zu verketten (analog zur Konkatenation). Dann müssen wir nur noch sichergehen, dass das leere Wort akzeptiert wird. Dafür fügen wir (falls notwendig) einen Zustand ein, der sowohl Start- als auch Endzustand ist. Um zu zeigen, dass die Iteration einer regulären Sprache wieder regulär ist, bilden wir zu einem NFA $M=(Σ, Z_1, δ_1, S_1, F_1)$ einen Rückkopplungsautomaten $M_2$. Wir starten damit den $M$ mit sich selbst zu verketten (analog zur Konkatenation). Dann müssen wir nur noch sichergehen, dass das leere Wort akzeptiert wird. Dafür fügen wir (falls notwendig) einen Zustand ein, der sowohl Start- als auch Endzustand ist.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
::load ::load
MACHINE NFA MACHINE NFA
SETS SETS
Z = {z10,z11, z12, z} Z = {z10,z11, z12, z}
CONSTANTS Σ, M, δ, CONSTANTS Σ, M, δ,
M1, Z1, δ1, S1, F1, M1, Z1, δ1, S1, F1,
M2, Z2, δ2, S2, F2 M2, Z2, δ2, S2, F2
PROPERTIES PROPERTIES
Σ = {0,1} Σ = {0,1}
// Der Automat M1 (L(M1)={w| w=u0 mit u∈{0,1}*}): // Der Automat M1 (L(M1)={w| w=u0 mit u∈{0,1}*}):
M1 = (Σ, Z1, δ1, S1, F1) ∧ M1 = (Σ, Z1, δ1, S1, F1) ∧
Z1 ⊆ Z ∧ Z1 = {z10,z11,z12} ∧ Z1 ⊆ Z ∧ Z1 = {z10,z11,z12} ∧
δ1 ∈ (Z1×Σ) → ℙ(Z1) ∧ δ1 ∈ (Z1×Σ) → ℙ(Z1) ∧
S1 ⊆ Z1 ∧ F1 ⊆ Z1 S1 ⊆ Z1 ∧ F1 ⊆ Z1
S1 = {z10} ∧ F1 = {z12} ∧ S1 = {z10} ∧ F1 = {z12} ∧
δ1 = { (z10,0)↦{z12}, (z10,1)↦{z11}, δ1 = { (z10,0)↦{z12}, (z10,1)↦{z11},
(z11,0)↦{z12}, (z11,1)↦{z11}, (z11,0)↦{z12}, (z11,1)↦{z11},
(z12,0)↦{z12}, (z12,1)↦{z11}} ∧ (z12,0)↦{z12}, (z12,1)↦{z11}} ∧
//Die Regeln von Folie 53 //Die Regeln von Folie 53
M2 = (Σ, Z2, δ2, S2, F2) ∧ M2 = (Σ, Z2, δ2, S2, F2) ∧
Z2 ⊆ Z ∧ Z2 ⊆ Z ∧
δ2 ∈ (Z2×Σ) +-> ℙ(Z2) ∧ δ2 ∈ (Z2×Σ) +-> ℙ(Z2) ∧
S2 ⊆ Z2 ∧ F2 ⊆ Z2 S2 ⊆ Z2 ∧ F2 ⊆ Z2
Z2 = IF S1∩F1 ≠ ∅ THEN Z1 ELSE Z1∪{z} END ∧ Z2 = IF S1∩F1 ≠ ∅ THEN Z1 ELSE Z1∪{z} END ∧
δ2 = δ1 ∧ δ2 = δ1 ∧
S2 = IF S1∩F1 ≠ ∅ THEN S1 ELSE S1∪{z} END ∧ S2 = IF S1∩F1 ≠ ∅ THEN S1 ELSE S1∪{z} END ∧
F2 = IF S1∩F1 ≠ ∅ THEN F1 ELSE F1∪{z} END ∧ F2 = IF S1∩F1 ≠ ∅ THEN F1 ELSE F1∪{z} END ∧
//Die Regeln von Folie 54: //Die Regeln von Folie 54:
M = (Σ, Z2, δ, S2, F2) ∧ M = (Σ, Z2, δ, S2, F2) ∧
δ = {x | x∈(Z*INTEGER)*POW(Z) ∧ δ = {x | x∈(Z*INTEGER)*POW(Z) ∧
∃zustand,symbol,menge.(x=(zustand, symbol)↦menge ∧ ( ∃zustand,symbol,menge.(x=(zustand, symbol)↦menge ∧ (
(zustand∈Z2 ∧ menge = δ2(zustand,symbol) ∧ δ2(zustand,symbol)∩F2= ∅) ∨ (zustand∈Z2 ∧ menge = δ2(zustand,symbol) ∧ δ2(zustand,symbol)∩F2= ∅) ∨
(zustand∈Z2 ∧ menge = δ2(zustand,symbol) ∪ S2 ∧ δ2(zustand,symbol)∩F2 ≠ ∅)))} (zustand∈Z2 ∧ menge = δ2(zustand,symbol) ∪ S2 ∧ δ2(zustand,symbol)∩F2 ≠ ∅)))}
DEFINITIONS // Für den Zustandsgraphen: DEFINITIONS // Für den Zustandsgraphen:
CUSTOM_GRAPH_NODES1 == rec(shape:"doublecircle",nodes:F2); // Endzustände CUSTOM_GRAPH_NODES1 == rec(shape:"doublecircle",nodes:F2); // Endzustände
CUSTOM_GRAPH_NODES2 == rec(shape:"circle",nodes:Z2\F2); // andere Zustä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_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_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_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_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 CUSTOM_GRAPH_EDGES4 == rec(color:"black",label:"",edges:{""}*S2) // Kanten für Startknoten
END END
``` ```
%% Output %% Output
Loaded machine: NFA Loaded machine: NFA
%% 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() Machine constants set up using operation 0: $setup_constants()
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:dot custom_graph :dot custom_graph
``` ```
%% Output %% Output
<Dot visualization: custom_graph []> <Dot visualization: custom_graph []>
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Im folgenden schauen wir uns die Differenz zweier Sprachen $L1-L2$ genauer an. Im folgenden schauen wir uns die Differenz zweier Sprachen $L1-L2$ genauer an.
Das Vorgehen ist hierbei, dass man zwei NFAs $M_1=(Σ, Z_1, δ_1, S_1, F_1)$ udnd $M_2=(Σ, Z_2, δ_2, S_2, F_2)$ parallel ausführt und die Endzustandsmenge so wählt, dass man in einem Zustand aus $F_1$, aber nicht gleichzeitig in einem aus $F_2$ landet. Das Vorgehen (aus dem Buch [Grundkurs Theoretische Informatik](https://link.springer.com/content/pdf/10.1007/978-3-8348-2202-4.pdf "Vossen, G., & Witt, K. U. (2016). Grundkurs Theoretische Informatik. Springer Fachmedien Wiesbaden.") von G. Vossen & K. U. Witt, Seite 99f.) ist hierbei, dass man zwei NFAs $M_1=(Σ, Z_1, δ_1, S_1, F_1)$ udnd $M_2=(Σ, Z_2, δ_2, S_2, F_2)$ parallel ausführt und die Endzustandsmenge so wählt, dass man in einem Zustand aus $F_1$, aber nicht gleichzeitig in einem aus $F_2$ landet.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
::load ::load
MACHINE NFA MACHINE NFA
SETS SETS
Z = {z10,z11, z12, z20,z21,z22} Z = {z10,z11, z12, z20,z21,z22}
CONSTANTS Σ, M, Z_gesamt, δ, S, F, f, CONSTANTS Σ, M, Z_gesamt, δ, S, F, f,
M1, Z1, δ1, S1, F1, M1, Z1, δ1, S1, F1,
M2, Z2, δ2, S2, F2 M2, Z2, δ2, S2, F2
PROPERTIES PROPERTIES
Σ = {0,1} ∧ Σ = {0,1} ∧
Z1 ∩ Z2 = ∅ ∧ Z1 ∩ Z2 = ∅ ∧
Z= Z1 ∪ Z2 Z= Z1 ∪ Z2
// Der Automat M1 (L(M1)={w| |w|=0 ∨ w=u0 mit u∈{0,1}*}): // Der Automat M1 (L(M1)={w| |w|=0 ∨ w=u0 mit u∈{0,1}*}):
M1 = (Σ, Z1, δ1, S1, F1) ∧ M1 = (Σ, Z1, δ1, S1, F1) ∧
Z1 ⊆ Z ∧ Z1 ⊆ Z ∧
δ1 ∈ (Z1×Σ) → ℙ(Z1) ∧ δ1 ∈ (Z1×Σ) → ℙ(Z1) ∧
S1 ⊆ Z1 ∧ F1 ⊆ Z1 S1 ⊆ Z1 ∧ F1 ⊆ Z1
Z1 = {z10,z11,z12} ∧ Z1 = {z10,z11,z12} ∧
S1 = {z10} ∧ F1 = {z10, z12} ∧ S1 = {z10} ∧ F1 = {z10, z12} ∧
δ1 = { (z10,0)↦{z12}, (z10,1)↦{z11}, δ1 = { (z10,0)↦{z12}, (z10,1)↦{z11},
(z11,0)↦{z12}, (z11,1)↦{z11}, (z11,0)↦{z12}, (z11,1)↦{z11},
(z12,0)↦{z12}, (z12,1)↦{z11}} ∧ (z12,0)↦{z12}, (z12,1)↦{z11}} ∧
// Der Automat M2 (L(M2)={1^n|n∈ℕ_0}): // Der Automat M2 (L(M2)={1^n|n∈ℕ_0}):
M2 = (Σ, Z2, δ2, S2, F2) ∧ M2 = (Σ, Z2, δ2, S2, F2) ∧
Z2 ⊆ Z ∧ Z2 ⊆ Z ∧
δ2 ∈ (Z2×Σ) → ℙ(Z2) ∧ δ2 ∈ (Z2×Σ) → ℙ(Z2) ∧
S2 ⊆ Z2 ∧ F2 ⊆ Z2 S2 ⊆ Z2 ∧ F2 ⊆ Z2
Z2 = {z20,z21,z22} ∧ Z2 = {z20,z21,z22} ∧
S2 = {z20, z21} ∧ F2 = {z20, z21} ∧ S2 = {z20, z21} ∧ F2 = {z20, z21} ∧
δ2 = { (z20,0)↦{z22}, (z20,1)↦{z21}, δ2 = { (z20,0)↦{z22}, (z20,1)↦{z21},
(z21,0)↦{z22}, (z21,1)↦{z21}, (z21,0)↦{z22}, (z21,1)↦{z21},
(z22,0)↦{z22}, (z22,1)↦{z22}} ∧ (z22,0)↦{z22}, (z22,1)↦{z22}} ∧
//TODO Referenz auf Buch einbauen! //Der Automat nach "Grundkurs Theoretische Informatik"
M = (Σ, Z, δ, S, F) ∧ M = (Σ, Z, δ, S, F) ∧
Z_gesamt = Z1*Z2 ∧ Z_gesamt = Z1*Z2 ∧
S = S1*S2 ∧ S = S1*S2 ∧
F = F1*(Z2\F2) ∧ F = F1*(Z2\F2) ∧
δ = {x | x∈((Z1*Z2)*Σ)*ℙ(Z_gesamt) ∧ δ = {x | x∈((Z1*Z2)*Σ)*ℙ(Z_gesamt) ∧
∃zustand1,zustand2,symbol,menge.( ∃zustand1,zustand2,symbol,menge.(
x=((zustand1, zustand2), symbol)↦menge ∧ x=((zustand1, zustand2), symbol)↦menge ∧
zustand1∈Z1 ∧ zustand2∈Z2 ∧ symbol∈Σ ∧ zustand1∈Z1 ∧ zustand2∈Z2 ∧ symbol∈Σ ∧
menge = δ1(zustand1, symbol)*δ2(zustand2, symbol))} ∧ menge = δ1(zustand1, symbol)*δ2(zustand2, symbol))} ∧
//Eine Hilfsfunktion zur Visualisierung //Eine Hilfsfunktion zur Visualisierung
f ∈ seq(Z_gesamt) ∧ ran(f) = Z_gesamt f ∈ seq(Z_gesamt) ∧ ran(f) = Z_gesamt
DEFINITIONS // Für den Zustandsgraphen: DEFINITIONS // Für den Zustandsgraphen:
ANIMATION_FUNCTION1 == {r,c,i| r∈dom(f) ∧ c=0 ∧ i=f(r)}; 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_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_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)}; ANIMATION_FUNCTION4 == {r,c,i| r∈dom(f) ∧ c=2 ∧ i=δ(f(r), 1)};
END END
``` ```
%% Output %% Output
Loaded machine: NFA Loaded machine: NFA
%% 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() Machine constants set up using operation 0: $setup_constants()
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:init :init
``` ```
%% Output %% Output
Machine initialised using operation 1: $initialise_machine() Machine initialised using operation 1: $initialise_machine()
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:show :show
``` ```
%% Output %% Output
<table style="font-family:monospace"><tbody> <table style="font-family:monospace"><tbody>
<tr> <tr>
<td style="padding:10px">Zustand</td> <td style="padding:10px">Zustand</td>
<td style="padding:10px">δ(Zustand,0)</td> <td style="padding:10px">δ(Zustand,0)</td>
<td style="padding:10px">δ(Zustand,1)</td> <td style="padding:10px">δ(Zustand,1)</td>
</tr> </tr>
<tr> <tr>
<td style="padding:10px">(z10|->z20)</td> <td style="padding:10px">(z10|->z20)</td>
<td style="padding:10px">{(z12|->z22)}</td> <td style="padding:10px">{(z12|->z22)}</td>
<td style="padding:10px">{(z11|->z21)}</td> <td style="padding:10px">{(z11|->z21)}</td>
</tr> </tr>
<tr> <tr>
<td style="padding:10px">(z10|->z21)</td> <td style="padding:10px">(z10|->z21)</td>
<td style="padding:10px">{(z12|->z22)}</td> <td style="padding:10px">{(z12|->z22)}</td>
<td style="padding:10px">{(z11|->z21)}</td> <td style="padding:10px">{(z11|->z21)}</td>
</tr> </tr>
<tr> <tr>
<td style="padding:10px">(z10|->z22)</td> <td style="padding:10px">(z10|->z22)</td>
<td style="padding:10px">{(z12|->z22)}</td> <td style="padding:10px">{(z12|->z22)}</td>
<td style="padding:10px">{(z11|->z22)}</td> <td style="padding:10px">{(z11|->z22)}</td>
</tr> </tr>
<tr> <tr>
<td style="padding:10px">(z11|->z20)</td> <td style="padding:10px">(z11|->z20)</td>
<td style="padding:10px">{(z12|->z22)}</td> <td style="padding:10px">{(z12|->z22)}</td>
<td style="padding:10px">{(z11|->z21)}</td> <td style="padding:10px">{(z11|->z21)}</td>
</tr> </tr>
<tr> <tr>
<td style="padding:10px">(z11|->z21)</td> <td style="padding:10px">(z11|->z21)</td>
<td style="padding:10px">{(z12|->z22)}</td> <td style="padding:10px">{(z12|->z22)}</td>
<td style="padding:10px">{(z11|->z21)}</td> <td style="padding:10px">{(z11|->z21)}</td>
</tr> </tr>
<tr> <tr>
<td style="padding:10px">(z11|->z22)</td> <td style="padding:10px">(z11|->z22)</td>
<td style="padding:10px">{(z12|->z22)}</td> <td style="padding:10px">{(z12|->z22)}</td>
<td style="padding:10px">{(z11|->z22)}</td> <td style="padding:10px">{(z11|->z22)}</td>
</tr> </tr>
<tr> <tr>
<td style="padding:10px">(z12|->z20)</td> <td style="padding:10px">(z12|->z20)</td>
<td style="padding:10px">{(z12|->z22)}</td> <td style="padding:10px">{(z12|->z22)}</td>
<td style="padding:10px">{(z11|->z21)}</td> <td style="padding:10px">{(z11|->z21)}</td>
</tr> </tr>
<tr> <tr>
<td style="padding:10px">(z12|->z21)</td> <td style="padding:10px">(z12|->z21)</td>
<td style="padding:10px">{(z12|->z22)}</td> <td style="padding:10px">{(z12|->z22)}</td>
<td style="padding:10px">{(z11|->z21)}</td> <td style="padding:10px">{(z11|->z21)}</td>
</tr> </tr>
<tr> <tr>
<td style="padding:10px">(z12|->z22)</td> <td style="padding:10px">(z12|->z22)</td>
<td style="padding:10px">{(z12|->z22)}</td> <td style="padding:10px">{(z12|->z22)}</td>
<td style="padding:10px">{(z11|->z22)}</td> <td style="padding:10px">{(z11|->z22)}</td>
</tr> </tr>
</tbody></table> </tbody></table>
<Animation function visualisation> <Animation function visualisation>
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Indem man die Endzustände in der obigen Konstruktion so wählt, dass man in einem Zustand in $F_1$ und $F_2$ landet, kann man auch zeigen, dass der Schnitt zweier regulärer Sprachen regulär ist. Indem man die Endzustände in der obigen Konstruktion so wählt, dass man in einem Zustand in $F_1$ und $F_2$ landet, kann man auch zeigen, dass der Schnitt zweier regulärer Sprachen regulär ist.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
::load ::load
MACHINE NFA MACHINE NFA
SETS SETS
Z = {z10,z11, z12, z20,z21,z22} Z = {z10,z11, z12, z20,z21,z22}
CONSTANTS Σ, M, Z_gesamt, δ, S, F, f, CONSTANTS Σ, M, Z_gesamt, δ, S, F, f,
M1, Z1, δ1, S1, F1, M1, Z1, δ1, S1, F1,
M2, Z2, δ2, S2, F2 M2, Z2, δ2, S2, F2
PROPERTIES PROPERTIES
Σ = {0,1}∧ Σ = {0,1}∧
Z1 ∩ Z2 = ∅ ∧ Z1 ∩ Z2 = ∅ ∧
Z= Z1 ∪ Z2 Z= Z1 ∪ Z2
// Der Automat M1 (L(M1)={w| |w|=0 ∨ w=u0 mit u∈{0,1}*}): // Der Automat M1 (L(M1)={w| |w|=0 ∨ w=u0 mit u∈{0,1}*}):
M1 = (Σ, Z1, δ1, S1, F1) ∧ M1 = (Σ, Z1, δ1, S1, F1) ∧
Z1 ⊆ Z ∧ Z1 = {z10,z11,z12} ∧ Z1 ⊆ Z ∧ Z1 = {z10,z11,z12} ∧
F1 ⊆ Z1 ∧ S1 ⊆ Z1 ∧ F1 ⊆ Z1 ∧ S1 ⊆ Z1 ∧
δ1 ∈ (Z1×Σ) → ℙ(Z1) δ1 ∈ (Z1×Σ) → ℙ(Z1)
S1 = {z10} ∧ F1 = {z10, z12} ∧ S1 = {z10} ∧ F1 = {z10, z12} ∧
δ1 = { (z10,0)↦{z12}, (z10,1)↦{z11}, δ1 = { (z10,0)↦{z12}, (z10,1)↦{z11},
(z11,0)↦{z12}, (z11,1)↦{z11}, (z11,0)↦{z12}, (z11,1)↦{z11},
(z12,0)↦{z12}, (z12,1)↦{z11}} ∧ (z12,0)↦{z12}, (z12,1)↦{z11}} ∧
// Der Automat M2 (L(M2)={1^n|n∈ℕ_0}): // Der Automat M2 (L(M2)={1^n|n∈ℕ_0}):
M2 = (Σ, Z2, δ2, S2, F2) ∧ M2 = (Σ, Z2, δ2, S2, F2) ∧
Z2 ⊆ Z ∧ Z2 ⊆ Z ∧
δ2 ∈ (Z2×Σ) → ℙ(Z2) ∧ δ2 ∈ (Z2×Σ) → ℙ(Z2) ∧
S2 ⊆ Z2 ∧ F2 ⊆ Z2 S2 ⊆ Z2 ∧ F2 ⊆ Z2
Z2 = {z20,z21,z22} ∧ Z2 = {z20,z21,z22} ∧
S2 = {z20, z21} ∧ F2 = {z20, z21} ∧ S2 = {z20, z21} ∧ F2 = {z20, z21} ∧
δ2 = { (z20,0)↦{z22}, (z20,1)↦{z21}, δ2 = { (z20,0)↦{z22}, (z20,1)↦{z21},
(z21,0)↦{z22}, (z21,1)↦{z21}, (z21,0)↦{z22}, (z21,1)↦{z21},
(z22,0)↦{z22}, (z22,1)↦{z22}} ∧ (z22,0)↦{z22}, (z22,1)↦{z22}} ∧
//Konstruktion analog zu TODO Referenz auf Buch //Eigene Konstruktion analog zu "Grundkurs Theoretische Informatik" (s.o.)
M = (Σ, Z_gesamt, δ, S, F) ∧ M = (Σ, Z_gesamt, δ, S, F) ∧
Z_gesamt = Z1*Z2 ∧ Z_gesamt = Z1*Z2 ∧
S = S1*S2 ∧ S = S1*S2 ∧
F = F1*F2 ∧ F = F1*F2 ∧
δ = {x | x∈((Z*Z)*Σ)*ℙ(Z_gesamt) ∧ δ = {x | x∈((Z*Z)*Σ)*ℙ(Z_gesamt) ∧
∃zustand1,zustand2,symbol,menge.( ∃zustand1,zustand2,symbol,menge.(
x=((zustand1, zustand2), symbol)↦menge ∧ x=((zustand1, zustand2), symbol)↦menge ∧
zustand1∈Z1 ∧ zustand2∈Z2 ∧ symbol∈Σ ∧ zustand1∈Z1 ∧ zustand2∈Z2 ∧ symbol∈Σ ∧
menge = δ1(zustand1, symbol)*δ2(zustand2, symbol))} menge = δ1(zustand1, symbol)*δ2(zustand2, symbol))}
//Eine Hilfsfunktion zur Visualisierung //Eine Hilfsfunktion zur Visualisierung
∧ f ∈ seq(Z_gesamt) ∧ ran(f) = Z_gesamt ∧ f ∈ seq(Z_gesamt) ∧ ran(f) = Z_gesamt
DEFINITIONS // Für den Zustandsgraphen: DEFINITIONS // Für den Zustandsgraphen:
"LibraryStrings.def"; "LibraryStrings.def";
ANIMATION_FUNCTION1 == {r,c,i| r∈dom(f) ∧ c=0 ∧ i=f(r)}; 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_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_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)}; ANIMATION_FUNCTION4 == {r,c,i| r∈dom(f) ∧ c=2 ∧ i=δ(f(r), 1)};
END END
``` ```
%% Output %% Output
Loaded machine: NFA Loaded machine: NFA
%% 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() Machine constants set up using operation 0: $setup_constants()
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:init :init
``` ```
%% Output %% Output
Machine initialised using operation 1: $initialise_machine() Machine initialised using operation 1: $initialise_machine()
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:show :show
``` ```
%% Output %% Output
<table style="font-family:monospace"><tbody> <table style="font-family:monospace"><tbody>
<tr> <tr>
<td style="padding:10px">Zustand</td> <td style="padding:10px">Zustand</td>
<td style="padding:10px">δ(Zustand,0)</td> <td style="padding:10px">δ(Zustand,0)</td>
<td style="padding:10px">δ(Zustand,1)</td> <td style="padding:10px">δ(Zustand,1)</td>
</tr> </tr>
<tr> <tr>
<td style="padding:10px">(z10|->z20)</td> <td style="padding:10px">(z10|->z20)</td>
<td style="padding:10px">{(z12|->z22)}</td> <td style="padding:10px">{(z12|->z22)}</td>
<td style="padding:10px">{(z11|->z21)}</td> <td style="padding:10px">{(z11|->z21)}</td>
</tr> </tr>
<tr> <tr>
<td style="padding:10px">(z10|->z21)</td> <td style="padding:10px">(z10|->z21)</td>
<td style="padding:10px">{(z12|->z22)}</td> <td style="padding:10px">{(z12|->z22)}</td>
<td style="padding:10px">{(z11|->z21)}</td> <td style="padding:10px">{(z11|->z21)}</td>
</tr> </tr>
<tr> <tr>
<td style="padding:10px">(z10|->z22)</td> <td style="padding:10px">(z10|->z22)</td>
<td style="padding:10px">{(z12|->z22)}</td> <td style="padding:10px">{(z12|->z22)}</td>
<td style="padding:10px">{(z11|->z22)}</td> <td style="padding:10px">{(z11|->z22)}</td>
</tr> </tr>
<tr> <tr>
<td style="padding:10px">(z11|->z20)</td> <td style="padding:10px">(z11|->z20)</td>
<td style="padding:10px">{(z12|->z22)}</td> <td style="padding:10px">{(z12|->z22)}</td>
<td style="padding:10px">{(z11|->z21)}</td> <td style="padding:10px">{(z11|->z21)}</td>
</tr> </tr>
<tr> <tr>
<td style="padding:10px">(z11|->z21)</td> <td style="padding:10px">(z11|->z21)</td>
<td style="padding:10px">{(z12|->z22)}</td> <td style="padding:10px">{(z12|->z22)}</td>
<td style="padding:10px">{(z11|->z21)}</td> <td style="padding:10px">{(z11|->z21)}</td>
</tr> </tr>
<tr> <tr>
<td style="padding:10px">(z11|->z22)</td> <td style="padding:10px">(z11|->z22)</td>
<td style="padding:10px">{(z12|->z22)}</td> <td style="padding:10px">{(z12|->z22)}</td>
<td style="padding:10px">{(z11|->z22)}</td> <td style="padding:10px">{(z11|->z22)}</td>
</tr> </tr>
<tr> <tr>
<td style="padding:10px">(z12|->z20)</td> <td style="padding:10px">(z12|->z20)</td>
<td style="padding:10px">{(z12|->z22)}</td> <td style="padding:10px">{(z12|->z22)}</td>
<td style="padding:10px">{(z11|->z21)}</td> <td style="padding:10px">{(z11|->z21)}</td>
</tr> </tr>
<tr> <tr>
<td style="padding:10px">(z12|->z21)</td> <td style="padding:10px">(z12|->z21)</td>
<td style="padding:10px">{(z12|->z22)}</td> <td style="padding:10px">{(z12|->z22)}</td>
<td style="padding:10px">{(z11|->z21)}</td> <td style="padding:10px">{(z11|->z21)}</td>
</tr> </tr>
<tr> <tr>
<td style="padding:10px">(z12|->z22)</td> <td style="padding:10px">(z12|->z22)</td>
<td style="padding:10px">{(z12|->z22)}</td> <td style="padding:10px">{(z12|->z22)}</td>
<td style="padding:10px">{(z11|->z22)}</td> <td style="padding:10px">{(z11|->z22)}</td>
</tr> </tr>
</tbody></table> </tbody></table>
<Animation function visualisation> <Animation function visualisation>
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Zuletzt bleibt noch die Spiegelung einer Sprache. Um dies zu erreichen erstellen wir aus einem DFA einen NFA. Zuletzt bleibt noch die Spiegelung einer Sprache. Um dies zu erreichen erstellen wir aus einem DFA $M$ einen NFA $M_2$ (Vorgehen nach [Grundkurs Theoretische Informatik](https://link.springer.com/content/pdf/10.1007/978-3-8348-2202-4.pdf "Vossen, G., & Witt, K. U. (2016). Grundkurs Theoretische Informatik. Springer Fachmedien Wiesbaden."), Seite 101). $M_2$ hat als Startzustände die Endzustände von $M$ und als einzigen Endzustand den Startzustand von $M$. Die Übergänge von $M_2$ erhält man, indem man alle Übergange von $M$ umdreht. Dadurch ist der Automat ggf. auch nicht deterministisch.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
::load ::load
MACHINE DFA MACHINE DFA
SETS SETS
Z = {z0,z1,z2,z3} Z = {z0,z1,z2,z3}
CONSTANTS Σ, M, δ, δ2, F, M2, z_start CONSTANTS Σ, M, δ, δ2, F, M2, z_start
PROPERTIES PROPERTIES
Σ = {0,1} Σ = {0,1}
M = (Σ, Z, δ, z_start, F) ∧ M = (Σ, Z, δ, z_start, F) ∧
δ ∈ (Z×Σ) → Z ∧ δ ∈ (Z×Σ) → Z ∧
z_start ∈ Z ∧ z_start ∈ Z ∧
F ⊆ Z ∧ F ⊆ Z ∧
M2 = (Σ, Z, δ2, F, {z_start}) ∧ M2 = (Σ, Z, δ2, F, {z_start}) ∧
δ2 ∈ (Z×Σ) <-> ℙ(Z) ∧ δ2 ∈ (Z×Σ) <-> ℙ(Z) ∧
δ2 = {x |∃a,s,s2.(x=((s2, a)↦{s}) ∧ a∈Σ ∧ s∈Z ∧ s2∈Z ∧ δ(s,a) = s2)} δ2 = {x |∃a,s,s2.(x=((s2, a)↦{s}) ∧ a∈Σ ∧ s∈Z ∧ s2∈Z ∧ δ(s,a) = s2)}
DEFINITIONS // Für den Zustandsgraphen: DEFINITIONS // Für den Zustandsgraphen:
CUSTOM_GRAPH_NODES1 == rec(shape:"doublecircle",nodes:{z_start}); // Endzustände 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_NODES2 == rec(shape:"circle",nodes:Z\{z_start}); // andere Zustände
CUSTOM_GRAPH_NODES3 == rec(shape:"none",color:"white",style:"none",nodes:{""}); 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_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_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_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 CUSTOM_GRAPH_EDGES4 == rec(color:"black",label:"",edges:{""}*F) // Kanten für Startknoten
END END
``` ```
%% Output %% Output
Loaded machine: DFA Loaded machine: DFA
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:constants M=({0,1}, //Σ :constants M=({0,1}, //Σ
{z0,z1,z2,z3}, //Z {z0,z1,z2,z3}, //Z
{(z0,0)↦z1, (z0,1)↦z3, {(z0,0)↦z1, (z0,1)↦z3,
(z1,0)↦z3, (z1,1)↦z2, (z1,0)↦z3, (z1,1)↦z2,
(z2,0)↦z2, (z2,1)↦z2, (z2,0)↦z2, (z2,1)↦z2,
(z3,0)↦z3, (z3,1)↦z3 }, //δ (z3,0)↦z3, (z3,1)↦z3 }, //δ
z0, {z0, z2}) //z0, F z0, {z0, z2}) //z0, F
``` ```
%% Output %% Output
Machine constants set up using operation 0: $setup_constants() Machine constants set up using operation 0: $setup_constants()
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:dot custom_graph :dot custom_graph
``` ```
%% Output %% Output
<Dot visualization: custom_graph []> <Dot visualization: custom_graph []>
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment