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

Erweiterung des Notebooks um ein zweites Beispiel

parent 361420e9
No related branches found
No related tags found
1 merge request!1Master
%% Cell type:markdown id: tags:
# Der Satz von Myhill und Nerode
Wir betrachten die Myhill-Nerode-Äquivalenzrelation anhand der Sprache L = {a, b, aa, bb, aac, bbc, ccc}.
%% Cell type:code id: tags:
``` prob
MACHINE EquivalenceRelation
/* Ein Modell der Myhill-Nerode Äquivalenzrelation R_L,
der entsprechenden Äquivalenzklassen und dem Index der Sprache.*/
SETS
Alphabet = {a,b,c}
CONSTANTS L, RL, maxsize, All, Classes, index
DEFINITIONS
class(x) == {y | x↦y : RL} ;
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_FUNCTION3 == {(1, 0, "Wort:"), (2, 0, "Äquivalenzklasse:")};
PROPERTIES
L ⊆ seq(Alphabet) ∧
// All = {z | z∈seq(Alphabet) ∧ size(z)<=maxsz} & /* beschränkt auf endliche Folgen */
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))}) ∧
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} */
index = card( Classes )
ASSERTIONS
/* Test ob wir eine Äquivalenzrelation haben: */
∀x.(x∈All ⇒ x↦x ∈ RL); /* Reflexivität */
∀(x,y).(x↦y ∈ RL ⇒ y↦x ∈ RL); /* Symetrie */
∀(x,y,z).(x↦y ∈ RL ∧ y↦z ∈ RL ⇒ x↦z ∈ RL); /* Transitivität */
/* Einige Beispiele : */
[a,a] ↦ [b,b] ∈ RL;
[a,a] ↦ [c,c] ∉ RL;
[b,b,c] ↦ [c,c,c] ∈ RL;
class([a,a]) = {[a,a],[b,b]};
class([c,c,c]) = {[a,a,c],[b,b,c],[c,c,c]}
/* Der durch die Äquivalenzklassen induzierte DFA: */
VARIABLES z, word
INVARIANT z ⊆ All ∧ word ∈ seq(Alphabet)
INITIALISATION z := class([]); word := []
OPERATIONS
Delta(terminal) = PRE terminal∈Alphabet THEN
ANY x WHERE x∈z ∧ ∀x2.(x2∈z ⇒ size(x2)≥size(x)) THEN
z := class(x^[terminal]);
word := word^[terminal]
END
END;
Final = SELECT z ∩ L ≠ {} THEN skip END
END
```
%% Output
Loaded machine: EquivalenceRelation
%% 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
index
```
%% Output
$8$
8
%% Cell type:markdown id: tags:
Da der $Index(L)=8<\infty$ ist die gegebene Sprache regulär.
%% Cell type:markdown id: tags:
Durch die Äquivalenzklassen wird ein Minimalautomat induziert.
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.
%% Cell type:code id: tags:
``` prob
:browse
```
%% Output
Machine: EquivalenceRelation
Sets: Alphabet
Constants: L, RL, maxsize, All, Classes, index
Variables: z, word
Operations:
Delta(a)
Delta(b)
Delta(c)
%% Cell type:code id: tags:
``` prob
:exec Delta terminal=a
```
%% Output
Executed operation: Delta(a)
%% Cell type:code id: tags:
``` prob
:exec Delta terminal=a
```
%% Output
Executed operation: Delta(a)
%% Cell type:code id: tags:
``` prob
:show
```
%% Output
<table style="font-family:monospace"><tbody>
<tr>
<td style="padding:10px">Wort:</td>
<td style="padding:10px">a</td>
<td style="padding:10px">a</td>
</tr>
<tr>
<td style="padding:10px">Äquivalenzklasse:</td>
<td style="padding:10px">{{(1|->a),(2|->a)},{(1|->b),(2|->b)}}</td>
<td style="padding:0px"></td>
</tr>
</tbody></table>
<Animation function visualisation>
%% Cell type:markdown id: tags:
Ein weiteres Beispiel ist die Sprache L={a^n | n>=0}.
%% Cell type:code id: tags:
``` prob
MACHINE EquivalenceRelation2
SETS
Alphabet = {a,b,c}
CONSTANTS L, RL, maxsize, All, Classes, index
DEFINITIONS
class(x) == {y | x↦y : RL} ;
PROPERTIES
L ⊆ seq(Alphabet) ∧
// All = {z | z∈seq(Alphabet) ∧ size(z)≤maxsize} & /* Beschränkt auf endliche Folgen */
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))}) ∧
/*L = {x | x=a^n ∧ size(x)≤maxsize} Beschränkt auf endliche Folgen*/
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} */
index = card( Classes )
END
```
%% Output
Loaded machine: EquivalenceRelation2
%% 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
index
```
%% Output
$8$
8
$5$
5
%% Cell type:markdown id: tags:
Da der $Index(L)=8<\infty$ ist die gegebene Sprache 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.
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$.
%% Cell type:code id: tags:
``` prob
L
```
%% 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})\}\}$
{∅,{(1↦a)},{(1↦a),(2↦a)},{(1↦a),(2↦a),(3↦a)}}
%% Cell type:code id: tags:
``` prob
x=[a] ∧ y=[a, a] ∧ ∃z.(z∈All ∧ not(x^z ∈ L ⇔ y^z ∈ L)) /*Gegenbeispiel für [a] ↦ [a,a] ∈ R_L*/
```
%% Output
$\mathit{TRUE}$
**Solution:**
* $\mathit{x} = \{(1\mapsto \mathit{a})\}$
* $\mathit{y} = \{(1\mapsto \mathit{a}),(2\mapsto \mathit{a})\}$
* $\mathit{z} = \{(1\mapsto \mathit{a}),(2\mapsto \mathit{a})\}$
TRUE
Solution:
x = {(1↦a)}
y = {(1↦a),(2↦a)}
z = {(1↦a),(2↦a)}
%% Cell type:markdown id: tags:
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.
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment