Skip to content
Snippets Groups Projects
Commit 73f0cbb1 authored by Michael Leuschel's avatar Michael Leuschel
Browse files

add DPDA notebook

parent 4b4cd44b
Branches
No related tags found
No related merge requests found
Show whitespace changes
Inline Side-by-side
info4/kapitel-4/DPDA.ipynb 0 → 100644
+ 651
− 0
View file @ 73f0cbb1
%% Cell type:markdown id: tags:
# DPDA
Ein __deterministischer Kellerautomat__
(kurz DPDA für __deterministic push-down automaton__) ist ein $7$-Tupel
$M = (\Sigma, \Gamma, Z, \delta , z_0, \#,F)$, wobei
* $\Sigma$ das Eingabe-Alphabet ist,
* $\Gamma$ das Kelleralphabet,
* $Z$ eine endliche Menge von Zuständen,
* $\delta : Z \times (\Sigma \cup \{\lambda\}) \times \Gamma
\rightarrow \mathfrak{P}_e(Z \times \Gamma^{\ast})$ die
Überführungsfunktion,
* $z_0 \in Z$ der Startzustand,
* $\# \in \Gamma$ das Bottom-Symbol im Keller,
* $F \subseteq Z$ sind die Endzustände
wo gilt:
* $(\forall a \in \Sigma)\, (\forall A \in \Gamma)\, (\forall z \in
Z)\, [ \|\delta(z, a, A)\| + \|\delta(z, \lambda , A)\| \leq 1]$
Anmerkung: $\mathfrak{P}_e(Z \times \Gamma^{\ast})$ ist die Menge aller
__endlichen__ Teilmengen von $Z \times \Gamma^{\ast}$.
%% Cell type:code id: tags:
``` prob
::load
MACHINE DPDA
/* B Modell eines PDA */
SETS
Z = {z0,z1,ze}; // die Zustände des Automaten, z0 ist der Startzustand
SYMBOLE={a,b, A, BOT, lambda} /* BOT = # = Bottom-Symbol im Keller*/
DEFINITIONS
ANIMATION_FUNCTION_DEFAULT == {(1,1,z)};
ANIMATION_FUNCTION == {2}*α ∪ {3}*(γ);
ANIMATION_FUNCTION1 == {(1,0,"z: "),(2,0,"α:"),(3,0,"γ:")};
ANIMATION_STR_JUSTIFY_LEFTx == TRUE;
SET_PREF_PP_SEQUENCES == TRUE
CONSTANTS δ, F, Σ, Γ
PROPERTIES
Σ = {a,b} // das Eingabe-Alphabet
∧
Γ = {A,BOT} // das Kelleralphabet
∧
/* Der PDA für {a^m b^m| m>=1} ; Beispiel von Info 4 (Folie 95ff) */
δ = { (z0,a,BOT) ↦ (z0,[A,BOT]),
(z0,a,A) ↦ (z0,[A,A]),
(z0,b,A) ↦ (z1,[]),
(z1,lambda,BOT) ↦ (ze,[]),
(z1,b,A) ↦ (z1,[]) } ∧
F = {ze} // die Endzustände
// Anmerkung: δ ist hier als Relation anstatt als Funktion zu Mengen definiert
// Deshalb entspricht δ[{(z,a,g)}] in der B Maschine δ(z,a,g) aus dem Skript
ASSERTIONS
!(a,A,z).(a∈Σ ∧ A∈Γ ∧ z∈Z => card(δ[{(z,a,A)}]) + card(δ[{(z,a,A)}]) ≤ 1)
/*@desc Die Überführungsfunktion ist deterministisch */
VARIABLES
z, α, γ // Konfiguration in dem sich der PDA befindet
INVARIANT
z ∈ Z ∧ // der aktuelle Zustand
α ∈ seq(Σ) ∧ // der noch zu lesende Teil des Eingabeworts
γ ∈ seq(Γ) // aktuelle Kellerinhalt
INITIALISATION
z := z0 ||
γ := [BOT] || // Initialisierung des Stapels
α := [a,a,b,b] // das Eingabewort
OPERATIONS
// die Operationen Schritt und LambdaSchritt modellieren
// Schritte in der Ableitungsrelation
Schritt(z‘,s) = PRE α ≠ ∅ ∧ γ ≠ ∅ ∧
z‘↦s ∈ δ[{(z,first(α),first(γ))}] THEN
z := z‘ || // in den neuen Zustand wechseln
α := tail(α) || // das erste Symbol auf der Eingabe löschen
γ := s^tail(γ) // s auf den Stapel packen
END;
LambdaSchritt(z‘,s) = PRE γ ≠ ∅ ∧
z‘↦s ∈ δ[{(z,lambda,first(γ))}] THEN
z := z‘ || // in den neuen Zustand wechseln
γ := s^tail(γ) // s auf den Stapel packen
END;
Akzeptieren = PRE γ = ∅ ∧ z∈F THEN
/* Wir akzeptieren wenn Eingabe leer und wir in einem Endzustand sind */
skip END;
AkzeptierenMitLeeremKeller = PRE γ = ∅ ∧ α = ∅ THEN
/* Wir akzeptieren wenn Eingabe und Stapel leer sind */
skip END
END
```
%% Output
Loaded machine: DPDA
%% 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:
Wir prüfen nun ob der PDA auch wirklich deterministisch ist:
%% Cell type:code id: tags:
``` prob
!(a,A,z).(a∈Σ ∧ A∈Γ ∧ z∈Z => card(δ[{(z,a,A)}]) + card(δ[{(z,lambda,A)}]) ≤ 1)
```
%% Output
$\mathit{TRUE}$
TRUE
%% Cell type:markdown id: tags:
Wir können uns auch tabellarisch für jede Kombination an Symbolen und Zuständen die Kardinalität der möglichen Übergange ausgeben:
%% Cell type:code id: tags:
``` prob
:table {a,A,z,ca,cl| a∈Σ ∧ A∈Γ ∧ z∈Z ∧ ca=card(δ[{(z,a,A)}]) & cl = card(δ[{(z,lambda,A)}])}
```
%% Output
|a|A|z|ca|cl|
|---|---|---|---|---|
|$\mathit{a}$|$\mathit{A}$|$\mathit{z0}$|$1$|$0$|
|$\mathit{a}$|$\mathit{A}$|$\mathit{z1}$|$0$|$0$|
|$\mathit{a}$|$\mathit{A}$|$\mathit{ze}$|$0$|$0$|
|$\mathit{a}$|$\mathit{BOT}$|$\mathit{z0}$|$1$|$0$|
|$\mathit{a}$|$\mathit{BOT}$|$\mathit{z1}$|$0$|$1$|
|$\mathit{a}$|$\mathit{BOT}$|$\mathit{ze}$|$0$|$0$|
|$\mathit{b}$|$\mathit{A}$|$\mathit{z0}$|$1$|$0$|
|$\mathit{b}$|$\mathit{A}$|$\mathit{z1}$|$1$|$0$|
|$\mathit{b}$|$\mathit{A}$|$\mathit{ze}$|$0$|$0$|
|$\mathit{b}$|$\mathit{BOT}$|$\mathit{z0}$|$0$|$0$|
|$\mathit{b}$|$\mathit{BOT}$|$\mathit{z1}$|$0$|$1$|
|$\mathit{b}$|$\mathit{BOT}$|$\mathit{ze}$|$0$|$0$|
a A z ca cl
a A z0 1 0
a A z1 0 0
a A ze 0 0
a BOT z0 1 0
a BOT z1 0 1
a BOT ze 0 0
b A z0 1 0
b A z1 1 0
b A ze 0 0
b BOT z0 0 0
b BOT z1 0 1
b BOT ze 0 0
%% Cell type:code id: tags:
``` prob
:browse
```
%% Output
Machine: DPDA
Sets: Z, SYMBOLE
Constants: δ, F, Σ, Γ
Variables: z, α, γ
Operations:
Schritt(z0,[A,BOT])
%% Cell type:code id: tags:
``` prob
:exec Schritt
```
%% Output
Executed operation: Schritt(z0,[A,BOT])
%% Cell type:code id: tags:
``` prob
:show
```
%% Output
<table style="font-family:monospace"><tbody>
<tr>
<td style="padding:10px">z: </td>
<td style="padding:10px">z0</td>
<td style="padding:0px"></td>
<td style="padding:0px"></td>
</tr>
<tr>
<td style="padding:10px">α:</td>
<td style="padding:10px">a</td>
<td style="padding:10px">b</td>
<td style="padding:10px">b</td>
</tr>
<tr>
<td style="padding:10px">γ:</td>
<td style="padding:10px">A</td>
<td style="padding:10px">BOT</td>
<td style="padding:0px"></td>
</tr>
</tbody></table>
<Animation function visualisation>
%% Cell type:code id: tags:
``` prob
:exec Schritt
```
%% Output
Executed operation: Schritt(z0,[A,A])
%% Cell type:code id: tags:
``` prob
:show
```
%% Output
<table style="font-family:monospace"><tbody>
<tr>
<td style="padding:10px">z: </td>
<td style="padding:10px">z0</td>
<td style="padding:0px"></td>
<td style="padding:0px"></td>
</tr>
<tr>
<td style="padding:10px">α:</td>
<td style="padding:10px">b</td>
<td style="padding:10px">b</td>
<td style="padding:0px"></td>
</tr>
<tr>
<td style="padding:10px">γ:</td>
<td style="padding:10px">A</td>
<td style="padding:10px">A</td>
<td style="padding:10px">BOT</td>
</tr>
</tbody></table>
<Animation function visualisation>
%% Cell type:code id: tags:
``` prob
:exec Schritt
```
%% Output
Executed operation: Schritt(z1,[])
%% Cell type:code id: tags:
``` prob
:show
```
%% Output
<table style="font-family:monospace"><tbody>
<tr>
<td style="padding:10px">z: </td>
<td style="padding:10px">z1</td>
<td style="padding:0px"></td>
</tr>
<tr>
<td style="padding:10px">α:</td>
<td style="padding:10px">b</td>
<td style="padding:0px"></td>
</tr>
<tr>
<td style="padding:10px">γ:</td>
<td style="padding:10px">A</td>
<td style="padding:10px">BOT</td>
</tr>
</tbody></table>
<Animation function visualisation>
%% Cell type:code id: tags:
``` prob
:exec Schritt
```
%% Output
Executed operation: Schritt(z1,[])
%% Cell type:code id: tags:
``` prob
:show
```
%% Output
<table style="font-family:monospace"><tbody>
<tr>
<td style="padding:10px">z: </td>
<td style="padding:10px">z1</td>
</tr>
<tr>
<td style="padding:10px">α:</td>
<td style="padding:0px"></td>
</tr>
<tr>
<td style="padding:10px">γ:</td>
<td style="padding:10px">BOT</td>
</tr>
</tbody></table>
<Animation function visualisation>
%% Cell type:code id: tags:
``` prob
:browse
```
%% Output
Machine: DPDA
Sets: Z, SYMBOLE
Constants: δ, F, Σ, Γ
Variables: z, α, γ
Operations:
LambdaSchritt(ze,[])
%% Cell type:code id: tags:
``` prob
:exec LambdaSchritt
```
%% Output
Executed operation: LambdaSchritt(ze,[])
%% Cell type:code id: tags:
``` prob
:show
```
%% Output
<table style="font-family:monospace"><tbody>
<tr>
<td style="padding:10px">z: </td>
<td style="padding:10px">ze</td>
</tr>
<tr>
<td style="padding:10px">α:</td>
<td style="padding:0px"></td>
</tr>
<tr>
<td style="padding:10px">γ:</td>
<td style="padding:0px"></td>
</tr>
</tbody></table>
<Animation function visualisation>
%% Cell type:code id: tags:
``` prob
:browse
```
%% Output
Machine: DPDA
Sets: Z, SYMBOLE
Constants: δ, F, Σ, Γ
Variables: z, α, γ
Operations:
Akzeptieren()
AkzeptierenMitLeeremKeller()
%% Cell type:code id: tags:
``` prob
:exec Akzeptieren
```
%% Output
Executed operation: Akzeptieren()
%% 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