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

add shortest Solution

parent 561ba09d
Branches
No related tags found
No related merge requests found
Show whitespace changes
Inline Side-by-side
info4/kapitel-11/PCP.ipynb
+ 284
− 17
View file @ 67773a5e
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
# PCP - Das Postsche Korrespondenzproblem # PCP - Das Postsche Korrespondenzproblem
Sei $\Sigma$ ein Alphabet. Sei $\Sigma$ ein Alphabet.
Das __Postsche Korrespondenzproblem__ (über $\Sigma$) Das __Postsche Korrespondenzproblem__ (über $\Sigma$)
ist definiert durch ist definiert durch
$PCP_{\Sigma}$ = $\{ ((x_1, y_1), \ldots , (x_k, y_k)) |$ $PCP_{\Sigma}$ = $\{ ((x_1, y_1), \ldots , (x_k, y_k)) |$
so dass $k \in ℕ$ und $x_i, y_i \in \Sigma^{+}$ für $1 \leq i \leq k$} so dass $k \in ℕ$ und $x_i, y_i \in \Sigma^{+}$ für $1 \leq i \leq k$}
und es gibt $i_1, i_2, \ldots , i_n \in \{1, \ldots , k\}$, und es gibt $i_1, i_2, \ldots , i_n \in \{1, \ldots , k\}$,
so dass $x_{i_1} x_{i_2} \cdots x_{i_n} = y_{i_1} y_{i_2} \cdots so dass $x_{i_1} x_{i_2} \cdots x_{i_n} = y_{i_1} y_{i_2} \cdots
y_{i_n}$ y_{i_n}$
$\}$. $\}$.
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Diese Maschine modelliert das PCP Problem von Folie 35. Die einzelnen Lösungschritte (hinzufügen eines Indexes $i_j$) werden mit der Operation ```Schritt``` ausgeführt. Diese Maschine modelliert das PCP Problem von Folie 35. Die einzelnen Lösungschritte (hinzufügen eines Indexes $i_j$) werden mit der Operation ```Schritt``` ausgeführt.
Diese Maschine verhindert offensichtlich nutzlose Schritte, wo niemals eine Lösung gefunden werden kann, da der Anfang von x und y sich unterscheiden. Diese Maschine verhindert offensichtlich nutzlose Schritte, wo niemals eine Lösung gefunden werden kann, da der Anfang von x und y sich unterscheiden.
Sobald man eine Lösung gefunden hat ist die B Operation ```Lösung``` ausführbar. Sobald man eine Lösung gefunden hat ist die B Operation ```Lösung``` ausführbar.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
::load ::load
MACHINE PostCorrespondence_MC MACHINE PostCorrespondence_MC
/* Version wo die Schritt Operation nur sinnvolle Erweiterungen zulässt */ /* Version wo die Schritt Operation nur sinnvolle Erweiterungen zulässt */
CONSTANTS K, Σ CONSTANTS K, Σ
PROPERTIES PROPERTIES
Σ = {0,1} ∧ Σ = {0,1} ∧
K = [ [1]↦[1,0], [0,1]↦[1], [0,1,0] ↦ [1,0,0] ] /* Problem von Folie 35 */ K = [ [1]↦[1,0], [0,1]↦[1], [0,1,0] ↦ [1,0,0] ] /* Problem von Folie 35 */
VARIABLES x,y VARIABLES x,y
INVARIANT INVARIANT
x ∈ seq(Σ) ∧ y∈seq(Σ) x ∈ seq(Σ) ∧ y∈seq(Σ)
INITIALISATION x,y := <>,<> INITIALISATION x,y := <>,<>
OPERATIONS OPERATIONS
Schritt(i,ix,iy) = PRE i∈dom(K) ∧ K(i)=ix↦iy Schritt(i,ix,iy) = PRE i∈dom(K) ∧ K(i)=ix↦iy
∧ same_prefix(x^ix,y^iy) ∧ same_prefix(x^ix,y^iy)
/* kann man die beiden neuen Wörter überhaupt noch gleich machen ? */ /* kann man die beiden neuen Wörter überhaupt noch gleich machen ? */
THEN THEN
x := x ^ ix || x := x ^ ix ||
y := y ^ iy y := y ^ iy
END; END;
Lösung = SELECT x=y ∧ x ≠ [] THEN skip END Lösung = SELECT x=y ∧ x ≠ [] THEN skip END
DEFINITIONS DEFINITIONS
GOAL == (x=y ∧ x≠<>); GOAL == (x=y ∧ x≠<>);
ANIMATION_FUNCTION == {1}×x ∪ {2}×y ; ANIMATION_FUNCTION == {1}×x ∪ {2}×y ;
ANIMATION_FUNCTION_DEFAULT == {(1,(0,2)),(2,(0,3))} ∪ {1,2}×λi.(i∈dom(x)∪dom(y)|6); ANIMATION_FUNCTION_DEFAULT == {(1,(0,2)),(2,(0,3))} ∪ {1,2}×λi.(i∈dom(x)∪dom(y)|6);
ANIMATION_IMG0 == "images/sm_0.gif"; ANIMATION_IMG0 == "images/sm_0.gif";
ANIMATION_IMG1 == "images/sm_1.gif"; ANIMATION_IMG1 == "images/sm_1.gif";
ANIMATION_IMG2 == "images/sm_X.gif"; ANIMATION_IMG2 == "images/sm_X.gif";
ANIMATION_IMG3 == "images/sm_Y.gif"; ANIMATION_IMG3 == "images/sm_Y.gif";
ANIMATION_IMG6 == "images/sm_empty_box.gif"; ANIMATION_IMG6 == "images/sm_empty_box.gif";
SET_PREF_PP_SEQUENCES == TRUE; SET_PREF_PP_SEQUENCES == TRUE;
same_prefix(a,b) == LET ms BE ms=min({size(a),size(b)}) IN same_prefix(a,b) == LET ms BE ms=min({size(a),size(b)}) IN
a /|\ ms = b /|\ ms END a /|\ ms = b /|\ ms END
END END
``` ```
%% Output %% Output
Loaded machine: PostCorrespondence_MC Loaded machine: PostCorrespondence_MC
%% 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:0px"><img alt="2" src="images/sm_X.gif"/></td> <td style="padding:0px"><img alt="2" src="images/sm_X.gif"/></td>
</tr> </tr>
<tr> <tr>
<td style="padding:0px"><img alt="3" src="images/sm_Y.gif"/></td> <td style="padding:0px"><img alt="3" src="images/sm_Y.gif"/></td>
</tr> </tr>
</tbody></table> </tbody></table>
<Animation function visualisation> <Animation function visualisation>
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:browse :browse
``` ```
%% Output %% Output
Machine: PostCorrespondence_MC Machine: PostCorrespondence_MC
Sets: (none) Sets: (none)
Constants: K, Σ Constants: K, Σ
Variables: x, y Variables: x, y
Operations: Operations:
Schritt(1,[1],[1,0]) Schritt(1,[1],[1,0])
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Es wird nur Schritt mit $i=1$ angeboten, da sonst sich x und y am Anfang unterscheiden und wir nie mehr eine Lösung finden könnten. Es wird nur Schritt mit $i=1$ angeboten, da sonst sich x und y am Anfang unterscheiden und wir nie mehr eine Lösung finden könnten.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:exec Schritt i=1 :exec Schritt i=1
``` ```
%% Output %% Output
Executed operation: Schritt(1,[1],[1,0]) Executed operation: Schritt(1,[1],[1,0])
%% 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:0px"><img alt="2" src="images/sm_X.gif"/></td> <td style="padding:0px"><img alt="2" src="images/sm_X.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td> <td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td>
<td style="padding:0px"><img alt="6" src="images/sm_empty_box.gif"/></td> <td style="padding:0px"><img alt="6" src="images/sm_empty_box.gif"/></td>
</tr> </tr>
<tr> <tr>
<td style="padding:0px"><img alt="3" src="images/sm_Y.gif"/></td> <td style="padding:0px"><img alt="3" src="images/sm_Y.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td> <td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td> <td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td>
</tr> </tr>
</tbody></table> </tbody></table>
<Animation function visualisation> <Animation function visualisation>
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
x
```
%% Output
$[Hash,\mathit{z0},\mathit{a},\mathit{b},\mathit{Hash},\mathit{a},\mathit{z0},\mathit{b},\mathit{Hash},\mathit{a},\mathit{b},\mathit{z1},\mathit{Hash},\mathit{a},\mathit{b},\mathit{z2},\mathit{Hash},\mathit{a},\mathit{z2},\mathit{Hash},\mathit{z2},\mathit{Hash},Hash]$
[Hash,z0,a,b,Hash,a,z0,b,Hash,a,b,z1,Hash,a,b,z2,Hash,a,z2,Hash,z2,Hash,Hash]
%% Cell type:code id: tags:
``` prob
y
```
%% Output
$[Hash,\mathit{z0},\mathit{a},\mathit{b},\mathit{Hash},\mathit{a},\mathit{z0},\mathit{b},\mathit{Hash},\mathit{a},\mathit{b},\mathit{z1},\mathit{Hash},\mathit{a},\mathit{b},\mathit{z2},\mathit{Hash},\mathit{a},\mathit{z2},\mathit{Hash},\mathit{z2},\mathit{Hash},Hash]$
[Hash,z0,a,b,Hash,a,z0,b,Hash,a,b,z1,Hash,a,b,z2,Hash,a,z2,Hash,z2,Hash,Hash]
%% Cell type:code id: tags:
``` prob
:browse :browse
``` ```
%% Output %% Output
Machine: PostCorrespondence_MC Machine: PostCorrespondence_MC
Sets: (none) Sets: (none)
Constants: K, Σ Constants: K, Σ
Variables: x, y Variables: x, y
Operations: Operations:
Schritt(2,[0,1],[1]) Schritt(2,[0,1],[1])
Schritt(3,[0,1,0],[1,0,0]) Schritt(3,[0,1,0],[1,0,0])
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Hier gibt es zwei Möglichkeiten: wir können Index 2 oder 3 wählen Hier gibt es zwei Möglichkeiten: wir können Index 2 oder 3 wählen
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:exec Schritt i=2 :exec Schritt i=2
``` ```
%% Output %% Output
Executed operation: Schritt(2,[0,1],[1]) Executed operation: Schritt(2,[0,1],[1])
%% 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:0px"><img alt="2" src="images/sm_X.gif"/></td> <td style="padding:0px"><img alt="2" src="images/sm_X.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td> <td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td> <td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td> <td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td>
</tr> </tr>
<tr> <tr>
<td style="padding:0px"><img alt="3" src="images/sm_Y.gif"/></td> <td style="padding:0px"><img alt="3" src="images/sm_Y.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td> <td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td> <td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td> <td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td>
</tr> </tr>
</tbody></table> </tbody></table>
<Animation function visualisation> <Animation function visualisation>
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:exec Lösung :exec Lösung
``` ```
%% Output %% Output
Executed operation: Lösung() Executed operation: Lösung()
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Wir haben eine Lösung gefunden. Wir haben eine Lösung gefunden.
Um die Lösung von den Folien nachzuspielen gehen wir noch einmal züruck. Um die Lösung von den Folien nachzuspielen gehen wir noch einmal züruck.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:trace :trace
``` ```
%% Output %% Output
* -1: Root state * -1: Root state
* 0: `SETUP_CONSTANTS()` * 0: `SETUP_CONSTANTS()`
* 1: `INITIALISATION()` * 1: `INITIALISATION()`
* 2: `Schritt(1,[1],[1,0])` * 2: `Schritt(1,[1],[1,0])`
* 3: `Schritt(2,[0,1],[1])` * 3: `Schritt(2,[0,1],[1])`
* 4: `Lösung()` **(current)** * 4: `Lösung()` **(current)**
-1: Root state -1: Root state
0: SETUP_CONSTANTS() 0: SETUP_CONSTANTS()
1: INITIALISATION() 1: INITIALISATION()
2: Schritt(1,[1],[1,0]) 2: Schritt(1,[1],[1,0])
3: Schritt(2,[0,1],[1]) 3: Schritt(2,[0,1],[1])
4: Lösung() (current) 4: Lösung() (current)
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:goto 2 :goto 2
``` ```
%% Output %% Output
Changed to state with index 2 Changed to state with index 2
%% 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:0px"><img alt="2" src="images/sm_X.gif"/></td> <td style="padding:0px"><img alt="2" src="images/sm_X.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td> <td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td>
<td style="padding:0px"><img alt="6" src="images/sm_empty_box.gif"/></td> <td style="padding:0px"><img alt="6" src="images/sm_empty_box.gif"/></td>
</tr> </tr>
<tr> <tr>
<td style="padding:0px"><img alt="3" src="images/sm_Y.gif"/></td> <td style="padding:0px"><img alt="3" src="images/sm_Y.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td> <td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td> <td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td>
</tr> </tr>
</tbody></table> </tbody></table>
<Animation function visualisation> <Animation function visualisation>
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:exec Schritt i=3 :exec Schritt i=3
``` ```
%% Output %% Output
Executed operation: Schritt(3,[0,1,0],[1,0,0]) Executed operation: Schritt(3,[0,1,0],[1,0,0])
%% 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:0px"><img alt="2" src="images/sm_X.gif"/></td> <td style="padding:0px"><img alt="2" src="images/sm_X.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td> <td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td> <td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td> <td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td> <td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td>
<td style="padding:0px"><img alt="6" src="images/sm_empty_box.gif"/></td> <td style="padding:0px"><img alt="6" src="images/sm_empty_box.gif"/></td>
</tr> </tr>
<tr> <tr>
<td style="padding:0px"><img alt="3" src="images/sm_Y.gif"/></td> <td style="padding:0px"><img alt="3" src="images/sm_Y.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td> <td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td> <td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td> <td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td> <td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td> <td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td>
</tr> </tr>
</tbody></table> </tbody></table>
<Animation function visualisation> <Animation function visualisation>
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:exec Schritt i=3 :exec Schritt i=3
``` ```
%% Output %% Output
Executed operation: Schritt(3,[0,1,0],[1,0,0]) Executed operation: Schritt(3,[0,1,0],[1,0,0])
%% 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:0px"><img alt="2" src="images/sm_X.gif"/></td> <td style="padding:0px"><img alt="2" src="images/sm_X.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td> <td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td> <td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td> <td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td> <td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td> <td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td> <td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td> <td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td>
<td style="padding:0px"><img alt="6" src="images/sm_empty_box.gif"/></td> <td style="padding:0px"><img alt="6" src="images/sm_empty_box.gif"/></td>
</tr> </tr>
<tr> <tr>
<td style="padding:0px"><img alt="3" src="images/sm_Y.gif"/></td> <td style="padding:0px"><img alt="3" src="images/sm_Y.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td> <td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td> <td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td> <td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td> <td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td> <td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td> <td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td> <td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td> <td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td>
</tr> </tr>
</tbody></table> </tbody></table>
<Animation function visualisation> <Animation function visualisation>
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:exec Schritt i=2 :exec Schritt i=2
``` ```
%% Output %% Output
Executed operation: Schritt(2,[0,1],[1]) Executed operation: Schritt(2,[0,1],[1])
%% 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:0px"><img alt="2" src="images/sm_X.gif"/></td> <td style="padding:0px"><img alt="2" src="images/sm_X.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td> <td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td> <td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td> <td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td> <td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td> <td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td> <td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td> <td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td> <td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td> <td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td>
</tr> </tr>
<tr> <tr>
<td style="padding:0px"><img alt="3" src="images/sm_Y.gif"/></td> <td style="padding:0px"><img alt="3" src="images/sm_Y.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td> <td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td> <td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td> <td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td> <td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td> <td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td> <td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td> <td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td> <td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td> <td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td>
</tr> </tr>
</tbody></table> </tbody></table>
<Animation function visualisation> <Animation function visualisation>
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:exec Lösung :exec Lösung
``` ```
%% Output %% Output
Executed operation: Lösung() Executed operation: Lösung()
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:trace :trace
``` ```
%% Output %% Output
* -1: Root state * -1: Root state
* 0: `SETUP_CONSTANTS()` * 0: `SETUP_CONSTANTS()`
* 1: `INITIALISATION()` * 1: `INITIALISATION()`
* 2: `Schritt(1,[1],[1,0])` * 2: `Schritt(1,[1],[1,0])`
* 3: `Schritt(3,[0,1,0],[1,0,0])` * 3: `Schritt(3,[0,1,0],[1,0,0])`
* 4: `Schritt(3,[0,1,0],[1,0,0])` * 4: `Schritt(3,[0,1,0],[1,0,0])`
* 5: `Schritt(2,[0,1],[1])` * 5: `Schritt(2,[0,1],[1])`
* 6: `Lösung()` **(current)** * 6: `Lösung()` **(current)**
-1: Root state -1: Root state
0: SETUP_CONSTANTS() 0: SETUP_CONSTANTS()
1: INITIALISATION() 1: INITIALISATION()
2: Schritt(1,[1],[1,0]) 2: Schritt(1,[1],[1,0])
3: Schritt(3,[0,1,0],[1,0,0]) 3: Schritt(3,[0,1,0],[1,0,0])
4: Schritt(3,[0,1,0],[1,0,0]) 4: Schritt(3,[0,1,0],[1,0,0])
5: Schritt(2,[0,1],[1]) 5: Schritt(2,[0,1],[1])
6: Lösung() (current) 6: Lösung() (current)
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Sie können das B Modell oben mit anderen Werten für K ausprobieren: Sie können das B Modell oben mit anderen Werten für K ausprobieren:
- K = [ [0,1]↦[1], [0,1,0]↦[1,0,0], [1]↦[1,0] ] Problem von Folie 36 */ - K = [ [0,1]↦[1], [0,1,0]↦[1,0,0], [1]↦[1,0] ] Problem von Folie 36 */
- K = [ [1]↦[1,0,1], [1,0]↦[0,0], [0,1,1]↦[1,1] ] - K = [ [1]↦[1,0,1], [1,0]↦[0,0], [0,1,1]↦[1,1] ]
- K = [ [0,0,1]↦[0], [0,1]↦[0,1,1], [0,1]↦[1,0,1], [1,0] ↦ [0,0,1] ], Problem von Folie 32; kleinse Lösung hat 66 Elemente - K = [ [0,0,1]↦[0], [0,1]↦[0,1,1], [0,1]↦[1,0,1], [1,0] ↦ [0,0,1] ], Problem von Folie 32; kleinse Lösung hat 66 Elemente
Hier erst einmal Illustration der Lösung von Folie 36. Hier erst einmal Illustration der Lösung von Folie 36.
Folgende Maschine hat keinen vordefinierten Wert von K; man muss diesen der :constants Anweisung übergeben. Folgende Maschine hat keinen vordefinierten Wert von K; man muss diesen der :constants Anweisung übergeben.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
::load ::load
MACHINE PostCorrespondence_MC MACHINE PostCorrespondence_MC
/* Version wo die Schritt Operation nur sinnvolle Erweiterungen zulässt */ /* Version wo die Schritt Operation nur sinnvolle Erweiterungen zulässt */
CONSTANTS K, Σ CONSTANTS K, Σ
PROPERTIES PROPERTIES
Σ = {0,1} ∧ Σ = {0,1} ∧
K ∈ seq(seq(Σ)×seq(Σ)) K ∈ seq(seq(Σ)×seq(Σ))
VARIABLES x,y VARIABLES x,y
INVARIANT INVARIANT
x ∈ seq(Σ) ∧ y∈seq(Σ) x ∈ seq(Σ) ∧ y∈seq(Σ)
INITIALISATION x,y := <>,<> INITIALISATION x,y := <>,<>
OPERATIONS OPERATIONS
Schritt(i,ix,iy) = PRE i∈dom(K) ∧ K(i)=ix↦iy Schritt(i,ix,iy) = PRE i∈dom(K) ∧ K(i)=ix↦iy
∧ same_prefix(x^ix,y^iy) ∧ same_prefix(x^ix,y^iy)
/* kann man die beiden neuen Wörter überhaupt noch gleich machen ? */ /* kann man die beiden neuen Wörter überhaupt noch gleich machen ? */
THEN THEN
x := x ^ ix || x := x ^ ix ||
y := y ^ iy y := y ^ iy
END; END;
Lösung = SELECT x=y ∧ x ≠ [] THEN skip END Lösung = SELECT x=y ∧ x ≠ [] THEN skip END
DEFINITIONS DEFINITIONS
GOAL == (x=y ∧ x≠<>); GOAL == (x=y ∧ x≠<>);
ANIMATION_FUNCTION == {1} × x ∪ {2} × y ; ANIMATION_FUNCTION == {1} × x ∪ {2} × y ;
ANIMATION_FUNCTION_DEFAULT == {(1,(0,2)),(2,(0,3))} ∪ {1,2}×λi.(i∈dom(x)∪dom(y)|6); ANIMATION_FUNCTION_DEFAULT == {(1,(0,2)),(2,(0,3))} ∪ {1,2}×λi.(i∈dom(x)∪dom(y)|6);
ANIMATION_IMG0 == "images/sm_0.gif"; ANIMATION_IMG0 == "images/sm_0.gif";
ANIMATION_IMG1 == "images/sm_1.gif"; ANIMATION_IMG1 == "images/sm_1.gif";
ANIMATION_IMG2 == "images/sm_X.gif"; ANIMATION_IMG2 == "images/sm_X.gif";
ANIMATION_IMG3 == "images/sm_Y.gif"; ANIMATION_IMG3 == "images/sm_Y.gif";
ANIMATION_IMG6 == "images/sm_empty_box.gif"; ANIMATION_IMG6 == "images/sm_empty_box.gif";
SET_PREF_PP_SEQUENCES == TRUE; SET_PREF_PP_SEQUENCES == TRUE;
same_prefix(a,b) == LET ms BE ms=min({size(a),size(b)}) IN same_prefix(a,b) == LET ms BE ms=min({size(a),size(b)}) IN
a /|\ ms = b /|\ ms END a /|\ ms = b /|\ ms END
END END
``` ```
%% Output %% Output
Loaded machine: PostCorrespondence_MC Loaded machine: PostCorrespondence_MC
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:constants K = [ [0,1]↦[1], [0,1,0]↦[1,0,0], [1]↦[1,0] ] :constants K = [ [0,1]↦[1], [0,1,0]↦[1,0,0], [1]↦[1,0] ]
``` ```
%% 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
:exec Schritt i=3 :exec Schritt i=3
``` ```
%% Output %% Output
Executed operation: Schritt(3,[1],[1,0]) Executed operation: Schritt(3,[1],[1,0])
%% 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:0px"><img alt="2" src="images/sm_X.gif"/></td> <td style="padding:0px"><img alt="2" src="images/sm_X.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td> <td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td>
<td style="padding:0px"><img alt="6" src="images/sm_empty_box.gif"/></td> <td style="padding:0px"><img alt="6" src="images/sm_empty_box.gif"/></td>
</tr> </tr>
<tr> <tr>
<td style="padding:0px"><img alt="3" src="images/sm_Y.gif"/></td> <td style="padding:0px"><img alt="3" src="images/sm_Y.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td> <td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td> <td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td>
</tr> </tr>
</tbody></table> </tbody></table>
<Animation function visualisation> <Animation function visualisation>
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:exec Schritt i=2 :exec Schritt i=2
``` ```
%% Output %% Output
Executed operation: Schritt(2,[0,1,0],[1,0,0]) Executed operation: Schritt(2,[0,1,0],[1,0,0])
%% 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:0px"><img alt="2" src="images/sm_X.gif"/></td> <td style="padding:0px"><img alt="2" src="images/sm_X.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td> <td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td> <td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td> <td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td> <td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td>
<td style="padding:0px"><img alt="6" src="images/sm_empty_box.gif"/></td> <td style="padding:0px"><img alt="6" src="images/sm_empty_box.gif"/></td>
</tr> </tr>
<tr> <tr>
<td style="padding:0px"><img alt="3" src="images/sm_Y.gif"/></td> <td style="padding:0px"><img alt="3" src="images/sm_Y.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td> <td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td> <td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td> <td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td> <td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td> <td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td>
</tr> </tr>
</tbody></table> </tbody></table>
<Animation function visualisation> <Animation function visualisation>
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:exec Schritt i=2 :exec Schritt i=2
``` ```
%% Output %% Output
Executed operation: Schritt(2,[0,1,0],[1,0,0]) Executed operation: Schritt(2,[0,1,0],[1,0,0])
%% 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:0px"><img alt="2" src="images/sm_X.gif"/></td> <td style="padding:0px"><img alt="2" src="images/sm_X.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td> <td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td> <td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td> <td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td> <td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td> <td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td> <td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td> <td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td>
<td style="padding:0px"><img alt="6" src="images/sm_empty_box.gif"/></td> <td style="padding:0px"><img alt="6" src="images/sm_empty_box.gif"/></td>
</tr> </tr>
<tr> <tr>
<td style="padding:0px"><img alt="3" src="images/sm_Y.gif"/></td> <td style="padding:0px"><img alt="3" src="images/sm_Y.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td> <td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td> <td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td> <td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td> <td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td> <td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td> <td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td> <td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td> <td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td>
</tr> </tr>
</tbody></table> </tbody></table>
<Animation function visualisation> <Animation function visualisation>
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:exec Schritt i=1 :exec Schritt i=1
``` ```
%% Output %% Output
Executed operation: Schritt(1,[0,1],[1]) Executed operation: Schritt(1,[0,1],[1])
%% 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:0px"><img alt="2" src="images/sm_X.gif"/></td> <td style="padding:0px"><img alt="2" src="images/sm_X.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td> <td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td> <td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td> <td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td> <td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td> <td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td> <td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td> <td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td> <td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td> <td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td>
</tr> </tr>
<tr> <tr>
<td style="padding:0px"><img alt="3" src="images/sm_Y.gif"/></td> <td style="padding:0px"><img alt="3" src="images/sm_Y.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td> <td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td> <td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td> <td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td> <td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td> <td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td> <td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td> <td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td> <td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td> <td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td>
</tr> </tr>
</tbody></table> </tbody></table>
<Animation function visualisation> <Animation function visualisation>
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Wir haben eine Lösung gefunden. Wir haben eine Lösung gefunden.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:goto -1 :goto -1
``` ```
%% Output %% Output
Changed to state with index -1 Changed to state with index -1
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:constants K = [ [0,0,1]↦[0], [0,1]↦[0,1,1], [0,1]↦[1,0,1], [1,0] ↦ [0,0,1] ] :constants K = [ [0,0,1]↦[0], [0,1]↦[0,1,1], [0,1]↦[1,0,1], [1,0] ↦ [0,0,1] ]
``` ```
%% Output %% Output
Machine constants set up using operation 11: $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 12: $initialise_machine() Machine initialised using operation 1: $initialise_machine()
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:browse :browse
``` ```
%% Output %% Output
Machine: PostCorrespondence_MC Machine: PostCorrespondence_MC
Sets: (none) Sets: (none)
Constants: K, Σ Constants: K, Σ
Variables: x, y Variables: x, y
Operations: Operations:
Schritt(1,[0,0,1],[0]) Schritt(1,[0,0,1],[0])
Schritt(2,[0,1],[0,1,1]) Schritt(2,[0,1],[0,1,1])
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:exec Schritt i=2 :exec Schritt i=2
``` ```
%% Output %% Output
Executed operation: Schritt(2,[0,1],[0,1,1]) Executed operation: Schritt(2,[0,1],[0,1,1])
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:exec Schritt i=4 :exec Schritt i=4
``` ```
%% Output %% Output
Executed operation: Schritt(4,[1,0],[0,0,1]) Executed operation: Schritt(4,[1,0],[0,0,1])
%% 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:0px"><img alt="2" src="images/sm_X.gif"/></td> <td style="padding:0px"><img alt="2" src="images/sm_X.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td> <td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td> <td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td> <td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td> <td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td>
<td style="padding:0px"><img alt="6" src="images/sm_empty_box.gif"/></td> <td style="padding:0px"><img alt="6" src="images/sm_empty_box.gif"/></td>
<td style="padding:0px"><img alt="6" src="images/sm_empty_box.gif"/></td> <td style="padding:0px"><img alt="6" src="images/sm_empty_box.gif"/></td>
</tr> </tr>
<tr> <tr>
<td style="padding:0px"><img alt="3" src="images/sm_Y.gif"/></td> <td style="padding:0px"><img alt="3" src="images/sm_Y.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td> <td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td> <td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td> <td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td> <td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td> <td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td> <td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td>
</tr> </tr>
</tbody></table> </tbody></table>
<Animation function visualisation> <Animation function visualisation>
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
jetzt fehlen nur noch 64 Schritte bis zu einer Lösung. Jetzt fehlen nur noch 64 Schritte bis zu einer Lösung.
%% Cell type:code id: tags:
``` prob
:exec Schritt i=3
```
%% Output
Executed operation: Schritt(3,[0,1],[1,0,1])
%% Cell type:code id: tags:
``` prob
:exec Schritt i=4
```
%% Output
Executed operation: Schritt(4,[1,0],[0,0,1])
%% Cell type:code id: tags:
``` prob
:exec Schritt i=4
```
%% Output
Executed operation: Schritt(4,[1,0],[0,0,1])
%% Cell type:code id: tags:
``` prob
:exec Schritt i=2
```
%% Output
Executed operation: Schritt(2,[0,1],[0,1,1])
%% Cell type:code id: tags:
``` prob
:show
```
%% Output
<table style="font-family:monospace"><tbody>
<tr>
<td style="padding:0px"><img alt="2" src="images/sm_X.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td>
<td style="padding:0px"><img alt="6" src="images/sm_empty_box.gif"/></td>
<td style="padding:0px"><img alt="6" src="images/sm_empty_box.gif"/></td>
<td style="padding:0px"><img alt="6" src="images/sm_empty_box.gif"/></td>
<td style="padding:0px"><img alt="6" src="images/sm_empty_box.gif"/></td>
<td style="padding:0px"><img alt="6" src="images/sm_empty_box.gif"/></td>
<td style="padding:0px"><img alt="6" src="images/sm_empty_box.gif"/></td>
</tr>
<tr>
<td style="padding:0px"><img alt="3" src="images/sm_Y.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td>
<td style="padding:0px"><img alt="0" src="images/sm_0.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/sm_1.gif"/></td>
</tr>
</tbody></table>
<Animation function visualisation>
%% Cell type:markdown id: tags:
jetzt fehlen nur noch 60 Schritte bis zu der kürzesten Lösung.
Die gesamte Lösung ist:
Schritt(2,[0,1],[0,1,1])
Schritt(4,[1,0],[0,0,1])
Schritt(3,[0,1],[1,0,1])
Schritt(4,[1,0],[0,0,1])
Schritt(4,[1,0],[0,0,1])
Schritt(2,[0,1],[0,1,1])
Schritt(1,[0,0,1],[0])
Schritt(2,[0,1],[0,1,1])
Schritt(4,[1,0],[0,0,1])
Schritt(3,[0,1],[1,0,1])
Schritt(4,[1,0],[0,0,1])
Schritt(3,[0,1],[1,0,1])
Schritt(4,[1,0],[0,0,1])
Schritt(4,[1,0],[0,0,1])
Schritt(3,[0,1],[1,0,1])
Schritt(4,[1,0],[0,0,1])
Schritt(4,[1,0],[0,0,1])
Schritt(2,[0,1],[0,1,1])
Schritt(1,[0,0,1],[0])
Schritt(4,[1,0],[0,0,1])
Schritt(4,[1,0],[0,0,1])
Schritt(2,[0,1],[0,1,1])
Schritt(1,[0,0,1],[0])
Schritt(3,[0,1],[1,0,1])
Schritt(4,[1,0],[0,0,1])
Schritt(1,[0,0,1],[0])
Schritt(1,[0,0,1],[0])
Schritt(3,[0,1],[1,0,1])
Schritt(4,[1,0],[0,0,1])
Schritt(4,[1,0],[0,0,1])
Schritt(4,[1,0],[0,0,1])
Schritt(2,[0,1],[0,1,1])
Schritt(1,[0,0,1],[0])
Schritt(2,[0,1],[0,1,1])
Schritt(1,[0,0,1],[0])
Schritt(1,[0,0,1],[0])
Schritt(1,[0,0,1],[0])
Schritt(3,[0,1],[1,0,1])
Schritt(4,[1,0],[0,0,1])
Schritt(3,[0,1],[1,0,1])
Schritt(4,[1,0],[0,0,1])
Schritt(1,[0,0,1],[0])
Schritt(2,[0,1],[0,1,1])
Schritt(1,[0,0,1],[0])
Schritt(4,[1,0],[0,0,1])
Schritt(4,[1,0],[0,0,1])
Schritt(2,[0,1],[0,1,1])
Schritt(1,[0,0,1],[0])
Schritt(4,[1,0],[0,0,1])
Schritt(1,[0,0,1],[0])
Schritt(1,[0,0,1],[0])
Schritt(3,[0,1],[1,0,1])
Schritt(4,[1,0],[0,0,1])
Schritt(1,[0,0,1],[0])
Schritt(1,[0,0,1],[0])
Schritt(3,[0,1],[1,0,1])
Schritt(1,[0,0,1],[0])
Schritt(1,[0,0,1],[0])
Schritt(3,[0,1],[1,0,1])
Schritt(1,[0,0,1],[0])
Schritt(2,[0,1],[0,1,1])
Schritt(1,[0,0,1],[0])
Schritt(4,[1,0],[0,0,1])
Schritt(1,[0,0,1],[0])
Schritt(1,[0,0,1],[0])
Schritt(3,[0,1],[1,0,1])
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
## Kodierung des Halteproblems als MPCP Problem ## Kodierung des Halteproblems als MPCP Problem
Folgende B Maschine kodiert das Halteproblem einer Turingmaschine als MPCP Problem. Folgende B Maschine kodiert das Halteproblem einer Turingmaschine als MPCP Problem.
Der erste Schritt zu einer Lösung wird in der Initialisierung kodiert; dort wir erzwungen, dass wir das erste Paar aus dem Skript $(\#,\# z_0 w)$ benutzen. Der erste Schritt zu einer Lösung wird in der Initialisierung kodiert; dort wir erzwungen, dass wir das erste Paar aus dem Skript $(\#,\# z_0 w)$ benutzen.
Die Turing Maschine hat 3 Zustände: z0,z1,z2. Die Turing Maschine hat 3 Zustände: z0,z1,z2.
z2 ist der Endzustand. z2 ist der Endzustand.
z0 akzeptiert a and wechselt bei einem b zu z1, z1 akzeptiert b's und geht zu z2 bei einem Blank. z0 akzeptiert a and wechselt bei einem b zu z1, z1 akzeptiert b's und geht zu z2 bei einem Blank.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
::load ::load
MACHINE PostCorrespondence_Turing_MC MACHINE PostCorrespondence_Turing_MC
/* The Turing machine has 3 states: z0,z1,z2; z2 is Final /* The Turing machine has 3 states: z0,z1,z2; z2 is Final
z0 accepts a and goes to z1 via b; z1 accepts b and goes to z2 via Blank z0 accepts a and goes to z1 via b; z1 accepts b and goes to z2 via Blank
*/ */
SETS SETS
Σ={a,b,Blank,z0,z1,z2,Hash} Σ={a,b,Blank,z0,z1,z2,Hash}
CONSTANTS K CONSTANTS K
PROPERTIES PROPERTIES
K = [ [a]↦[a], [b]↦[b], [Hash] ↦ [Hash] /* Copy Regeln */ K = [ [a]↦[a], [b]↦[b], [Hash] ↦ [Hash] /* Copy Regeln */
, ,
[z0,a] ↦ [a,z0], [z0,b] ↦ [b,z1], [z0,a] ↦ [a,z0], [z0,b] ↦ [b,z1],
[z1,b] ↦ [b,z1], [z1,Hash] ↦ [z2,Hash] /* Transitionen der TM */ [z1,b] ↦ [b,z1], [z1,Hash] ↦ [z2,Hash] /* Transitionen der TM */
, ,
[a,z2] ↦ [z2], [b,z2] ↦ [z2] /* Löschregeln für Endzustände */ [a,z2] ↦ [z2], [b,z2] ↦ [z2] /* Löschregeln für Endzustände */
, ,
[z2,Hash,Hash] |-> [Hash] /* Abschlussregeln für Endzustände */ [z2,Hash,Hash] |-> [Hash] /* Abschlussregeln für Endzustände */
] ]
VARIABLES x,y VARIABLES x,y
INVARIANT INVARIANT
x∈seq(Σ) ∧ y∈seq(Σ) x∈seq(Σ) ∧ y∈seq(Σ)
INITIALISATION x,y := [Hash],[Hash,z0,a,b,Hash] /* Start configuration */ INITIALISATION x,y := [Hash],[Hash,z0,a,b,Hash] /* Start configuration */
OPERATIONS OPERATIONS
Schritt(i,ix,iy) = PRE i∈dom(K) ∧ K(i)=ix↦iy Schritt(i,ix,iy) = PRE i∈dom(K) ∧ K(i)=ix↦iy
∧ same_prefix(x^ix,y^iy) ∧ same_prefix(x^ix,y^iy)
/* kann man die beiden neuen Wörter überhaupt noch gleich machen ? */ /* kann man die beiden neuen Wörter überhaupt noch gleich machen ? */
THEN THEN
x := x ^ ix || x := x ^ ix ||
y := y ^ iy y := y ^ iy
END; END;
Lösung = SELECT x=y ∧ x ≠ [] THEN skip END Lösung = SELECT x=y ∧ x ≠ [] THEN skip END
DEFINITIONS DEFINITIONS
GOAL == (x=y ∧ x≠<>); GOAL == (x=y ∧ x≠<>);
ANIMATION_FUNCTION == {1}*x \/ {2} * y ; ANIMATION_FUNCTION == {1}*x \/ {2} * y ;
ANIMATION_FUNCTION_DEFAULT == {(1,0,"x"),(2,0,"y")}; ANIMATION_FUNCTION_DEFAULT == {(1,0,"x"),(2,0,"y")};
SET_PREF_MAX_OPERATIONS == 20; SET_PREF_MAX_OPERATIONS == 20;
SET_PREF_PP_SEQUENCES == TRUE; SET_PREF_PP_SEQUENCES == TRUE;
same_prefix(a,b) == LET ms BE ms=min({size(a),size(b)}) IN same_prefix(a,b) == LET ms BE ms=min({size(a),size(b)}) IN
a /|\ ms = b /|\ ms END a /|\ ms = b /|\ ms END
END END
``` ```
%% Output %% Output
Loaded machine: PostCorrespondence_Turing_MC Loaded machine: PostCorrespondence_Turing_MC
%% 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">x</td> <td style="padding:10px">x</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
<td style="padding:0px"></td> <td style="padding:0px"></td>
<td style="padding:0px"></td> <td style="padding:0px"></td>
<td style="padding:0px"></td> <td style="padding:0px"></td>
<td style="padding:0px"></td> <td style="padding:0px"></td>
</tr> </tr>
<tr> <tr>
<td style="padding:10px">y</td> <td style="padding:10px">y</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
<td style="padding:10px">z0</td> <td style="padding:10px">z0</td>
<td style="padding:10px">a</td> <td style="padding:10px">a</td>
<td style="padding:10px">b</td> <td style="padding:10px">b</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
</tr> </tr>
</tbody></table> </tbody></table>
<Animation function visualisation> <Animation function visualisation>
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:browse :browse
``` ```
%% Output %% Output
Machine: PostCorrespondence_Turing_MC Machine: PostCorrespondence_Turing_MC
Sets: Σ Sets: Σ
Constants: K Constants: K
Variables: x, y Variables: x, y
Operations: Operations:
Schritt(4,[z0,a],[a,z0]) Schritt(4,[z0,a],[a,z0])
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:exec Schritt i=4 :exec Schritt i=4
``` ```
%% Output %% Output
Executed operation: Schritt(4,[z0,a],[a,z0]) Executed operation: Schritt(4,[z0,a],[a,z0])
%% 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">x</td> <td style="padding:10px">x</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
<td style="padding:10px">z0</td> <td style="padding:10px">z0</td>
<td style="padding:10px">a</td> <td style="padding:10px">a</td>
<td style="padding:0px"></td> <td style="padding:0px"></td>
<td style="padding:0px"></td> <td style="padding:0px"></td>
<td style="padding:0px"></td> <td style="padding:0px"></td>
<td style="padding:0px"></td> <td style="padding:0px"></td>
</tr> </tr>
<tr> <tr>
<td style="padding:10px">y</td> <td style="padding:10px">y</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
<td style="padding:10px">z0</td> <td style="padding:10px">z0</td>
<td style="padding:10px">a</td> <td style="padding:10px">a</td>
<td style="padding:10px">b</td> <td style="padding:10px">b</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
<td style="padding:10px">a</td> <td style="padding:10px">a</td>
<td style="padding:10px">z0</td> <td style="padding:10px">z0</td>
</tr> </tr>
</tbody></table> </tbody></table>
<Animation function visualisation> <Animation function visualisation>
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Wir haben jetzt die Zuständsänderung ausgeführt; der neue Zustand befindet sich in der y-Reihe. Hier ist der neue Zustand gleich dem alten Zustand. Wir haben jetzt die Zuständsänderung ausgeführt; der neue Zustand befindet sich in der y-Reihe. Hier ist der neue Zustand gleich dem alten Zustand.
Jetzt müssen noch die Kopierregeln angewendet werden um den unveränderten Bandinhalt zu kopieren. Jetzt müssen noch die Kopierregeln angewendet werden um den unveränderten Bandinhalt zu kopieren.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:browse :browse
``` ```
%% Output %% Output
Machine: PostCorrespondence_Turing_MC Machine: PostCorrespondence_Turing_MC
Sets: Σ Sets: Σ
Constants: K Constants: K
Variables: x, y Variables: x, y
Operations: Operations:
Schritt(2,[b],[b]) Schritt(2,[b],[b])
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:exec Schritt i=2 :exec Schritt i=2
``` ```
%% Output %% Output
Executed operation: Schritt(2,[b],[b]) Executed operation: Schritt(2,[b],[b])
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:browse :browse
``` ```
%% Output %% Output
Machine: PostCorrespondence_Turing_MC Machine: PostCorrespondence_Turing_MC
Sets: Σ Sets: Σ
Constants: K Constants: K
Variables: x, y Variables: x, y
Operations: Operations:
Schritt(3,[Hash],[Hash]) Schritt(3,[Hash],[Hash])
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:exec Schritt i=3 :exec Schritt i=3
``` ```
%% Output %% Output
Executed operation: Schritt(3,[Hash],[Hash]) Executed operation: Schritt(3,[Hash],[Hash])
%% 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">x</td> <td style="padding:10px">x</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
<td style="padding:10px">z0</td> <td style="padding:10px">z0</td>
<td style="padding:10px">a</td> <td style="padding:10px">a</td>
<td style="padding:10px">b</td> <td style="padding:10px">b</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
<td style="padding:0px"></td> <td style="padding:0px"></td>
<td style="padding:0px"></td> <td style="padding:0px"></td>
<td style="padding:0px"></td> <td style="padding:0px"></td>
<td style="padding:0px"></td> <td style="padding:0px"></td>
</tr> </tr>
<tr> <tr>
<td style="padding:10px">y</td> <td style="padding:10px">y</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
<td style="padding:10px">z0</td> <td style="padding:10px">z0</td>
<td style="padding:10px">a</td> <td style="padding:10px">a</td>
<td style="padding:10px">b</td> <td style="padding:10px">b</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
<td style="padding:10px">a</td> <td style="padding:10px">a</td>
<td style="padding:10px">z0</td> <td style="padding:10px">z0</td>
<td style="padding:10px">b</td> <td style="padding:10px">b</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
</tr> </tr>
</tbody></table> </tbody></table>
<Animation function visualisation> <Animation function visualisation>
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:browse :browse
``` ```
%% Output %% Output
Machine: PostCorrespondence_Turing_MC Machine: PostCorrespondence_Turing_MC
Sets: Σ Sets: Σ
Constants: K Constants: K
Variables: x, y Variables: x, y
Operations: Operations:
Schritt(1,[a],[a]) Schritt(1,[a],[a])
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Jetzt muss noch der Bandinhalt links vom Schreibkopf kopiert werden: Jetzt muss noch der Bandinhalt links vom Schreibkopf kopiert werden:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:exec Schritt i=1 :exec Schritt i=1
``` ```
%% Output %% Output
Executed operation: Schritt(1,[a],[a]) Executed operation: Schritt(1,[a],[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">x</td> <td style="padding:10px">x</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
<td style="padding:10px">z0</td> <td style="padding:10px">z0</td>
<td style="padding:10px">a</td> <td style="padding:10px">a</td>
<td style="padding:10px">b</td> <td style="padding:10px">b</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
<td style="padding:10px">a</td> <td style="padding:10px">a</td>
<td style="padding:0px"></td> <td style="padding:0px"></td>
<td style="padding:0px"></td> <td style="padding:0px"></td>
<td style="padding:0px"></td> <td style="padding:0px"></td>
<td style="padding:0px"></td> <td style="padding:0px"></td>
</tr> </tr>
<tr> <tr>
<td style="padding:10px">y</td> <td style="padding:10px">y</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
<td style="padding:10px">z0</td> <td style="padding:10px">z0</td>
<td style="padding:10px">a</td> <td style="padding:10px">a</td>
<td style="padding:10px">b</td> <td style="padding:10px">b</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
<td style="padding:10px">a</td> <td style="padding:10px">a</td>
<td style="padding:10px">z0</td> <td style="padding:10px">z0</td>
<td style="padding:10px">b</td> <td style="padding:10px">b</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
<td style="padding:10px">a</td> <td style="padding:10px">a</td>
</tr> </tr>
</tbody></table> </tbody></table>
<Animation function visualisation> <Animation function visualisation>
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:browse :browse
``` ```
%% Output %% Output
Machine: PostCorrespondence_Turing_MC Machine: PostCorrespondence_Turing_MC
Sets: Σ Sets: Σ
Constants: K Constants: K
Variables: x, y Variables: x, y
Operations: Operations:
Schritt(5,[z0,b],[b,z1]) Schritt(5,[z0,b],[b,z1])
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:exec Schritt i=5 :exec Schritt i=5
``` ```
%% Output %% Output
Executed operation: Schritt(5,[z0,b],[b,z1]) Executed operation: Schritt(5,[z0,b],[b,z1])
%% 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">x</td> <td style="padding:10px">x</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
<td style="padding:10px">z0</td> <td style="padding:10px">z0</td>
<td style="padding:10px">a</td> <td style="padding:10px">a</td>
<td style="padding:10px">b</td> <td style="padding:10px">b</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
<td style="padding:10px">a</td> <td style="padding:10px">a</td>
<td style="padding:10px">z0</td> <td style="padding:10px">z0</td>
<td style="padding:10px">b</td> <td style="padding:10px">b</td>
<td style="padding:0px"></td> <td style="padding:0px"></td>
<td style="padding:0px"></td> <td style="padding:0px"></td>
<td style="padding:0px"></td> <td style="padding:0px"></td>
<td style="padding:0px"></td> <td style="padding:0px"></td>
</tr> </tr>
<tr> <tr>
<td style="padding:10px">y</td> <td style="padding:10px">y</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
<td style="padding:10px">z0</td> <td style="padding:10px">z0</td>
<td style="padding:10px">a</td> <td style="padding:10px">a</td>
<td style="padding:10px">b</td> <td style="padding:10px">b</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
<td style="padding:10px">a</td> <td style="padding:10px">a</td>
<td style="padding:10px">z0</td> <td style="padding:10px">z0</td>
<td style="padding:10px">b</td> <td style="padding:10px">b</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
<td style="padding:10px">a</td> <td style="padding:10px">a</td>
<td style="padding:10px">b</td> <td style="padding:10px">b</td>
<td style="padding:10px">z1</td> <td style="padding:10px">z1</td>
</tr> </tr>
</tbody></table> </tbody></table>
<Animation function visualisation> <Animation function visualisation>
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Jetzt haben wir den Zustand gewechselt; wir müssen wieder kopieren. Jetzt haben wir den Zustand gewechselt; wir müssen wieder kopieren.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:exec Schritt :exec Schritt
``` ```
%% Output %% Output
Executed operation: Schritt(3,[Hash],[Hash]) Executed operation: Schritt(3,[Hash],[Hash])
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:exec Schritt :exec Schritt
``` ```
%% Output %% Output
Executed operation: Schritt(1,[a],[a]) Executed operation: Schritt(1,[a],[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">x</td> <td style="padding:10px">x</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
<td style="padding:10px">z0</td> <td style="padding:10px">z0</td>
<td style="padding:10px">a</td> <td style="padding:10px">a</td>
<td style="padding:10px">b</td> <td style="padding:10px">b</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
<td style="padding:10px">a</td> <td style="padding:10px">a</td>
<td style="padding:10px">z0</td> <td style="padding:10px">z0</td>
<td style="padding:10px">b</td> <td style="padding:10px">b</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
<td style="padding:10px">a</td> <td style="padding:10px">a</td>
<td style="padding:0px"></td> <td style="padding:0px"></td>
<td style="padding:0px"></td> <td style="padding:0px"></td>
<td style="padding:0px"></td> <td style="padding:0px"></td>
<td style="padding:0px"></td> <td style="padding:0px"></td>
</tr> </tr>
<tr> <tr>
<td style="padding:10px">y</td> <td style="padding:10px">y</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
<td style="padding:10px">z0</td> <td style="padding:10px">z0</td>
<td style="padding:10px">a</td> <td style="padding:10px">a</td>
<td style="padding:10px">b</td> <td style="padding:10px">b</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
<td style="padding:10px">a</td> <td style="padding:10px">a</td>
<td style="padding:10px">z0</td> <td style="padding:10px">z0</td>
<td style="padding:10px">b</td> <td style="padding:10px">b</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
<td style="padding:10px">a</td> <td style="padding:10px">a</td>
<td style="padding:10px">b</td> <td style="padding:10px">b</td>
<td style="padding:10px">z1</td> <td style="padding:10px">z1</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
<td style="padding:10px">a</td> <td style="padding:10px">a</td>
</tr> </tr>
</tbody></table> </tbody></table>
<Animation function visualisation> <Animation function visualisation>
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:exec Schritt :exec Schritt
``` ```
%% Output %% Output
Executed operation: Schritt(2,[b],[b]) Executed operation: Schritt(2,[b],[b])
%% 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">x</td> <td style="padding:10px">x</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
<td style="padding:10px">z0</td> <td style="padding:10px">z0</td>
<td style="padding:10px">a</td> <td style="padding:10px">a</td>
<td style="padding:10px">b</td> <td style="padding:10px">b</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
<td style="padding:10px">a</td> <td style="padding:10px">a</td>
<td style="padding:10px">z0</td> <td style="padding:10px">z0</td>
<td style="padding:10px">b</td> <td style="padding:10px">b</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
<td style="padding:10px">a</td> <td style="padding:10px">a</td>
<td style="padding:10px">b</td> <td style="padding:10px">b</td>
<td style="padding:0px"></td> <td style="padding:0px"></td>
<td style="padding:0px"></td> <td style="padding:0px"></td>
<td style="padding:0px"></td> <td style="padding:0px"></td>
<td style="padding:0px"></td> <td style="padding:0px"></td>
</tr> </tr>
<tr> <tr>
<td style="padding:10px">y</td> <td style="padding:10px">y</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
<td style="padding:10px">z0</td> <td style="padding:10px">z0</td>
<td style="padding:10px">a</td> <td style="padding:10px">a</td>
<td style="padding:10px">b</td> <td style="padding:10px">b</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
<td style="padding:10px">a</td> <td style="padding:10px">a</td>
<td style="padding:10px">z0</td> <td style="padding:10px">z0</td>
<td style="padding:10px">b</td> <td style="padding:10px">b</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
<td style="padding:10px">a</td> <td style="padding:10px">a</td>
<td style="padding:10px">b</td> <td style="padding:10px">b</td>
<td style="padding:10px">z1</td> <td style="padding:10px">z1</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
<td style="padding:10px">a</td> <td style="padding:10px">a</td>
<td style="padding:10px">b</td> <td style="padding:10px">b</td>
</tr> </tr>
</tbody></table> </tbody></table>
<Animation function visualisation> <Animation function visualisation>
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:browse :browse
``` ```
%% Output %% Output
Machine: PostCorrespondence_Turing_MC Machine: PostCorrespondence_Turing_MC
Sets: Σ Sets: Σ
Constants: K Constants: K
Variables: x, y Variables: x, y
Operations: Operations:
Schritt(7,[z1,Hash],[z2,Hash]) Schritt(7,[z1,Hash],[z2,Hash])
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:exec Schritt i=7 :exec Schritt i=7
``` ```
%% Output %% Output
Executed operation: Schritt(7,[z1,Hash],[z2,Hash]) Executed operation: Schritt(7,[z1,Hash],[z2,Hash])
%% 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">x</td> <td style="padding:10px">x</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
<td style="padding:10px">z0</td> <td style="padding:10px">z0</td>
<td style="padding:10px">a</td> <td style="padding:10px">a</td>
<td style="padding:10px">b</td> <td style="padding:10px">b</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
<td style="padding:10px">a</td> <td style="padding:10px">a</td>
<td style="padding:10px">z0</td> <td style="padding:10px">z0</td>
<td style="padding:10px">b</td> <td style="padding:10px">b</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
<td style="padding:10px">a</td> <td style="padding:10px">a</td>
<td style="padding:10px">b</td> <td style="padding:10px">b</td>
<td style="padding:10px">z1</td> <td style="padding:10px">z1</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
<td style="padding:0px"></td> <td style="padding:0px"></td>
<td style="padding:0px"></td> <td style="padding:0px"></td>
<td style="padding:0px"></td> <td style="padding:0px"></td>
<td style="padding:0px"></td> <td style="padding:0px"></td>
</tr> </tr>
<tr> <tr>
<td style="padding:10px">y</td> <td style="padding:10px">y</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
<td style="padding:10px">z0</td> <td style="padding:10px">z0</td>
<td style="padding:10px">a</td> <td style="padding:10px">a</td>
<td style="padding:10px">b</td> <td style="padding:10px">b</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
<td style="padding:10px">a</td> <td style="padding:10px">a</td>
<td style="padding:10px">z0</td> <td style="padding:10px">z0</td>
<td style="padding:10px">b</td> <td style="padding:10px">b</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
<td style="padding:10px">a</td> <td style="padding:10px">a</td>
<td style="padding:10px">b</td> <td style="padding:10px">b</td>
<td style="padding:10px">z1</td> <td style="padding:10px">z1</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
<td style="padding:10px">a</td> <td style="padding:10px">a</td>
<td style="padding:10px">b</td> <td style="padding:10px">b</td>
<td style="padding:10px">z2</td> <td style="padding:10px">z2</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
</tr> </tr>
</tbody></table> </tbody></table>
<Animation function visualisation> <Animation function visualisation>
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Jetzt haben wir in den Endzustand z2 gewechselt. Bald greifen die Löschregeln um eine Lösung zu produzieren. Jetzt haben wir in den Endzustand z2 gewechselt. Bald greifen die Löschregeln um eine Lösung zu produzieren.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:browse :browse
``` ```
%% Output %% Output
Machine: PostCorrespondence_Turing_MC Machine: PostCorrespondence_Turing_MC
Sets: Σ Sets: Σ
Constants: K Constants: K
Variables: x, y Variables: x, y
Operations: Operations:
Schritt(1,[a],[a]) Schritt(1,[a],[a])
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:exec Schritt :exec Schritt
``` ```
%% Output %% Output
Executed operation: Schritt(1,[a],[a]) Executed operation: Schritt(1,[a],[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">x</td> <td style="padding:10px">x</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
<td style="padding:10px">z0</td> <td style="padding:10px">z0</td>
<td style="padding:10px">a</td> <td style="padding:10px">a</td>
<td style="padding:10px">b</td> <td style="padding:10px">b</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
<td style="padding:10px">a</td> <td style="padding:10px">a</td>
<td style="padding:10px">z0</td> <td style="padding:10px">z0</td>
<td style="padding:10px">b</td> <td style="padding:10px">b</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
<td style="padding:10px">a</td> <td style="padding:10px">a</td>
<td style="padding:10px">b</td> <td style="padding:10px">b</td>
<td style="padding:10px">z1</td> <td style="padding:10px">z1</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
<td style="padding:10px">a</td> <td style="padding:10px">a</td>
<td style="padding:0px"></td> <td style="padding:0px"></td>
<td style="padding:0px"></td> <td style="padding:0px"></td>
<td style="padding:0px"></td> <td style="padding:0px"></td>
<td style="padding:0px"></td> <td style="padding:0px"></td>
</tr> </tr>
<tr> <tr>
<td style="padding:10px">y</td> <td style="padding:10px">y</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
<td style="padding:10px">z0</td> <td style="padding:10px">z0</td>
<td style="padding:10px">a</td> <td style="padding:10px">a</td>
<td style="padding:10px">b</td> <td style="padding:10px">b</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
<td style="padding:10px">a</td> <td style="padding:10px">a</td>
<td style="padding:10px">z0</td> <td style="padding:10px">z0</td>
<td style="padding:10px">b</td> <td style="padding:10px">b</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
<td style="padding:10px">a</td> <td style="padding:10px">a</td>
<td style="padding:10px">b</td> <td style="padding:10px">b</td>
<td style="padding:10px">z1</td> <td style="padding:10px">z1</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
<td style="padding:10px">a</td> <td style="padding:10px">a</td>
<td style="padding:10px">b</td> <td style="padding:10px">b</td>
<td style="padding:10px">z2</td> <td style="padding:10px">z2</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
<td style="padding:10px">a</td> <td style="padding:10px">a</td>
</tr> </tr>
</tbody></table> </tbody></table>
<Animation function visualisation> <Animation function visualisation>
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:browse :browse
``` ```
%% Output %% Output
Machine: PostCorrespondence_Turing_MC Machine: PostCorrespondence_Turing_MC
Sets: Σ Sets: Σ
Constants: K Constants: K
Variables: x, y Variables: x, y
Operations: Operations:
Schritt(2,[b],[b]) Schritt(2,[b],[b])
Schritt(9,[b,z2],[z2]) Schritt(9,[b,z2],[z2])
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Jetzt greift die Löschregel 9. Jetzt greift die Löschregel 9.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:exec Schritt i=9 :exec Schritt i=9
``` ```
%% Output %% Output
Executed operation: Schritt(9,[b,z2],[z2]) Executed operation: Schritt(9,[b,z2],[z2])
%% 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">x</td> <td style="padding:10px">x</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
<td style="padding:10px">z0</td> <td style="padding:10px">z0</td>
<td style="padding:10px">a</td> <td style="padding:10px">a</td>
<td style="padding:10px">b</td> <td style="padding:10px">b</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
<td style="padding:10px">a</td> <td style="padding:10px">a</td>
<td style="padding:10px">z0</td> <td style="padding:10px">z0</td>
<td style="padding:10px">b</td> <td style="padding:10px">b</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
<td style="padding:10px">a</td> <td style="padding:10px">a</td>
<td style="padding:10px">b</td> <td style="padding:10px">b</td>
<td style="padding:10px">z1</td> <td style="padding:10px">z1</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
<td style="padding:10px">a</td> <td style="padding:10px">a</td>
<td style="padding:10px">b</td> <td style="padding:10px">b</td>
<td style="padding:10px">z2</td> <td style="padding:10px">z2</td>
<td style="padding:0px"></td> <td style="padding:0px"></td>
<td style="padding:0px"></td> <td style="padding:0px"></td>
<td style="padding:0px"></td> <td style="padding:0px"></td>
</tr> </tr>
<tr> <tr>
<td style="padding:10px">y</td> <td style="padding:10px">y</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
<td style="padding:10px">z0</td> <td style="padding:10px">z0</td>
<td style="padding:10px">a</td> <td style="padding:10px">a</td>
<td style="padding:10px">b</td> <td style="padding:10px">b</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
<td style="padding:10px">a</td> <td style="padding:10px">a</td>
<td style="padding:10px">z0</td> <td style="padding:10px">z0</td>
<td style="padding:10px">b</td> <td style="padding:10px">b</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
<td style="padding:10px">a</td> <td style="padding:10px">a</td>
<td style="padding:10px">b</td> <td style="padding:10px">b</td>
<td style="padding:10px">z1</td> <td style="padding:10px">z1</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
<td style="padding:10px">a</td> <td style="padding:10px">a</td>
<td style="padding:10px">b</td> <td style="padding:10px">b</td>
<td style="padding:10px">z2</td> <td style="padding:10px">z2</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
<td style="padding:10px">a</td> <td style="padding:10px">a</td>
<td style="padding:10px">z2</td> <td style="padding:10px">z2</td>
</tr> </tr>
</tbody></table> </tbody></table>
<Animation function visualisation> <Animation function visualisation>
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:browse :browse
``` ```
%% Output %% Output
Machine: PostCorrespondence_Turing_MC Machine: PostCorrespondence_Turing_MC
Sets: Σ Sets: Σ
Constants: K Constants: K
Variables: x, y Variables: x, y
Operations: Operations:
Schritt(3,[Hash],[Hash]) Schritt(3,[Hash],[Hash])
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:exec Schritt :exec Schritt
``` ```
%% Output %% Output
Executed operation: Schritt(3,[Hash],[Hash]) Executed operation: Schritt(3,[Hash],[Hash])
%% 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">x</td> <td style="padding:10px">x</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
<td style="padding:10px">z0</td> <td style="padding:10px">z0</td>
<td style="padding:10px">a</td> <td style="padding:10px">a</td>
<td style="padding:10px">b</td> <td style="padding:10px">b</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
<td style="padding:10px">a</td> <td style="padding:10px">a</td>
<td style="padding:10px">z0</td> <td style="padding:10px">z0</td>
<td style="padding:10px">b</td> <td style="padding:10px">b</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
<td style="padding:10px">a</td> <td style="padding:10px">a</td>
<td style="padding:10px">b</td> <td style="padding:10px">b</td>
<td style="padding:10px">z1</td> <td style="padding:10px">z1</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
<td style="padding:10px">a</td> <td style="padding:10px">a</td>
<td style="padding:10px">b</td> <td style="padding:10px">b</td>
<td style="padding:10px">z2</td> <td style="padding:10px">z2</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
<td style="padding:0px"></td> <td style="padding:0px"></td>
<td style="padding:0px"></td> <td style="padding:0px"></td>
<td style="padding:0px"></td> <td style="padding:0px"></td>
</tr> </tr>
<tr> <tr>
<td style="padding:10px">y</td> <td style="padding:10px">y</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
<td style="padding:10px">z0</td> <td style="padding:10px">z0</td>
<td style="padding:10px">a</td> <td style="padding:10px">a</td>
<td style="padding:10px">b</td> <td style="padding:10px">b</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
<td style="padding:10px">a</td> <td style="padding:10px">a</td>
<td style="padding:10px">z0</td> <td style="padding:10px">z0</td>
<td style="padding:10px">b</td> <td style="padding:10px">b</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
<td style="padding:10px">a</td> <td style="padding:10px">a</td>
<td style="padding:10px">b</td> <td style="padding:10px">b</td>
<td style="padding:10px">z1</td> <td style="padding:10px">z1</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
<td style="padding:10px">a</td> <td style="padding:10px">a</td>
<td style="padding:10px">b</td> <td style="padding:10px">b</td>
<td style="padding:10px">z2</td> <td style="padding:10px">z2</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
<td style="padding:10px">a</td> <td style="padding:10px">a</td>
<td style="padding:10px">z2</td> <td style="padding:10px">z2</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
</tr> </tr>
</tbody></table> </tbody></table>
<Animation function visualisation> <Animation function visualisation>
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:browse :browse
``` ```
%% Output %% Output
Machine: PostCorrespondence_Turing_MC Machine: PostCorrespondence_Turing_MC
Sets: Σ Sets: Σ
Constants: K Constants: K
Variables: x, y Variables: x, y
Operations: Operations:
Schritt(1,[a],[a]) Schritt(1,[a],[a])
Schritt(8,[a,z2],[z2]) Schritt(8,[a,z2],[z2])
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Wir können wieder ein Symbol löschen. Wir können wieder ein Symbol löschen.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:exec Schritt i=8 :exec Schritt i=8
``` ```
%% Output %% Output
Executed operation: Schritt(8,[a,z2],[z2]) Executed operation: Schritt(8,[a,z2],[z2])
%% 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">x</td> <td style="padding:10px">x</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
<td style="padding:10px">z0</td> <td style="padding:10px">z0</td>
<td style="padding:10px">a</td> <td style="padding:10px">a</td>
<td style="padding:10px">b</td> <td style="padding:10px">b</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
<td style="padding:10px">a</td> <td style="padding:10px">a</td>
<td style="padding:10px">z0</td> <td style="padding:10px">z0</td>
<td style="padding:10px">b</td> <td style="padding:10px">b</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
<td style="padding:10px">a</td> <td style="padding:10px">a</td>
<td style="padding:10px">b</td> <td style="padding:10px">b</td>
<td style="padding:10px">z1</td> <td style="padding:10px">z1</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
<td style="padding:10px">a</td> <td style="padding:10px">a</td>
<td style="padding:10px">b</td> <td style="padding:10px">b</td>
<td style="padding:10px">z2</td> <td style="padding:10px">z2</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
<td style="padding:10px">a</td> <td style="padding:10px">a</td>
<td style="padding:10px">z2</td> <td style="padding:10px">z2</td>
<td style="padding:0px"></td> <td style="padding:0px"></td>
<td style="padding:0px"></td> <td style="padding:0px"></td>
</tr> </tr>
<tr> <tr>
<td style="padding:10px">y</td> <td style="padding:10px">y</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
<td style="padding:10px">z0</td> <td style="padding:10px">z0</td>
<td style="padding:10px">a</td> <td style="padding:10px">a</td>
<td style="padding:10px">b</td> <td style="padding:10px">b</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
<td style="padding:10px">a</td> <td style="padding:10px">a</td>
<td style="padding:10px">z0</td> <td style="padding:10px">z0</td>
<td style="padding:10px">b</td> <td style="padding:10px">b</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
<td style="padding:10px">a</td> <td style="padding:10px">a</td>
<td style="padding:10px">b</td> <td style="padding:10px">b</td>
<td style="padding:10px">z1</td> <td style="padding:10px">z1</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
<td style="padding:10px">a</td> <td style="padding:10px">a</td>
<td style="padding:10px">b</td> <td style="padding:10px">b</td>
<td style="padding:10px">z2</td> <td style="padding:10px">z2</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
<td style="padding:10px">a</td> <td style="padding:10px">a</td>
<td style="padding:10px">z2</td> <td style="padding:10px">z2</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
<td style="padding:10px">z2</td> <td style="padding:10px">z2</td>
</tr> </tr>
</tbody></table> </tbody></table>
<Animation function visualisation> <Animation function visualisation>
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:exec Schritt :exec Schritt
``` ```
%% Output %% Output
Executed operation: Schritt(3,[Hash],[Hash]) Executed operation: Schritt(3,[Hash],[Hash])
%% 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">x</td> <td style="padding:10px">x</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
<td style="padding:10px">z0</td> <td style="padding:10px">z0</td>
<td style="padding:10px">a</td> <td style="padding:10px">a</td>
<td style="padding:10px">b</td> <td style="padding:10px">b</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
<td style="padding:10px">a</td> <td style="padding:10px">a</td>
<td style="padding:10px">z0</td> <td style="padding:10px">z0</td>
<td style="padding:10px">b</td> <td style="padding:10px">b</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
<td style="padding:10px">a</td> <td style="padding:10px">a</td>
<td style="padding:10px">b</td> <td style="padding:10px">b</td>
<td style="padding:10px">z1</td> <td style="padding:10px">z1</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
<td style="padding:10px">a</td> <td style="padding:10px">a</td>
<td style="padding:10px">b</td> <td style="padding:10px">b</td>
<td style="padding:10px">z2</td> <td style="padding:10px">z2</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
<td style="padding:10px">a</td> <td style="padding:10px">a</td>
<td style="padding:10px">z2</td> <td style="padding:10px">z2</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
<td style="padding:0px"></td> <td style="padding:0px"></td>
<td style="padding:0px"></td> <td style="padding:0px"></td>
</tr> </tr>
<tr> <tr>
<td style="padding:10px">y</td> <td style="padding:10px">y</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
<td style="padding:10px">z0</td> <td style="padding:10px">z0</td>
<td style="padding:10px">a</td> <td style="padding:10px">a</td>
<td style="padding:10px">b</td> <td style="padding:10px">b</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
<td style="padding:10px">a</td> <td style="padding:10px">a</td>
<td style="padding:10px">z0</td> <td style="padding:10px">z0</td>
<td style="padding:10px">b</td> <td style="padding:10px">b</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
<td style="padding:10px">a</td> <td style="padding:10px">a</td>
<td style="padding:10px">b</td> <td style="padding:10px">b</td>
<td style="padding:10px">z1</td> <td style="padding:10px">z1</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
<td style="padding:10px">a</td> <td style="padding:10px">a</td>
<td style="padding:10px">b</td> <td style="padding:10px">b</td>
<td style="padding:10px">z2</td> <td style="padding:10px">z2</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
<td style="padding:10px">a</td> <td style="padding:10px">a</td>
<td style="padding:10px">z2</td> <td style="padding:10px">z2</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
<td style="padding:10px">z2</td> <td style="padding:10px">z2</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
</tr> </tr>
</tbody></table> </tbody></table>
<Animation function visualisation> <Animation function visualisation>
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:browse :browse
``` ```
%% Output %% Output
Machine: PostCorrespondence_Turing_MC Machine: PostCorrespondence_Turing_MC
Sets: Σ Sets: Σ
Constants: K Constants: K
Variables: x, y Variables: x, y
Operations: Operations:
Schritt(10,[z2,Hash,Hash],[Hash]) Schritt(10,[z2,Hash,Hash],[Hash])
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Jetzt greift die Abschlussregel um endlich eine Lösung zu finden. Jetzt greift die Abschlussregel um endlich eine Lösung zu finden.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:exec Schritt i=10 :exec Schritt i=10
``` ```
%% Output %% Output
Executed operation: Schritt(10,[z2,Hash,Hash],[Hash]) Executed operation: Schritt(10,[z2,Hash,Hash],[Hash])
%% 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">x</td> <td style="padding:10px">x</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
<td style="padding:10px">z0</td> <td style="padding:10px">z0</td>
<td style="padding:10px">a</td> <td style="padding:10px">a</td>
<td style="padding:10px">b</td> <td style="padding:10px">b</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
<td style="padding:10px">a</td> <td style="padding:10px">a</td>
<td style="padding:10px">z0</td> <td style="padding:10px">z0</td>
<td style="padding:10px">b</td> <td style="padding:10px">b</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
<td style="padding:10px">a</td> <td style="padding:10px">a</td>
<td style="padding:10px">b</td> <td style="padding:10px">b</td>
<td style="padding:10px">z1</td> <td style="padding:10px">z1</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
<td style="padding:10px">a</td> <td style="padding:10px">a</td>
<td style="padding:10px">b</td> <td style="padding:10px">b</td>
<td style="padding:10px">z2</td> <td style="padding:10px">z2</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
<td style="padding:10px">a</td> <td style="padding:10px">a</td>
<td style="padding:10px">z2</td> <td style="padding:10px">z2</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
<td style="padding:10px">z2</td> <td style="padding:10px">z2</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
</tr> </tr>
<tr> <tr>
<td style="padding:10px">y</td> <td style="padding:10px">y</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
<td style="padding:10px">z0</td> <td style="padding:10px">z0</td>
<td style="padding:10px">a</td> <td style="padding:10px">a</td>
<td style="padding:10px">b</td> <td style="padding:10px">b</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
<td style="padding:10px">a</td> <td style="padding:10px">a</td>
<td style="padding:10px">z0</td> <td style="padding:10px">z0</td>
<td style="padding:10px">b</td> <td style="padding:10px">b</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
<td style="padding:10px">a</td> <td style="padding:10px">a</td>
<td style="padding:10px">b</td> <td style="padding:10px">b</td>
<td style="padding:10px">z1</td> <td style="padding:10px">z1</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
<td style="padding:10px">a</td> <td style="padding:10px">a</td>
<td style="padding:10px">b</td> <td style="padding:10px">b</td>
<td style="padding:10px">z2</td> <td style="padding:10px">z2</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
<td style="padding:10px">a</td> <td style="padding:10px">a</td>
<td style="padding:10px">z2</td> <td style="padding:10px">z2</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
<td style="padding:10px">z2</td> <td style="padding:10px">z2</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
<td style="padding:10px">Hash</td> <td style="padding:10px">Hash</td>
</tr> </tr>
</tbody></table> </tbody></table>
<Animation function visualisation> <Animation function visualisation>
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:exec Lösung :exec Lösung
``` ```
%% Output %% Output
Executed operation: Lösung() Executed operation: Lösung()
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
``` ```
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment