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

Notebook zu Myhill Nerode verschoben und leicht angepasst.

parent 248614df
No related branches found
No related tags found
1 merge request!1Master
Show whitespace changes
Inline Side-by-side
info4/kapitel-2/Minimalautomat.ipynb
+ 1
− 1
View file @ ead07adb
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
## Algorithmus Minimalautomat ## Algorithmus Minimalautomat
Dieses Notebook begleitet die Vorlesung zur Myhill-Nerode Äquivalenzrelation und dem Minimalautomaten. Dieses Notebook begleitet die Vorlesung zu dem Minimalautomaten.
Hier ist der Beispiel DFA aus den Folien zur Illustration der Konstruktion des Minimalautomaten. Hier ist der Beispiel DFA aus den Folien zur Illustration der Konstruktion des Minimalautomaten.
%% 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,z4} Z = {z0,z1,z2,z3,z4}
ABSTRACT_CONSTANTS δs, L ABSTRACT_CONSTANTS δs, L
CONSTANTS Σ, F, δ CONSTANTS Σ, F, δ
PROPERTIES PROPERTIES
F ⊆ Z ∧ δ ∈ (Z×Σ) → Z ∧ F ⊆ Z ∧ δ ∈ (Z×Σ) → Z ∧
/* Definition der erweiterten Überführungsfunktion */ /* Definition der erweiterten Überführungsfunktion */
δs ∈ (Z×seq(Σ)) → Z ∧ δs ∈ (Z×seq(Σ)) → Z ∧
δs = λ(z,s).(z∈Z ∧ s∈seq(Σ) | δs = λ(z,s).(z∈Z ∧ s∈seq(Σ) |
IF s=[] THEN z IF s=[] THEN z
ELSE δs(δ(z,first(s)),tail(s)) END) ELSE δs(δ(z,first(s)),tail(s)) END)
∧ ∧
/* Die vom Automaten akzeptierte Sprache L */ /* Die vom Automaten akzeptierte Sprache L */
L = {ω|ω∈seq(Σ) ∧ δs(z0,ω) ∈ F} L = {ω|ω∈seq(Σ) ∧ δs(z0,ω) ∈ F}
∧ ∧
/* Der Automat von Folie 10: */ /* Der Automat von Folie 10: */
Σ = {0,1} ∧ Σ = {0,1} ∧
F = {z3,z4} ∧ F = {z3,z4} ∧
δ = { (z0,0)↦z1, (z0,1)↦z2, δ = { (z0,0)↦z1, (z0,1)↦z2,
(z1,0)↦z3, (z1,1)↦z3, (z1,0)↦z3, (z1,1)↦z3,
(z2,0)↦z4, (z2,1)↦z4, (z2,0)↦z4, (z2,1)↦z4,
(z3,0)↦z3, (z3,1)↦z3, (z3,0)↦z3, (z3,1)↦z3,
(z4,0)↦z4, (z4,1)↦z4 } (z4,0)↦z4, (z4,1)↦z4 }
DEFINITIONS DEFINITIONS
//SET_PREF_DOT_HORIZONTAL_LAYOUT==TRUE; //SET_PREF_DOT_HORIZONTAL_LAYOUT==TRUE;
//SET_PREF_DOT_LIMIT_PAGE_SIZE==FALSE; //SET_PREF_DOT_LIMIT_PAGE_SIZE==FALSE;
CUSTOM_GRAPH_NODES1 == rec(shape:"doublecircle",nodes:F); CUSTOM_GRAPH_NODES1 == rec(shape:"doublecircle",nodes:F);
CUSTOM_GRAPH_NODES2 == rec(shape:"circle",nodes:Z\F); CUSTOM_GRAPH_NODES2 == rec(shape:"circle",nodes:Z\F);
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:{"" |-> z0}) CUSTOM_GRAPH_EDGES3 == rec(color:"black",label:"",edges:{"" |-> z0})
END END
``` ```
%% Output %% Output
Loaded machine: DFA Loaded machine: DFA
%% 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:
Der Automat sieht grafisch so aus: Der Automat sieht grafisch so aus:
%% 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:
In der folgenden B Maschine sind (bis auf die Entfernung der nicht erreichbaren Zustände) die Schritte des Algorithmus umgesetzt worden. In der folgenden B Maschine sind (bis auf die Entfernung der nicht erreichbaren Zustände) die Schritte des Algorithmus umgesetzt worden.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
::load ::load
MACHINE MinimalDFA MACHINE MinimalDFA
SETS SETS
Z = {z0,z1,z2,z3,z4} Z = {z0,z1,z2,z3,z4}
CONSTANTS Σ, F, δ CONSTANTS Σ, F, δ
PROPERTIES PROPERTIES
F ⊆ Z ∧ δ ∈ (Z×Σ) → Z ∧ F ⊆ Z ∧ δ ∈ (Z×Σ) → Z ∧
/* Der Automat von den Folien: */ /* Der Automat von den Folien: */
Σ = {0,1} ∧ Σ = {0,1} ∧
F = {z3,z4} ∧ F = {z3,z4} ∧
δ = { (z0,0)↦z1, (z0,1)↦z2, δ = { (z0,0)↦z1, (z0,1)↦z2,
(z1,0)↦z3, (z1,1)↦z3, (z1,0)↦z3, (z1,1)↦z3,
(z2,0)↦z4, (z2,1)↦z4, (z2,0)↦z4, (z2,1)↦z4,
(z3,0)↦z3, (z3,1)↦z3, (z3,0)↦z3, (z3,1)↦z3,
(z4,0)↦z4, (z4,1)↦z4 } (z4,0)↦z4, (z4,1)↦z4 }
VARIABLES VARIABLES
markiert, fusioniert markiert, fusioniert
INVARIANT markiert : Z <-> Z & INVARIANT markiert : Z <-> Z &
fusioniert : Z <-> Z fusioniert : Z <-> Z
INITIALISATION markiert := {za,zb| za∈F ⇔ zb∉F} || fusioniert := {} INITIALISATION markiert := {za,zb| za∈F ⇔ zb∉F} || fusioniert := {}
OPERATIONS OPERATIONS
Markiere(za,zb,a) = SELECT (za,zb) ∉ markiert ∧ Markiere(za,zb,a) = SELECT (za,zb) ∉ markiert ∧
a∈Σ ∧ a∈Σ ∧
(δ(za,a),δ(zb,a)) ∈ markiert THEN (δ(za,a),δ(zb,a)) ∈ markiert THEN
markiert := markiert \/ {(za,zb),(zb,za)} markiert := markiert \/ {(za,zb),(zb,za)}
END; END;
Fertig = SELECT fusioniert={} ∧ Fertig = SELECT fusioniert={} ∧
!(za,zb,a).((za,zb) ∉ markiert ∧ a∈Σ !(za,zb,a).((za,zb) ∉ markiert ∧ a∈Σ
=> =>
(δ(za,a),δ(zb,a)) ∉ markiert) THEN (δ(za,a),δ(zb,a)) ∉ markiert) THEN
fusioniert := {za,zb|(za,zb) ∉ markiert ∧ za ≠ zb} || fusioniert := {za,zb|(za,zb) ∉ markiert ∧ za ≠ zb} ||
markiert := {} markiert := {}
END END
DEFINITIONS DEFINITIONS
//SET_PREF_DOT_HORIZONTAL_LAYOUT==TRUE; //SET_PREF_DOT_HORIZONTAL_LAYOUT==TRUE;
//SET_PREF_DOT_LIMIT_PAGE_SIZE==FALSE; //SET_PREF_DOT_LIMIT_PAGE_SIZE==FALSE;
CUSTOM_GRAPH_NODES1 == rec(shape:"doublecircle",nodes:F); CUSTOM_GRAPH_NODES1 == rec(shape:"doublecircle",nodes:F);
CUSTOM_GRAPH_NODES2 == rec(shape:"circle",nodes:Z\F); CUSTOM_GRAPH_NODES2 == rec(shape:"circle",nodes:Z\F);
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:{"" |-> z0}); CUSTOM_GRAPH_EDGES3 == rec(color:"black",label:"",edges:{"" |-> z0});
CUSTOM_GRAPH_EDGES4 == rec(color:"gray",label:"×",style:"dotted",edges:markiert); CUSTOM_GRAPH_EDGES4 == rec(color:"gray",label:"×",style:"dotted",edges:markiert);
CUSTOM_GRAPH_EDGES5 == rec(color:"purple",label:"↔",style:"bold",edges:fusioniert) CUSTOM_GRAPH_EDGES5 == rec(color:"purple",label:"↔",style:"bold",edges:fusioniert)
END END
``` ```
%% Output %% Output
Loaded machine: MinimalDFA Loaded machine: MinimalDFA
%% 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:markdown id: tags: %% Cell type:markdown id: tags:
Markiere alle Paare $\{z, z'\}$ mit Markiere alle Paare $\{z, z'\}$ mit
* $z \in F \Longleftrightarrow z' \not\in F$. * $z \in F \Longleftrightarrow z' \not\in F$.
Dies wird in der B Maschine in der INITIALISATION Klausel gemacht. Im Graphen unten sind die markierten Paare mit $\times$ gekennzeichnet. Dies wird in der B Maschine in der INITIALISATION Klausel gemacht. Im Graphen unten sind die markierten Paare mit $\times$ gekennzeichnet.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:pref DOT_ENGINE=circo :pref DOT_ENGINE=circo
``` ```
%% Output %% Output
Preference changed: DOT_ENGINE = circo Preference changed: DOT_ENGINE = circo
%% 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:
Sei $\{z, z'\}$ ein unmarkiertes Paar. Prüfe für jedes Sei $\{z, z'\}$ ein unmarkiertes Paar. Prüfe für jedes
$a \in \Sigma$, ob $\{\delta(z,a), \delta(z',a)\}$ bereits markiert $a \in \Sigma$, ob $\{\delta(z,a), \delta(z',a)\}$ bereits markiert
ist. Ist mindestens ein Test erfolgreich, so markiere auch ist. Ist mindestens ein Test erfolgreich, so markiere auch
$\{z,z'\}$. $\{z,z'\}$.
Dies ist hier der Fall: Dies ist hier der Fall:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:exec Markiere :exec Markiere
``` ```
%% Output %% Output
Executed operation: Markiere(z1,z0,0) Executed operation: Markiere(z1,z0,0)
%% 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:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:exec Markiere :exec Markiere
``` ```
%% Output %% Output
Executed operation: Markiere(z2,z0,0) Executed operation: Markiere(z2,z0,0)
%% 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:
Es kann jetzt kein Markieren mehr ausgeführt werden, man kann nun Zustände fusionieren. Die Fusion selber ist hier nur grafisch angedeutet, nicht ausgeführt. Es kann jetzt kein Markieren mehr ausgeführt werden, man kann nun Zustände fusionieren. Die Fusion selber ist hier nur grafisch angedeutet, nicht ausgeführt.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:exec Fertig :exec Fertig
``` ```
%% Output %% Output
Executed operation: Fertig() Executed operation: Fertig()
%% 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:
Anmerkung: wenn man oben zum Beispiel $F = \{z2\}$ setzt kommt ein anderes Ergebnis heraus. Anmerkung: wenn man oben zum Beispiel $F = \{z2\}$ setzt kommt ein anderes Ergebnis heraus.
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Das sind die Zustände die fusioniert werden können: Das sind die Zustände die fusioniert werden können:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
fusioniert fusioniert
``` ```
%% Output %% Output
$\{(\mathit{z1}\mapsto \mathit{z2}),(\mathit{z2}\mapsto \mathit{z1}),(\mathit{z3}\mapsto \mathit{z4}),(\mathit{z4}\mapsto \mathit{z3})\}$ $\{(\mathit{z1}\mapsto \mathit{z2}),(\mathit{z2}\mapsto \mathit{z1}),(\mathit{z3}\mapsto \mathit{z4}),(\mathit{z4}\mapsto \mathit{z3})\}$
{(z1↦z2),(z2↦z1),(z3↦z4),(z4↦z3)} {(z1↦z2),(z2↦z1),(z3↦z4),(z4↦z3)}
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Wir berechnen jetzt die neue Menge ```ZF``` an fusionierten Zuständen (mit der reflexiven und transitiven Hülle ```closure``` von ```fusioniert```): Wir berechnen jetzt die neue Menge ```ZF``` an fusionierten Zuständen (mit der reflexiven und transitiven Hülle ```closure``` von ```fusioniert```):
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:let ZF {zs| #x.(x:Z & closure(fusioniert)[{x}] = zs)} :let ZF {zs| #x.(x:Z & closure(fusioniert)[{x}] = zs)}
``` ```
%% Output %% Output
$\{\{\mathit{z0}\},\{\mathit{z1},\mathit{z2}\},\{\mathit{z3},\mathit{z4}\}\}$ $\{\{\mathit{z0}\},\{\mathit{z1},\mathit{z2}\},\{\mathit{z3},\mathit{z4}\}\}$
{{z0},{z1,z2},{z3,z4}} {{z0},{z1,z2},{z3,z4}}
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Man kann jetzt die Übergangsfunktion für ZF so ausrechnen: Man kann jetzt die Übergangsfunktion für ZF so ausrechnen:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:let δF %(zfa,a).(zfa:ZF & a:Σ | closure(fusioniert)[UNION(za).(za:zfa|{δ(za,a)})]) :let δF %(zfa,a).(zfa:ZF & a:Σ | closure(fusioniert)[UNION(za).(za:zfa|{δ(za,a)})])
``` ```
%% Output %% Output
$\{(\{\mathit{z0}\}\mapsto 0\mapsto\{\mathit{z1},\mathit{z2}\}),(\{\mathit{z0}\}\mapsto 1\mapsto\{\mathit{z1},\mathit{z2}\}),(\{\mathit{z1},\mathit{z2}\}\mapsto 0\mapsto\{\mathit{z3},\mathit{z4}\}),(\{\mathit{z1},\mathit{z2}\}\mapsto 1\mapsto\{\mathit{z3},\mathit{z4}\}),(\{\mathit{z3},\mathit{z4}\}\mapsto 0\mapsto\{\mathit{z3},\mathit{z4}\}),(\{\mathit{z3},\mathit{z4}\}\mapsto 1\mapsto\{\mathit{z3},\mathit{z4}\})\}$ $\{(\{\mathit{z0}\}\mapsto 0\mapsto\{\mathit{z1},\mathit{z2}\}),(\{\mathit{z0}\}\mapsto 1\mapsto\{\mathit{z1},\mathit{z2}\}),(\{\mathit{z1},\mathit{z2}\}\mapsto 0\mapsto\{\mathit{z3},\mathit{z4}\}),(\{\mathit{z1},\mathit{z2}\}\mapsto 1\mapsto\{\mathit{z3},\mathit{z4}\}),(\{\mathit{z3},\mathit{z4}\}\mapsto 0\mapsto\{\mathit{z3},\mathit{z4}\}),(\{\mathit{z3},\mathit{z4}\}\mapsto 1\mapsto\{\mathit{z3},\mathit{z4}\})\}$
{({z0}↦0↦{z1,z2}),({z0}↦1↦{z1,z2}),({z1,z2}↦0↦{z3,z4}),({z1,z2}↦1↦{z3,z4}),({z3,z4}↦0↦{z3,z4}),({z3,z4}↦1↦{z3,z4})} {({z0}↦0↦{z1,z2}),({z0}↦1↦{z1,z2}),({z1,z2}↦0↦{z3,z4}),({z1,z2}↦1↦{z3,z4}),({z3,z4}↦0↦{z3,z4}),({z3,z4}↦1↦{z3,z4})}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:pref DOT_DECOMPOSE_NODES=FALSE DOT_ENGINE=dot :pref DOT_DECOMPOSE_NODES=FALSE DOT_ENGINE=dot
``` ```
%% Output %% Output
Preference changed: DOT_DECOMPOSE_NODES = FALSE Preference changed: DOT_DECOMPOSE_NODES = FALSE
Preference changed: DOT_ENGINE = dot Preference changed: DOT_ENGINE = dot
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:dot expr_as_graph ("0",{a,b|a:ZF & b=δF(a,0)}, "1",{a,b|a:ZF & b=δF(a,1)}) :dot expr_as_graph ("0",{a,b|a:ZF & b=δF(a,0)}, "1",{a,b|a:ZF & b=δF(a,1)})
``` ```
%% Output %% Output
<Dot visualization: expr_as_graph [δFZFδF={(({z0},0),{z1,z2}),(({z0},1),{z1,z2}),(({z1,z2},0),{z3,z4}),(({z1,z2},1),{z3,z4}),(({z3,z4},0),{z3,z4}),(({z3,z4},1),{z3,z4})} & ZF={{z0},{z1,z2},{z3,z4}}("0",{a,b|a:ZF & b=δF(a, 0)})]> <Dot visualization: expr_as_graph [δFZFδF={(({z0},0),{z1,z2}),(({z0},1),{z1,z2}),(({z1,z2},0),{z3,z4}),(({z1,z2},1),{z3,z4}),(({z3,z4},0),{z3,z4}),(({z3,z4},1),{z3,z4})} & ZF={{z0},{z1,z2},{z3,z4}}("0",{a,b|a:ZF & b=δF(a, 0)})]>
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:table δF :table δF
``` ```
%% Output %% Output
|prj11|prj12|prj2| |prj11|prj12|prj2|
|---|---|---| |---|---|---|
|$\{\mathit{z0}\}$|$0$|$\{\mathit{z1},\mathit{z2}\}$| |$\{\mathit{z0}\}$|$0$|$\{\mathit{z1},\mathit{z2}\}$|
|$\{\mathit{z0}\}$|$1$|$\{\mathit{z1},\mathit{z2}\}$| |$\{\mathit{z0}\}$|$1$|$\{\mathit{z1},\mathit{z2}\}$|
|$\{\mathit{z1},\mathit{z2}\}$|$0$|$\{\mathit{z3},\mathit{z4}\}$| |$\{\mathit{z1},\mathit{z2}\}$|$0$|$\{\mathit{z3},\mathit{z4}\}$|
|$\{\mathit{z1},\mathit{z2}\}$|$1$|$\{\mathit{z3},\mathit{z4}\}$| |$\{\mathit{z1},\mathit{z2}\}$|$1$|$\{\mathit{z3},\mathit{z4}\}$|
|$\{\mathit{z3},\mathit{z4}\}$|$0$|$\{\mathit{z3},\mathit{z4}\}$| |$\{\mathit{z3},\mathit{z4}\}$|$0$|$\{\mathit{z3},\mathit{z4}\}$|
|$\{\mathit{z3},\mathit{z4}\}$|$1$|$\{\mathit{z3},\mathit{z4}\}$| |$\{\mathit{z3},\mathit{z4}\}$|$1$|$\{\mathit{z3},\mathit{z4}\}$|
prj11 prj12 prj2 prj11 prj12 prj2
{z0} 0 {z1,z2} {z0} 0 {z1,z2}
{z0} 1 {z1,z2} {z0} 1 {z1,z2}
{z1,z2} 0 {z3,z4} {z1,z2} 0 {z3,z4}
{z1,z2} 1 {z3,z4} {z1,z2} 1 {z3,z4}
{z3,z4} 0 {z3,z4} {z3,z4} 0 {z3,z4}
{z3,z4} 1 {z3,z4} {z3,z4} 1 {z3,z4}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
``` ```
......
info4/kapitel-2/Der Satz von Myhill und Nerode.ipynb → info4/kapitel-2/Myhill_Nerode.ipynb
+ 10
− 2
View file @ ead07adb
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
# Der Satz von Myhill und Nerode # Der Satz von Myhill und Nerode
Wir betrachten die Myhill-Nerode-Äquivalenzrelation anhand der Sprache L = {a, b, aa, bb, aac, bbc, ccc}. Wir betrachten die Myhill-Nerode-Äquivalenzrelation anhand der Sprache L = {a, b, aa, bb, aac, bbc, ccc}.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
MACHINE EquivalenceRelation MACHINE EquivalenceRelation
/* Ein Modell der Myhill-Nerode Äquivalenzrelation R_L, /* Ein Modell der Myhill-Nerode Äquivalenzrelation R_L,
der entsprechenden Äquivalenzklassen und dem Index der Sprache.*/ der entsprechenden Äquivalenzklassen und dem Index der Sprache.*/
SETS SETS
Alphabet = {a,b,c} Alphabet = {a,b,c}
CONSTANTS L, RL, maxsize, All, Classes, index CONSTANTS L, RL, maxsize, All, Classes, index
DEFINITIONS DEFINITIONS
class(x) == {y | x↦y : RL} ; class(x) == {y | x↦y : RL} ;
ANIMATION_FUNCTION1 == {r,c,i |r=1 ∧ c∈ dom(word) ∧ i=word(c)}; ANIMATION_FUNCTION1 == {r,c,i |r=1 ∧ c∈ dom(word) ∧ i=word(c)};
ANIMATION_FUNCTION2 == {r,c,i |r=2 ∧ c=1 ∧ i=z}; ANIMATION_FUNCTION2 == {r,c,i |r=2 ∧ c=1 ∧ i=z};
ANIMATION_FUNCTION3 == {(1, 0, "Wort:"), (2, 0, "Äquivalenzklasse:")}; ANIMATION_FUNCTION3 == {(1, 0, "Wort:"), (2, 0, "Äquivalenzklasse:")};
PROPERTIES PROPERTIES
L ⊆ seq(Alphabet) ∧ L ⊆ seq(Alphabet) ∧
// All = {z | z∈seq(Alphabet) ∧ size(z)<=maxsz} & /* beschränkt auf endliche Folgen */ // All = {z | z∈seq(Alphabet) ∧ size(z)<=maxsz} & /* beschränkt auf endliche Folgen */
All = UNION(ii).(ii:0..maxsize| (1..ii) --> Alphabet) ∧ All = UNION(ii).(ii:0..maxsize| (1..ii) --> Alphabet) ∧
RL = ({x,y| x∈All ∧ y∈All ∧ ∀z.(z∈All ⇒ ( x^z ∈ L ⇔ y^z ∈ L))}) ∧ RL = ({x,y| x∈All ∧ y∈All ∧ ∀z.(z∈All ⇒ ( x^z ∈ L ⇔ y^z ∈ L))}) ∧
L = {[a],[b],[a,a],[b,b],[a,a,c],[b,b,c],[c,c,c]} ∧ maxsize = 3 ∧ L = {[a],[b],[a,a],[b,b],[a,a,c],[b,b,c],[c,c,c]} ∧ maxsize = 3 ∧
Classes = ran( %x.(x∈All|class(x))) ∧ /* Menge der Äquivalenzklassen {class(x)|x∈All} */ Classes = ran( %x.(x∈All|class(x))) ∧ /* Menge der Äquivalenzklassen {class(x)|x∈All} */
index = card( Classes ) index = card( Classes )
ASSERTIONS ASSERTIONS
/* Test ob wir eine Äquivalenzrelation haben: */ /* Test ob wir eine Äquivalenzrelation haben: */
∀x.(x∈All ⇒ x↦x ∈ RL); /* Reflexivität */ ∀x.(x∈All ⇒ x↦x ∈ RL); /* Reflexivität */
∀(x,y).(x↦y ∈ RL ⇒ y↦x ∈ RL); /* Symetrie */ ∀(x,y).(x↦y ∈ RL ⇒ y↦x ∈ RL); /* Symetrie */
∀(x,y,z).(x↦y ∈ RL ∧ y↦z ∈ RL ⇒ x↦z ∈ RL); /* Transitivität */ ∀(x,y,z).(x↦y ∈ RL ∧ y↦z ∈ RL ⇒ x↦z ∈ RL); /* Transitivität */
/* Einige Beispiele : */ /* Einige Beispiele : */
[a,a] ↦ [b,b] ∈ RL; [a,a] ↦ [b,b] ∈ RL;
[a,a] ↦ [c,c] ∉ RL; [a,a] ↦ [c,c] ∉ RL;
[b,b,c] ↦ [c,c,c] ∈ RL; [b,b,c] ↦ [c,c,c] ∈ RL;
class([a,a]) = {[a,a],[b,b]}; class([a,a]) = {[a,a],[b,b]};
class([c,c,c]) = {[a,a,c],[b,b,c],[c,c,c]} class([c,c,c]) = {[a,a,c],[b,b,c],[c,c,c]}
/* Der durch die Äquivalenzklassen induzierte DFA: */ /* Der durch die Äquivalenzklassen induzierte DFA: */
VARIABLES z, word VARIABLES z, word
INVARIANT z ⊆ All ∧ word ∈ seq(Alphabet) INVARIANT z ⊆ All ∧ word ∈ seq(Alphabet)
INITIALISATION z := class([]); word := [] INITIALISATION z := class([]); word := []
OPERATIONS OPERATIONS
Delta(terminal) = PRE terminal∈Alphabet THEN Delta(terminal) = PRE terminal∈Alphabet THEN
ANY x WHERE x∈z ∧ ∀x2.(x2∈z ⇒ size(x2)≥size(x)) THEN ANY x WHERE x∈z ∧ ∀x2.(x2∈z ⇒ size(x2)≥size(x)) THEN
z := class(x^[terminal]); z := class(x^[terminal]);
word := word^[terminal] word := word^[terminal]
END END
END; END;
Final = SELECT z ∩ L ≠ {} THEN skip END Final = SELECT z ∩ L ≠ {} THEN skip END
END END
``` ```
%% Output %% Output
Loaded machine: EquivalenceRelation Loaded machine: EquivalenceRelation
%% 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
index index
``` ```
%% Output %% Output
$8$ $8$
8 8
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Da der $Index(L)=8<\infty$ ist die gegebene Sprache regulär. Da der $Index(L)=8<\infty$ ist die gegebene Sprache regulär.
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Durch die Äquivalenzklassen wird ein Minimalautomat induziert. Durch die Äquivalenzklassen wird ein Minimalautomat induziert.
Die Menge der Zustände ist gleich der Menge der Äquivalenzklassen. Die Menge der Zustände ist gleich der Menge der Äquivalenzklassen.
Und nach dem Einlesen eines Wortes $w∈Σ^*$ landet man in dem Zustand, der der Äquivalenzklasse von $w$ bezüglich $R_L$ entspricht. Und nach dem Einlesen eines Wortes $w∈Σ^*$ landet man in dem Zustand, der der Äquivalenzklasse von $w$ bezüglich $R_L$ entspricht.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:browse :browse
``` ```
%% Output %% Output
Machine: EquivalenceRelation Machine: EquivalenceRelation
Sets: Alphabet Sets: Alphabet
Constants: L, RL, maxsize, All, Classes, index Constants: L, RL, maxsize, All, Classes, index
Variables: z, word Variables: z, word
Operations: Operations:
Delta(a) Delta(a)
Delta(b) Delta(b)
Delta(c) Delta(c)
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:exec Delta terminal=a :exec Delta terminal=a
``` ```
%% Output %% Output
Executed operation: Delta(a) Executed operation: Delta(a)
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:exec Delta terminal=a :exec Delta terminal=a
``` ```
%% Output %% Output
Executed operation: Delta(a) Executed operation: Delta(a)
%% 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">Wort:</td> <td style="padding:10px">Wort:</td>
<td style="padding:10px">a</td> <td style="padding:10px">a</td>
<td style="padding:10px">a</td> <td style="padding:10px">a</td>
</tr> </tr>
<tr> <tr>
<td style="padding:10px">Äquivalenzklasse:</td> <td style="padding:10px">Äquivalenzklasse:</td>
<td style="padding:10px">{{(1|->a),(2|->a)},{(1|->b),(2|->b)}}</td> <td style="padding:10px">{{(1|->a),(2|->a)},{(1|->b),(2|->b)}}</td>
<td style="padding:0px"></td> <td style="padding:0px"></td>
</tr> </tr>
</tbody></table> </tbody></table>
<Animation function visualisation> <Animation function visualisation>
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Ein weiteres Beispiel ist die Sprache L={a^n | n>=0}. Ein weiteres Beispiel ist die Sprache $L=\{a^n | n\geq0\}$.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
MACHINE EquivalenceRelation2 MACHINE EquivalenceRelation2
SETS SETS
Alphabet = {a,b,c} Alphabet = {a,b,c}
CONSTANTS L, RL, maxsize, All, Classes, index CONSTANTS L, RL, maxsize, All, Classes, index
DEFINITIONS DEFINITIONS
class(x) == {y | x↦y : RL} ; class(x) == {y | x↦y : RL} ;
PROPERTIES PROPERTIES
L ⊆ seq(Alphabet) ∧ L ⊆ seq(Alphabet) ∧
// All = {z | z∈seq(Alphabet) ∧ size(z)≤maxsize} & /* Beschränkt auf endliche Folgen */ // All = {z | z∈seq(Alphabet) ∧ size(z)≤maxsize} & /* Beschränkt auf endliche Folgen */
All = UNION(ii).(ii:0..maxsize| (1..ii) --> Alphabet) ∧ All = UNION(ii).(ii:0..maxsize| (1..ii) --> Alphabet) ∧
RL = ({x,y| x∈All ∧ y∈All ∧ ∀z.(z∈All ⇒ ( x^z ∈ L ⇔ y^z ∈ L))}) ∧ RL = ({x,y| x∈All ∧ y∈All ∧ ∀z.(z∈All ⇒ ( x^z ∈ L ⇔ y^z ∈ L))}) ∧
/*L = {x | x=a^n ∧ size(x)≤maxsize} Beschränkt auf endliche Folgen*/ /*L = {x | x=a^n ∧ size(x)≤maxsize} Beschränkt auf endliche Folgen*/
L = UNION(ii).(ii:0..maxsize| (1..ii) --> {a}) ∧ maxsize = 3 ∧ L = UNION(ii).(ii:0..maxsize| (1..ii) --> {a}) ∧ maxsize = 3 ∧
Classes = ran( %x.(x∈All|class(x))) ∧ /* Menge der Äquivalenzklassen {class(x)|x∈All} */ Classes = ran( %x.(x∈All|class(x))) ∧ /* Menge der Äquivalenzklassen {class(x)|x∈All} */
index = card( Classes ) index = card( Classes )
END END
``` ```
%% Output %% Output
Loaded machine: EquivalenceRelation2 Loaded machine: EquivalenceRelation2
%% 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
index index
``` ```
%% Output %% Output
$5$ $5$
5 5
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Auch diese Sprache ist offensichtlich regulär. Auch diese Sprache ist offensichtlich regulär.
Hier könnte man davon ausgehen, dass dies aus der Beschränkung auf endliche Folgen folgt. Hier könnte man davon ausgehen, dass dies aus der Beschränkung auf endliche Folgen folgt.
Denn je länger man die zugelassenen Folgen macht, desdo mehr Äquivalenzklassen gibt es. Denn je länger man die zugelassenen Folgen macht, desdo mehr Äquivalenzklassen gibt es.
Es gibt eine Äquivalenzklasse für jedes $a^m$ mit $0≤m≤n$ und eine für Wörter, die nicht in der Sprache liegen, also insgesamt $n+2$. Es gibt eine Äquivalenzklasse für jedes $a^m$ mit $0≤m≤n$ und eine für Wörter, die nicht in der Sprache liegen, also insgesamt $n+2$.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
L L
``` ```
%% Output %% Output
$\renewcommand{\emptyset}{\mathord\varnothing}\{\emptyset,\{(1\mapsto \mathit{a})\},\{(1\mapsto \mathit{a}),(2\mapsto \mathit{a})\},\{(1\mapsto \mathit{a}),(2\mapsto \mathit{a}),(3\mapsto \mathit{a})\}\}$ $\renewcommand{\emptyset}{\mathord\varnothing}\{\emptyset,\{(1\mapsto \mathit{a})\},\{(1\mapsto \mathit{a}),(2\mapsto \mathit{a})\},\{(1\mapsto \mathit{a}),(2\mapsto \mathit{a}),(3\mapsto \mathit{a})\}\}$
{∅,{(1↦a)},{(1↦a),(2↦a)},{(1↦a),(2↦a),(3↦a)}} {∅,{(1↦a)},{(1↦a),(2↦a)},{(1↦a),(2↦a),(3↦a)}}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
x=[a] ∧ y=[a, a] ∧ ∃z.(z∈All ∧ not(x^z ∈ L ⇔ y^z ∈ L)) /*Gegenbeispiel für [a] ↦ [a,a] ∈ R_L*/ x=[a] ∧ y=[a, a] ∧ ∃z.(z∈All ∧ not(x^z ∈ L ⇔ y^z ∈ L)) /*Gegenbeispiel für [a] ↦ [a,a] ∈ R_L*/
``` ```
%% Output %% Output
$\mathit{TRUE}$ $\mathit{TRUE}$
**Solution:** **Solution:**
* $\mathit{x} = \{(1\mapsto \mathit{a})\}$ * $\mathit{x} = \{(1\mapsto \mathit{a})\}$
* $\mathit{y} = \{(1\mapsto \mathit{a}),(2\mapsto \mathit{a})\}$ * $\mathit{y} = \{(1\mapsto \mathit{a}),(2\mapsto \mathit{a})\}$
* $\mathit{z} = \{(1\mapsto \mathit{a}),(2\mapsto \mathit{a})\}$ * $\mathit{z} = \{(1\mapsto \mathit{a}),(2\mapsto \mathit{a})\}$
TRUE TRUE
Solution: Solution:
x = {(1↦a)} x = {(1↦a)}
y = {(1↦a),(2↦a)} y = {(1↦a),(2↦a)}
z = {(1↦a),(2↦a)} z = {(1↦a),(2↦a)}
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Betrachtet man allerdings den unendlichen Fall, so fallen die Wörter $a^m$ alle in eine Klasse. Betrachtet man allerdings den unendlichen Fall, so fallen die Wörter $a^m$ alle in eine Klasse.
Dies gilt, da es kein "Ende" der Folgen mehr gibt und somit kein Gegenbeispiel wie oben. Dies gilt, da es kein "Ende" der Folgen mehr gibt und somit kein Gegenbeispiel wie oben.
Insgesamt gibt es dann 2 Äquivalenzklassen ([a], [b]) und somit bleibt die Sprache dennoch regulär.
%% Cell type:code id: tags:
``` prob
```
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment