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

fix NAT symbols

parent 18af9653
No related branches found
No related tags found
No related merge requests found
%% Cell type:markdown id: tags:
# Turing Maschinen und Berechenbarkeit
Bisher wurden Turingmaschinen als Akzeptoren definiert.
Nun wollen wir Turingmaschinen als Maschinen zur Berechnung von
Funktionen auffassen.
Eine Funktion $f: \nats^k \rightarrow \nats$ heißt
Eine Funktion $f: ^k \rightarrow $ heißt
__Turing-berechenbar__, falls es eine deterministische
Turingmaschine $M=(\Sigma, \Gamma, Z, \delta ,z_0, \Box, F)$
mit $\Sigma = \{0,1\}$
gibt,
so dass für alle $n_1, n_2, \ldots , n_k, m \in \nats$:
* $f(n_1, n_2, \ldots , n_k) = m$ $\Leftrightarrow$
* $\exists z\in F . z_0 \mbox{bin}(n_1) \#
\mbox{bin}(n_2) \# \cdots \# \mbox{bin}(n_k) \vdash_{M}^{\ast} z
\mbox{bin}(m)$
Falls $f(n_1, n_2, \ldots , n_k)$ nicht definiert ist, läuft $M$ in
eine unendliche Schleife oder stoppt in einem Zustand $z\not\in F$.
%% Cell type:markdown id: tags:
Die (total definierte) \alert{\em Nachfolgerfunktion} $f: \nats \rightarrow \nats$ mit
Die (total definierte) __Nachfolgerfunktion__ $f: \rightarrow $ mit
* $f:n\rightarrow n+1$
ist Turing-berechenbar.
%% Cell type:code id: tags:
``` prob
::load
MACHINE TuringMachine_2
/* B Modell einer 1-band Turing Maschine */
/* by Michael Leuschel, 2012 */
/* The turing machine implements the +1 function on binary numbers */
/* See Slide 2 from folien-kapitel-7.pdf (Info 4) */
SETS
Alphabet ={O,I,Blank};
Z = {z0,z1,z2,ze};
Direction = {L,R,N}
DEFINITIONS
Σ == {O,I};
Γ == Σ;
CurSymbol == (Right<-Blank)(1);
ANIMATION_FUNCTION_DEFAULT == {(1,0,cur)};
ANIMATION_FUNCTION1 == {1} *( (%i.(i∈-size(Left)..-1|i+size(Left)+1) ; Left) \/ Right)
CONSTANTS Final, δ
PROPERTIES
Final ⊆ Z ∧
δ ∈ (Z * Alphabet) <-> (Z * Alphabet * Direction) ∧
δ = { (z0,O) ↦ (z0,O,R), (z0,I) ↦ (z0,I,R), (z0,Blank) ↦ (z1,Blank,L),
(z1,O) ↦ (z2,I,L), (z1,I) ↦ (z1,O,L), (z1,Blank) ↦ (ze,I,N),
(z2,O) ↦ (z2,O,L), (z2,I) ↦ (z2,I,L), (z2,Blank) ↦ (ze,Blank,R)
} ∧
Final = {ze}
VARIABLES Left,cur,Right
INVARIANT
cur ∈ Z ∧
Left ∈ seq(Alphabet) ∧ Right ∈ seq(Alphabet)
INITIALISATION Left,cur,Right := [],z0,[I,I,I,I,I] // [I,O,I]
OPERATIONS
Accept = PRE cur : Final THEN
Left,cur,Right := [],z0,Right /* restart machine with previous number */
END;
GoTo(z,S,znew,NewSymbol,Dir) =
PRE z=cur ∧ S=CurSymbol ∧
(z, S) ↦ (znew,NewSymbol,Dir) ∈ δ THEN
ANY tail_Right
WHERE (Right=[] ⇒ tail_Right=[]) ∧
(Right/=[] ⇒ tail_Right = tail(Right)) THEN
cur := znew ||
IF Dir = N THEN
Right := NewSymbol -> tail_Right
ELSIF Dir = R THEN
Left,Right := Left <- NewSymbol, tail_Right
ELSIF Left=[] THEN
Left,Right := [], Blank -> (NewSymbol -> tail_Right)
ELSE
Left,Right := front(Left), last(Left) -> (NewSymbol -> tail_Right)
END
END
END
END
```
%% Output
Loaded machine: TuringMachine_2
%% Cell type:code id: tags:
``` prob
:constants
```
%% Output
Machine constants set up using operation 0: $setup_constants()
%% Cell type:code id: tags:
``` prob
:init
```
%% Output
Machine initialised using operation 1: $initialise_machine()
%% Cell type:markdown id: tags:
Die Turing Maschine wird mit der Binärzahl 11111 (31 als Dezimalzahl) aufgerufen.
%% Cell type:code id: tags:
``` prob
:show
```
%% Output
<table style="font-family:monospace"><tbody>
<tr>
<td style="padding:10px">z0</td>
<td style="padding:10px">I</td>
<td style="padding:10px">I</td>
<td style="padding:10px">I</td>
<td style="padding:10px">I</td>
<td style="padding:10px">I</td>
</tr>
</tbody></table>
<Animation function visualisation>
%% Cell type:code id: tags:
``` prob
:exec GoTo
```
%% Output
Executed operation: GoTo(z0,I,z0,I,R)
%% Cell type:code id: tags:
``` prob
:show
```
%% Output
<table style="font-family:monospace"><tbody>
<tr>
<td style="padding:10px">I</td>
<td style="padding:10px">z0</td>
<td style="padding:10px">I</td>
<td style="padding:10px">I</td>
<td style="padding:10px">I</td>
<td style="padding:10px">I</td>
</tr>
</tbody></table>
<Animation function visualisation>
%% Cell type:code id: tags:
``` prob
:exec GoTo
```
%% Output
Executed operation: GoTo(z0,I,z0,I,R)
%% Cell type:code id: tags:
``` prob
:show
```
%% Output
<table style="font-family:monospace"><tbody>
<tr>
<td style="padding:10px">I</td>
<td style="padding:10px">I</td>
<td style="padding:10px">z0</td>
<td style="padding:10px">I</td>
<td style="padding:10px">I</td>
<td style="padding:10px">I</td>
</tr>
</tbody></table>
<Animation function visualisation>
%% Cell type:code id: tags:
``` prob
:exec GoTo
```
%% Output
Executed operation: GoTo(z0,I,z0,I,R)
%% Cell type:code id: tags:
``` prob
:show
```
%% Output
<table style="font-family:monospace"><tbody>
<tr>
<td style="padding:10px">I</td>
<td style="padding:10px">I</td>
<td style="padding:10px">I</td>
<td style="padding:10px">z0</td>
<td style="padding:10px">I</td>
<td style="padding:10px">I</td>
</tr>
</tbody></table>
<Animation function visualisation>
%% Cell type:code id: tags:
``` prob
:exec GoTo
```
%% Output
Executed operation: GoTo(z0,I,z0,I,R)
%% Cell type:code id: tags:
``` prob
:show
```
%% Output
<table style="font-family:monospace"><tbody>
<tr>
<td style="padding:10px">I</td>
<td style="padding:10px">I</td>
<td style="padding:10px">I</td>
<td style="padding:10px">I</td>
<td style="padding:10px">z0</td>
<td style="padding:10px">I</td>
</tr>
</tbody></table>
<Animation function visualisation>
%% Cell type:code id: tags:
``` prob
:exec GoTo
```
%% Output
Executed operation: GoTo(z0,I,z0,I,R)
%% Cell type:code id: tags:
``` prob
:show
```
%% Output
<table style="font-family:monospace"><tbody>
<tr>
<td style="padding:10px">I</td>
<td style="padding:10px">I</td>
<td style="padding:10px">I</td>
<td style="padding:10px">I</td>
<td style="padding:10px">I</td>
<td style="padding:10px">z0</td>
</tr>
</tbody></table>
<Animation function visualisation>
%% Cell type:code id: tags:
``` prob
:exec GoTo
```
%% Output
Executed operation: GoTo(z0,Blank,z1,Blank,L)
%% Cell type:code id: tags:
``` prob
:show
```
%% Output
<table style="font-family:monospace"><tbody>
<tr>
<td style="padding:10px">I</td>
<td style="padding:10px">I</td>
<td style="padding:10px">I</td>
<td style="padding:10px">I</td>
<td style="padding:10px">z1</td>
<td style="padding:10px">I</td>
<td style="padding:10px">Blank</td>
</tr>
</tbody></table>
<Animation function visualisation>
%% Cell type:code id: tags:
``` prob
:exec GoTo
```
%% Output
Executed operation: GoTo(z1,I,z1,O,L)
%% Cell type:code id: tags:
``` prob
:show
```
%% Output
<table style="font-family:monospace"><tbody>
<tr>
<td style="padding:10px">I</td>
<td style="padding:10px">I</td>
<td style="padding:10px">I</td>
<td style="padding:10px">z1</td>
<td style="padding:10px">I</td>
<td style="padding:10px">O</td>
<td style="padding:10px">Blank</td>
</tr>
</tbody></table>
<Animation function visualisation>
%% Cell type:code id: tags:
``` prob
:exec GoTo
```
%% Output
Executed operation: GoTo(z1,I,z1,O,L)
%% Cell type:code id: tags:
``` prob
:show
```
%% Output
<table style="font-family:monospace"><tbody>
<tr>
<td style="padding:10px">I</td>
<td style="padding:10px">I</td>
<td style="padding:10px">z1</td>
<td style="padding:10px">I</td>
<td style="padding:10px">O</td>
<td style="padding:10px">O</td>
<td style="padding:10px">Blank</td>
</tr>
</tbody></table>
<Animation function visualisation>
%% Cell type:code id: tags:
``` prob
:exec GoTo
```
%% Output
Executed operation: GoTo(z1,I,z1,O,L)
%% Cell type:code id: tags:
``` prob
:show
```
%% Output
<table style="font-family:monospace"><tbody>
<tr>
<td style="padding:10px">I</td>
<td style="padding:10px">z1</td>
<td style="padding:10px">I</td>
<td style="padding:10px">O</td>
<td style="padding:10px">O</td>
<td style="padding:10px">O</td>
<td style="padding:10px">Blank</td>
</tr>
</tbody></table>
<Animation function visualisation>
%% Cell type:code id: tags:
``` prob
:exec GoTo
```
%% Output
Executed operation: GoTo(z1,I,z1,O,L)
%% Cell type:code id: tags:
``` prob
:show
```
%% Output
<table style="font-family:monospace"><tbody>
<tr>
<td style="padding:10px">z1</td>
<td style="padding:10px">I</td>
<td style="padding:10px">O</td>
<td style="padding:10px">O</td>
<td style="padding:10px">O</td>
<td style="padding:10px">O</td>
<td style="padding:10px">Blank</td>
</tr>
</tbody></table>
<Animation function visualisation>
%% Cell type:code id: tags:
``` prob
:exec GoTo
```
%% Output
Executed operation: GoTo(z1,I,z1,O,L)
%% Cell type:code id: tags:
``` prob
:show
```
%% Output
<table style="font-family:monospace"><tbody>
<tr>
<td style="padding:10px">z1</td>
<td style="padding:10px">Blank</td>
<td style="padding:10px">O</td>
<td style="padding:10px">O</td>
<td style="padding:10px">O</td>
<td style="padding:10px">O</td>
<td style="padding:10px">O</td>
<td style="padding:10px">Blank</td>
</tr>
</tbody></table>
<Animation function visualisation>
%% Cell type:code id: tags:
``` prob
:exec GoTo
```
%% Output
Executed operation: GoTo(z1,Blank,ze,I,N)
%% Cell type:code id: tags:
``` prob
:show
```
%% Output
<table style="font-family:monospace"><tbody>
<tr>
<td style="padding:10px">ze</td>
<td style="padding:10px">I</td>
<td style="padding:10px">O</td>
<td style="padding:10px">O</td>
<td style="padding:10px">O</td>
<td style="padding:10px">O</td>
<td style="padding:10px">O</td>
<td style="padding:10px">Blank</td>
</tr>
</tbody></table>
<Animation function visualisation>
%% Cell type:code id: tags:
``` prob
:exec Accept
```
%% Output
Executed operation: Accept()
%% Cell type:markdown id: tags:
Die Turing Maschine hat 32 als Ergebnis ausgerechnet. Wir können die Maschine wieder mit 32 als Eingabe starten:
%% Cell type:code id: tags:
``` prob
:show
```
%% Output
<table style="font-family:monospace"><tbody>
<tr>
<td style="padding:10px">z0</td>
<td style="padding:10px">I</td>
<td style="padding:10px">O</td>
<td style="padding:10px">O</td>
<td style="padding:10px">O</td>
<td style="padding:10px">O</td>
<td style="padding:10px">O</td>
<td style="padding:10px">Blank</td>
</tr>
</tbody></table>
<Animation function visualisation>
%% Cell type:code id: tags:
``` prob
:exec GoTo
```
%% Output
Executed operation: GoTo(z0,I,z0,I,R)
%% Cell type:code id: tags:
``` prob
:exec GoTo
```
%% Output
Executed operation: GoTo(z0,O,z0,O,R)
%% Cell type:code id: tags:
``` prob
:show
```
%% Output
<table style="font-family:monospace"><tbody>
<tr>
<td style="padding:10px">I</td>
<td style="padding:10px">O</td>
<td style="padding:10px">z0</td>
<td style="padding:10px">O</td>
<td style="padding:10px">O</td>
<td style="padding:10px">O</td>
<td style="padding:10px">O</td>
<td style="padding:10px">Blank</td>
</tr>
</tbody></table>
<Animation function visualisation>
%% Cell type:code id: tags:
``` prob
:exec GoTo
```
%% Output
Executed operation: GoTo(z0,O,z0,O,R)
%% Cell type:code id: tags:
``` prob
:exec GoTo
```
%% Output
Executed operation: GoTo(z0,O,z0,O,R)
%% Cell type:code id: tags:
``` prob
:exec GoTo
```
%% Output
Executed operation: GoTo(z0,O,z0,O,R)
%% Cell type:code id: tags:
``` prob
:exec GoTo
```
%% Output
Executed operation: GoTo(z0,O,z0,O,R)
%% Cell type:code id: tags:
``` prob
:exec GoTo
```
%% Output
Executed operation: GoTo(z0,Blank,z1,Blank,L)
%% Cell type:code id: tags:
``` prob
:show
```
%% Output
<table style="font-family:monospace"><tbody>
<tr>
<td style="padding:10px">I</td>
<td style="padding:10px">O</td>
<td style="padding:10px">O</td>
<td style="padding:10px">O</td>
<td style="padding:10px">O</td>
<td style="padding:10px">z1</td>
<td style="padding:10px">O</td>
<td style="padding:10px">Blank</td>
</tr>
</tbody></table>
<Animation function visualisation>
%% Cell type:code id: tags:
``` prob
:exec GoTo
```
%% Output
Executed operation: GoTo(z1,O,z2,I,L)
%% Cell type:code id: tags:
``` prob
:show
```
%% Output
<table style="font-family:monospace"><tbody>
<tr>
<td style="padding:10px">I</td>
<td style="padding:10px">O</td>
<td style="padding:10px">O</td>
<td style="padding:10px">O</td>
<td style="padding:10px">z2</td>
<td style="padding:10px">O</td>
<td style="padding:10px">I</td>
<td style="padding:10px">Blank</td>
</tr>
</tbody></table>
<Animation function visualisation>
%% Cell type:code id: tags:
``` prob
:exec GoTo
```
%% Output
Executed operation: GoTo(z2,O,z2,O,L)
%% Cell type:code id: tags:
``` prob
:exec GoTo
```
%% Output
Executed operation: GoTo(z2,O,z2,O,L)
%% Cell type:code id: tags:
``` prob
:exec GoTo
```
%% Output
Executed operation: GoTo(z2,O,z2,O,L)
%% Cell type:code id: tags:
``` prob
:exec GoTo
```
%% Output
Executed operation: GoTo(z2,O,z2,O,L)
%% Cell type:code id: tags:
``` prob
:exec GoTo
```
%% Output
Executed operation: GoTo(z2,I,z2,I,L)
%% Cell type:code id: tags:
``` prob
:show
```
%% Output
<table style="font-family:monospace"><tbody>
<tr>
<td style="padding:10px">z2</td>
<td style="padding:10px">Blank</td>
<td style="padding:10px">I</td>
<td style="padding:10px">O</td>
<td style="padding:10px">O</td>
<td style="padding:10px">O</td>
<td style="padding:10px">O</td>
<td style="padding:10px">I</td>
<td style="padding:10px">Blank</td>
</tr>
</tbody></table>
<Animation function visualisation>
%% Cell type:code id: tags:
``` prob
:exec GoTo
```
%% Output
Executed operation: GoTo(z2,Blank,ze,Blank,R)
%% Cell type:code id: tags:
``` prob
:show
```
%% Output
<table style="font-family:monospace"><tbody>
<tr>
<td style="padding:10px">Blank</td>
<td style="padding:10px">ze</td>
<td style="padding:10px">I</td>
<td style="padding:10px">O</td>
<td style="padding:10px">O</td>
<td style="padding:10px">O</td>
<td style="padding:10px">O</td>
<td style="padding:10px">I</td>
<td style="padding:10px">Blank</td>
</tr>
</tbody></table>
<Animation function visualisation>
%% Cell type:markdown id: tags:
Die Turing Maschine at 33 als Ergebnis zurückgegeben.
%% Cell type:code id: tags:
``` prob
:exec Accept
```
%% Output
Executed operation: Accept()
%% Cell type:code id: tags:
``` prob
```
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment