Skip to content
Snippets Groups Projects
Commit 0b8446e1 authored by dgelessus's avatar dgelessus
Browse files

Add NFA_to_DFA.ipynb

parent 2947b54c
No related branches found
No related tags found
No related merge requests found
Show whitespace changes
Inline Side-by-side
notebooks/models/NFA_to_DFA.ipynb 0 → 100644
+ 1019
− 0
View file @ 0b8446e1
%% Cell type:markdown id: tags:
# Application: Course Notes for Theoretical Computer Science (NFA)
#### DEFINITION 2.9 (NFA)
A non-deterministic finite automaton
(NFA) is a 5-tuple $M = (\Sigma, Z, \delta , S, F)$, where
* $\Sigma$ is the alphabet,
* $Z$ is a finite set of states with $\Sigma \cap Z = \emptyset$,
* $\delta : Z \times \Sigma \rightarrow POW(Z)$ is the transition function
($\pow(Z)$ is the powerset of $Z$, the set of all subsets of $Z$),
* $S \subseteq Z$ is the set of initial states,
* $F \subseteq Z$ is the set of final (accepting) states.
#### DEFINITION 2.10 (Language of an NFA)
Die erweiterte Überführungsfunktion $\widehat{\delta} :
\pow(Z) \times \Sigma^* \rightarrow \pow(Z)$ von $M$ ist
induktiv definiert:
* $\widehat{\delta}(Z', \lambda) = Z'$
* $\widehat{\delta}(Z', ax) = \bigcup_{z \in Z'} \widehat{\delta}(\delta(z,a), x)$
für alle $Z' \subseteq Z$, $a \in \Sigma$ und $x \in \Sigma^*$.
Die vom NFA $M$ akzeptierte Sprache ist definiert durch
* L(M) = $\{w \in \Sigma^* \mid \widehat{\delta}(S,w) \cap F \neq \emptyset\}$
%% Cell type:markdown id: tags:
Wie laden nun ein B Modell welches diese Definitionen beinhaltet.
Wörter werden dabei in der B Sprache mit eckigen Klammern und Kommas geschrieben; aus 101 wird [1,0,1].
Gewisse griechische Zeichen sind in der B Sprache als Schlüsselwörter reserviert, zB $\lambda$.
Auch kann man leider $\hat$ in Bezeichnern verwenden.
Deshalb wird aus
* $\Sigma^*$ wird ```seq(Σ)```
* $\widehat{\delta}$ wird ```δs```
%% Cell type:code id: tags:
``` prob
::load
MACHINE NFA_nach_DFA
SETS
Z = {z0,z1,z2,z3}
ABSTRACT_CONSTANTS δs, L
CONSTANTS Σ, S, F, δ
PROPERTIES
S ⊆ Z ∧ F ⊆ Z ∧ δ ∈ (Z×Σ) → ℙ(Z) ∧
/* Definition der erweiterten Übergangsfunktion */
δs ∈ (ℙ(Z)×seq(Σ)) → ℙ(Z) ∧
δs = λ(Z2,s).(Z2⊆Z ∧ s∈seq(Σ) |
IF s=[] THEN Z2
ELSE ⋃(z).(z∈Z2|δs(δ(z,first(s)),tail(s))) END)
∧
/* die vom Automaten generierte Sprache */
L = {ω|ω∈seq(Σ) ∧ δs(S,ω) ∩ F ≠ ∅}
∧
/* Nun ein Beispiel-Automat von Folie 24 (Info 4) */
Σ = {0,1} ∧
S = {z0} ∧ F={z2} ∧
δ = { (z0,0)↦{z0}, (z0,1)↦{z0,z1},
(z1,0)↦{z2}, (z1,1)↦{z2},
(z2,0)↦{z3}, (z2,1)↦{z3},
(z3,0)↦{z3}, (z3,1)↦{z3} }
END
```
%% Output
Loaded machine: NFA_nach_DFA
%% 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:markdown id: tags:
Die Übergangsfunktion $\delta$ gibt us für einen Zustand und ein Symbol die möglichen nächsten Zustande an:
%% Cell type:code id: tags:
``` prob
δ(z0,1)
```
%% Output
$\{\mathit{z0},\mathit{z1}\}$
{z0,z1}
%% Cell type:markdown id: tags:
As you can see, the automaton is non-deterministic as there are two successors for the state ```z0``` and the input symbol ```1```.
We can examine the transition function of this automaton as a table:
%% Cell type:code id: tags:
``` prob
:table δ
```
%% Output
|prj11|prj12|prj2|
|---|---|---|
|$\mathit{z0}$|$0$|$\{\mathit{z0}\}$|
|$\mathit{z0}$|$1$|$\{\mathit{z0},\mathit{z1}\}$|
|$\mathit{z1}$|$0$|$\{\mathit{z2}\}$|
|$\mathit{z1}$|$1$|$\{\mathit{z2}\}$|
|$\mathit{z2}$|$0$|$\{\mathit{z3}\}$|
|$\mathit{z2}$|$1$|$\{\mathit{z3}\}$|
|$\mathit{z3}$|$0$|$\{\mathit{z3}\}$|
|$\mathit{z3}$|$1$|$\{\mathit{z3}\}$|
prj11 prj12 prj2
z0 0 {z0}
z0 1 {z0,z1}
z1 0 {z2}
z1 1 {z2}
z2 0 {z3}
z2 1 {z3}
z3 0 {z3}
z3 1 {z3}
%% Cell type:markdown id: tags:
Alternatively, we can view it as graph:
%% Cell type:code id: tags:
``` prob
:dot expr_as_graph ("0",{x,y| x∈Z & y:δ(x,0)},
"1",{x,y| x∈S & y∈δ(x,1)})
```
%% Output
<Dot visualization: expr_as_graph [("0",{x,y|x:Z & y:δ(x, 0)})]>
%% Cell type:markdown id: tags:
Die Funktion $\widehat{\delta}$ berechnet die möglichen Zustände nach dem Abarbeiten eines Wortes. Zum Beispiel, kann sich der Automat nach dem Abarbeiten des Präfixes 111 in folgenden Zuständen befinden:
%% Cell type:code id: tags:
``` prob
δs(S,[1,1,1])
```
%% Output
$\{\mathit{z0},\mathit{z1},\mathit{z2},\mathit{z3}\}$
{z0,z1,z2,z3}
%% Cell type:markdown id: tags:
Der Automat akzeptiert zum Beispiel das Wort 111 und das Wort 101 nicht, da:
%% Cell type:code id: tags:
``` prob
δs(S,[1,1,1]) ∩ F
```
%% Output
$\{\mathit{z2}\}$
{z2}
%% Cell type:markdown id: tags:
Folgende Wörter der Länge 3 werden vom Automaten akzeptiert:
%% Cell type:code id: tags:
``` prob
:table {x,y,z| [x,y,z]∈L}
```
%% Output
|x|y|z|
|---|---|---|
|$0$|$1$|$0$|
|$0$|$1$|$1$|
|$1$|$1$|$0$|
|$1$|$1$|$1$|
x y z
0 1 0
0 1 1
1 1 0
1 1 1
%% Cell type:markdown id: tags:
and the following words of length 3 are not accepted:
%% Cell type:code id: tags:
``` prob
:table {x,y,z| {x,y,z} ⊆ Σ & ¬([x,y,z]∈L)}
```
%% Output
|x|y|z|
|---|---|---|
|$0$|$0$|$0$|
|$0$|$0$|$1$|
|$1$|$0$|$0$|
|$1$|$0$|$1$|
x y z
0 0 0
0 0 1
1 0 0
1 0 1
%% Cell type:markdown id: tags:
Es stellt sich die Frage, ob NFAs mächtiger sind als DFAs. Die
Antwort lautet: Nein.
## Theorem (Rabin und Scott)
Jede von einem NFA akzeptierte Sprache kann auch von einem DFA akzeptiert
werden.
### Beweis
Sei $M = (\Sigma, Z, \delta , S, E)$ ein NFA.
Konstruiere einen zu
$M$ äquivalenten DFA
$M' = (\Sigma, \pow(Z), \delta' ,z_0', F)$ wie folgt:
* Zustandsmenge von $M'$: die Potenzmenge $\pow(Z)$ von $Z$,
* $\delta'(Z' , a) = \widehat{\delta}(Z',a)$ für alle $Z' \subseteq Z$ und $a \in \Sigma$,
* $z_0'=S$,
* $F = \{ Z' \subseteq Z \mid Z' \cap E \neq \emptyset\}$.
Offenbar sind M' und M äquivalent, denn für alle ...
%% Cell type:markdown id: tags:
Für den oben geladen Automaten können wir diese Konstruktion illustrieren.
Die Potenzmenge der Zustände ist:
%% Cell type:code id: tags:
``` prob
ℙ(Z)
```
%% Output
$\renewcommand{\emptyset}{\mathord\varnothing}\{\emptyset,\{\mathit{z0}\},\{\mathit{z0},\mathit{z1}\},\{\mathit{z0},\mathit{z2}\},\{\mathit{z0},\mathit{z3}\},\{\mathit{z1}\},\{\mathit{z0},\mathit{z1},\mathit{z2}\},\{\mathit{z0},\mathit{z1},\mathit{z3}\},\{\mathit{z1},\mathit{z2}\},\{\mathit{z1},\mathit{z3}\},\{\mathit{z0},\mathit{z1},\mathit{z2},\mathit{z3}\},\{\mathit{z2}\},\{\mathit{z0},\mathit{z2},\mathit{z3}\},\{\mathit{z1},\mathit{z2},\mathit{z3}\},\{\mathit{z2},\mathit{z3}\},\{\mathit{z3}\}\}$
{∅,{z0},{z0,z1},{z0,z2},{z0,z3},{z1},{z0,z1,z2},{z0,z1,z3},{z1,z2},{z1,z3},{z0,z1,z2,z3},{z2},{z0,z2,z3},{z1,z2,z3},{z2,z3},{z3}}
%% Cell type:markdown id: tags:
Tabellarisch k¨ønnen wir $\widehat{\delta}$ für $\pow(Z)$ wie folgt ausrechnen:
%% Cell type:code id: tags:
``` prob
:table {x,a,y| a∈Σ & x∈ℙ(Z) & y=δs(x,[a])}
```
%% Output
|x|a|y|
|---|---|---|
|$\renewcommand{\emptyset}{\mathord\varnothing}\renewcommand{\emptyset}{\mathord\varnothing}\renewcommand{\emptyset}{\mathord\varnothing}\renewcommand{\emptyset}{\mathord\varnothing}\emptyset$|$0$|$\emptyset$|
|$\emptyset$|$1$|$\emptyset$|
|$\{\mathit{z0}\}$|$0$|$\{\mathit{z0}\}$|
|$\{\mathit{z0}\}$|$1$|$\{\mathit{z0},\mathit{z1}\}$|
|$\{\mathit{z0},\mathit{z1}\}$|$0$|$\{\mathit{z0},\mathit{z2}\}$|
|$\{\mathit{z0},\mathit{z1}\}$|$1$|$\{\mathit{z0},\mathit{z1},\mathit{z2}\}$|
|$\{\mathit{z0},\mathit{z2}\}$|$0$|$\{\mathit{z0},\mathit{z3}\}$|
|$\{\mathit{z0},\mathit{z2}\}$|$1$|$\{\mathit{z0},\mathit{z1},\mathit{z3}\}$|
|$\{\mathit{z0},\mathit{z3}\}$|$0$|$\{\mathit{z0},\mathit{z3}\}$|
|$\{\mathit{z0},\mathit{z3}\}$|$1$|$\{\mathit{z0},\mathit{z1},\mathit{z3}\}$|
|$\{\mathit{z1}\}$|$0$|$\{\mathit{z2}\}$|
|$\{\mathit{z1}\}$|$1$|$\{\mathit{z2}\}$|
|$\{\mathit{z0},\mathit{z1},\mathit{z2}\}$|$0$|$\{\mathit{z0},\mathit{z2},\mathit{z3}\}$|
|$\{\mathit{z0},\mathit{z1},\mathit{z2}\}$|$1$|$\{\mathit{z0},\mathit{z1},\mathit{z2},\mathit{z3}\}$|
|$\{\mathit{z0},\mathit{z1},\mathit{z3}\}$|$0$|$\{\mathit{z0},\mathit{z2},\mathit{z3}\}$|
|$\{\mathit{z0},\mathit{z1},\mathit{z3}\}$|$1$|$\{\mathit{z0},\mathit{z1},\mathit{z2},\mathit{z3}\}$|
|$\{\mathit{z1},\mathit{z2}\}$|$0$|$\{\mathit{z2},\mathit{z3}\}$|
|$\{\mathit{z1},\mathit{z2}\}$|$1$|$\{\mathit{z2},\mathit{z3}\}$|
|$\{\mathit{z1},\mathit{z3}\}$|$0$|$\{\mathit{z2},\mathit{z3}\}$|
|$\{\mathit{z1},\mathit{z3}\}$|$1$|$\{\mathit{z2},\mathit{z3}\}$|
|$\{\mathit{z0},\mathit{z1},\mathit{z2},\mathit{z3}\}$|$0$|$\{\mathit{z0},\mathit{z2},\mathit{z3}\}$|
|$\{\mathit{z0},\mathit{z1},\mathit{z2},\mathit{z3}\}$|$1$|$\{\mathit{z0},\mathit{z1},\mathit{z2},\mathit{z3}\}$|
|$\{\mathit{z2}\}$|$0$|$\{\mathit{z3}\}$|
|$\{\mathit{z2}\}$|$1$|$\{\mathit{z3}\}$|
|$\{\mathit{z0},\mathit{z2},\mathit{z3}\}$|$0$|$\{\mathit{z0},\mathit{z3}\}$|
|$\{\mathit{z0},\mathit{z2},\mathit{z3}\}$|$1$|$\{\mathit{z0},\mathit{z1},\mathit{z3}\}$|
|$\{\mathit{z1},\mathit{z2},\mathit{z3}\}$|$0$|$\{\mathit{z2},\mathit{z3}\}$|
|$\{\mathit{z1},\mathit{z2},\mathit{z3}\}$|$1$|$\{\mathit{z2},\mathit{z3}\}$|
|$\{\mathit{z2},\mathit{z3}\}$|$0$|$\{\mathit{z3}\}$|
|$\{\mathit{z2},\mathit{z3}\}$|$1$|$\{\mathit{z3}\}$|
|$\{\mathit{z3}\}$|$0$|$\{\mathit{z3}\}$|
|$\{\mathit{z3}\}$|$1$|$\{\mathit{z3}\}$|
x a y
{} 0 {}
{} 1 {}
{z0} 0 {z0}
{z0} 1 {z0,z1}
{z0,z1} 0 {z0,z2}
{z0,z1} 1 {z0,z1,z2}
{z0,z2} 0 {z0,z3}
{z0,z2} 1 {z0,z1,z3}
{z0,z3} 0 {z0,z3}
{z0,z3} 1 {z0,z1,z3}
{z1} 0 {z2}
{z1} 1 {z2}
{z0,z1,z2} 0 {z0,z2,z3}
{z0,z1,z2} 1 {z0,z1,z2,z3}
{z0,z1,z3} 0 {z0,z2,z3}
{z0,z1,z3} 1 {z0,z1,z2,z3}
{z1,z2} 0 {z2,z3}
{z1,z2} 1 {z2,z3}
{z1,z3} 0 {z2,z3}
{z1,z3} 1 {z2,z3}
{z0,z1,z2,z3} 0 {z0,z2,z3}
{z0,z1,z2,z3} 1 {z0,z1,z2,z3}
{z2} 0 {z3}
{z2} 1 {z3}
{z0,z2,z3} 0 {z0,z3}
{z0,z2,z3} 1 {z0,z1,z3}
{z1,z2,z3} 0 {z2,z3}
{z1,z2,z3} 1 {z2,z3}
{z2,z3} 0 {z3}
{z2,z3} 1 {z3}
{z3} 0 {z3}
{z3} 1 {z3}
%% Cell type:markdown id: tags:
Graphisch lässt sich der Automat wie folgt darstellen; die Start und Endzustände sind noch nicht schön markiert.
%% Cell type:code id: tags:
``` prob
:pref DOT_DECOMPOSE_NODES=FALSE
```
%% Output
Preference changed: DOT_DECOMPOSE_NODES = FALSE
%% Cell type:code id: tags:
``` prob
:dot expr_as_graph ("0",{x,y| x∈ℙ(Z) & δs(x,[0]) = y},
"1",{x,y| x∈ℙ(Z) & δs(x,[1]) = y},
"start", {x,y|x=y & x={z0}},
"end", {x,y|x=y & x∩F ≠ ∅})
```
%% Output
<Dot visualization: expr_as_graph [("0",{x,y|x:POW(Z) & δs(x, [0])=y})]>
%% 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