Computations of a Turing machine can be modelled by propositional formulas, provided there is a bound on the number of steps considered (and the number of tape cells available).

This statement is true regardless of which model of Turing machine is used. In the following, it is assumed that the tape is unbounded to the left and to the right and that a transition is of the form $q, a \to q', b', d$ where

$q$ and $q'$ are states,
$a$ and $b'$ are symbols from the working alphabet $B$, and
$d$ is a head direction, one of $\text L$, $\text N$, and $\text R$.

The blank symbol is denoted $\_$.

A configuration of a Turing machine is given by:

a state $q \in Q$,
a tape content $u$, which is a non-empty word over $B$,
a head position $j<|u|$.

When a transition is applicable to a given configuration, its application results in a new configuration (or the old one), depending on the concrete configuration and the concrete transition.

Example Suppose a Turing machine is in state $q_4$, its tape content is $abaadbaa$, and the head is at position $3$. Then the transition $q_4, a \to q_2, c, \text R$ would be applicable and the application of the transition would result in the configuration where the Turing machine is in state $q_2$, the tape content is $abacdbaa$, and the head position is $4$.

Example Suppose a Turing machine is in state $q_4$, its tape content is $abaadbaa$, and the head is at position $0$. Then the transition $q_4, a \to q_1, c, \text L$ would be applicable and the application of the transition would result in the configuration where the Turing machine is in state $q_1$, the tape content is $\_cbaadbaa$, and the head position is $0$. This is more complicated than the previous example, because the length of the tape changed.

The objective is to model computations with $k$ steps where no more than $l$ tape cells are used in propositional logic. More concretely, objects of the following form are to be modelled:

state	content of tape	position of head
$q_0$	$u_0$	$h_0$
$q_1$	$u_1$	$h_1$
...	...	...
$q_k$	$u_k$	$h_k$

How do we represent such sequences by variable assignments? What are the right variables to choose?

We use, for each configuration $i$ and

each state $q \in Q$, a variable $X_i^q$ which means: in configuration $i$ the state is $q$,
each symbol $b \in B$ and position $j<l$, a variable $X_i^{j,b}$ which means: in configuration $i$ the symbol $b$ is at position $j$,
each position $j<l$, a variable $X_i^j$ which means: in configuration $i$ the head is at position $j$.

To identify exactly those assignments to these variables that represent computations, we construct formulas which express the following:

States: There is exactly one state in each configuration.
Symbols: There is at most one symbol in each position of a configuration.
NoSymbols: If there is no symbol at some position in some configuration, then there is no further symbol to the right.
Heads: There is exactly one position where the head is and at this position there is a tape cell.
Transitions: From one configuration to the next one, a transition is applied.

Except for the last one, all these formulas are easy to come up with: \begin{align} \text{States} & = \bigwedge_{i<k+1} \dot{\bigvee_{q \in Q}} X_i^q\\ \text{Symbols} & = \bigwedge_{i<k+1} \bigwedge_{j<l} \bigwedge_{b \neq b'} \left(\neg X_i^{j,b} \vee \neg X_i^{j,b'}\right)\\ \text{NoSymbols} & = \bigwedge_{i<k+1} \bigwedge_{j +1< l} \left(\bigwedge_{b \in B} \neg X_i^{j,b} \rightarrow \bigwedge_{b \in B} \neg X_i^{j+1,b}\right)\\ \text{Heads} & = \bigwedge_{i<k+1} \left(\dot{\bigvee_{j<l}} X_i^j \wedge \bigwedge_{j<l} \left(X_i^j \rightarrow \bigvee_{b \in B} X_i^{j,b}\right)\right) \end{align}

What remains to be developped is the last formula. One approach is to say that for any configuration except for the last one, it is true that one of the transition applies. This leads to: \begin{align} \text{Transitions} & = \bigwedge_{i<k} \; \bigvee_{q,b \to q', b', d \in \delta} \text{Applies}_i(q, b, q', b', d) \enspace. \end{align}

So all that is left is to describe how a transition is applied. It is helpful to distinguish the following five different types of applications:

the head does not move,
the head moves to the left and is on the first cell,
the head moves to the left and is not on the first cell,
the head moves to the right and is on the last cell,
the head moves to the right and is not on the last cell.

A difficult situation is the second one described, because it requires to add a blank cell to the left of the current tape. Here is the formula that takes care of it: $$\left[ X_i^q \wedge X_i^0 \wedge X_i^{0,b} \wedge \bigwedge_{b \in B} \neg X_i^{l-1,b} \right] \wedge \left[ X_{i+1}^{q'} \wedge X_{i+1}^0 \wedge X_{i+1}^{0,\_} \wedge X_{i+1}^{1,b'} \right] \wedge \left[\bigwedge_{0<j<l-1} \bigwedge_{b \in B} \left(X_i^{j,b} \leftrightarrow X_{i+1}^{j+1,b}\right) \right] $$ The first part expresses what needs to be true in configuration $i$ so that the transition is applicable, the second part expresses what it means for the transition to be applied around the head, and the third row expresses that the other cells stay the same.

The overall formula is $\text{Computation}_k^l$, which is defined as $$\text{Computation}_k^l = \text{States} \wedge \text{Symbols} \wedge \text{NoSymbols} \wedge \text{Heads} \wedge \text{Transitions}$$ as described above.

Proposition

Let $T$ be a Turing machine as above, $k \geq 0$, and $l \geq 1$. Then the 1-assignments of the formula $\text{Computation}_{k,l}$ represent the computations of $T$ with $k$ steps and within space $l$.
The size of the formula is $\theta(k l)$.
When converted to conjunctive normal form, the size of the formula becomes $\theta(kl^2)$.

Proof We only sketch the proof of the second and third part by first estimating the size of the five conjuncts of the formula:

$\text{States}$: $\theta(k)$,
$\text{Symbols}$: $\theta(kl)$,
$\text{NoSymbols}$: $\theta(kl)$,
$\text{Heads}$: $\theta(kl)$,
$\text{Transitions}$: $\theta(kl)$.

Most of the subformulas of $\text{Computation}_k^l$ which are not in CNF are of constant size, which means they can easily be converted to CNF without changing the asymptotic size of the formula. The only exception is the exclusive or in $\text{Heads}$, which has size $\theta(l)$. A conversion to CNF results in a formula of size $\theta(l^2)$.

Exercises

Exercise Im folgenden betrachten wir Berechnungen der nichtdeterministischen Turingmaschine $M$ über dem Bandalphabet $B=\{0,1,\_\}$ mit den Zuständen $Q=\{q_0,q_1\}$, dem Startzustand $q_0$, den Transitionen $\{(q_0,0)\to (q_0,0,R); (q_0,1)\to (q_1,1,R); (q_1,0)\to (q_1,1,R);(q_1,0)\to (q_0,0,R); (q_1,1)\to (q_1,1,R)\}$.

Wie viele Variablen werden bei der Modellierung von Berechnungen für die oben genannte Turingmaschine benötigt, wenn man $k=5$ Schritte betrachtet und das Band maximal Länge $\ell=6$ hat?
Geben Sie die ersten fünf Konfiguration von zwei verschiedenen Berechnungen der Turingmaschine mit dem initialen Bandinhalt $u=011000$ an.
Gibt es eine 1-Belegung $\beta$ von $\text{Computation}^6_4$ mit $\beta(X_0^{0,0})=1$? Begründen Sie Ihre Antwort kurz.
Gibt es eine 1-Belegung $\beta$ von $\text{Computation}^6_4$, sodass $\beta(X_i^{p,1})=\beta(X_{i+1}^{p,0})=1$ für irgendeinen Schritt $i\leq 4$ und eine Position $p\leq 5$ gilt? Begründen Sie Ihre Antwort kurz.
Wie viele verschiedene knappe 1-Belegung $\beta$ von $\text{Init}[011000]\wedge \text{Computation}^{6}_{2}$ gibt es? Dabei sei $\text{Init}[u]$ wie hier definiert. Begründen Sie Ihre Antwort kurz.
Wie viele verschiedene knappe 1-Belegung $\beta$ von $\text{Init}[011000]\wedge \text{Computation}^{6}_{5}$ gibt es? Begründen Sie Ihre Antwort kurz.

Lösung

Zunächst eine kurze Überlegung welche Berechnungen $M$ durchführen kann: $M$ liest den Bandinhalt von links nach rechts. Liest $M$ eine $1$, können alle direkt folgende $0$en durch $1$en ersetzt werden. Das geschieht aber nichtdeterministisch, sodass die $0$en erstetzt werden können aber nicht müssen. Wird eine $1$ nicht ersetzt, so darf auch eine weitere direkt folgende $0$ ersetzt werden.

Allgemein gilt $|\{X_i^q \mid i\leq k, q\in Q \} \cup \{X_i^{j,b} \mid i\leq k, b\in B, j < l \} \cup \{X_i^j \mid j< l, i\leq k \}| = (k+1)|Q|+(k+1)l|B|+(k+1)l$. Somit gibt es bei $|Q|=2$, $|B|=3$, $k=5$ und $\ell=$6 insgesamt $156$ ($=12+108+36$) Variablen benötigt.
- $(q_0,011000,0),(q_0,011000,1),(q_1,011000,2),(q_1,011000,3),(q_0,011000,4)$
- $(q_0,011000,0),(q_0,011000,1),(q_1,011000,2),(q_1,011000,3),(q_1,011100,4)$
Ja, die gibt es. Es gibt das Wort $000000$, der Länge 6, bei dem die Turingmaschine vier Schritte hintereinander den Bandinhalt unverändert lässt und nur Ihren Kopf bewegt. Da $\beta(X_0^{0,0})$ bedeutet bei korrekter Modellierung dann nur, dass initial das erste Zeichen $0$ ist, was für das gegebene Wort der Fall ist.
Nein, die kann es nicht geben. Würde es diese geben, müsste die Turingmaschine im Schritt $i+1$ an der Position $p$ die $1$ zu einer $0$ ersetzen. Doch die Turingmaschine kann aufgrund ihrer Transitionsmenge nur eine $0$ schreiben, wenn an der Stelle bereits eine $0$ gelesen wurde. D.h. bei korrekter Modellierung wird die Teilformel $\text{Transitions}$ nicht erfüllt.
Genau eine. In den ersten zwei Schritten gibt es für die gegebene nur eine mögliche Konfigurationsfolge. Nichtdeterminismus ist erst möglich, sobald eine $0$ nach einer $1$ gelesen wurde und sich die TM im Zustand $q_1$ befindet. Da eine erfüllende knappe Belegung genau einer gültigen Konfiguration entspricht (Der Bandinhalt, die Kopfposition sind in jedem Schritt ist eindeutig), kann es also auch nicht verschiedene Belegungen geben.
Drei Möglichkeiten, da es auch genau drei mögliche gülte Konfigurationsfolgen für die ersten fünf Schritte der Turingmaschine gibt und jede einer knappen $1$-Belegung entspricht. Da der Kopf sich immer nur nach rechts bewegt, muss nur betrachtet werden, wie viele Möglichkeiten es gibt $0$en durch $1$en in den ersten fünf Schritten zu ersetzen. Es ergeben sich folgende drei Berechnungen:
- $(q_0,011000,0),(q_0,011000,1),(q_1,011000,2),(q_1,011000,3),(q_0,011000,4),(q_0,011000,5)$
- $(q_0,011000,0),(q_0,011000,1),(q_1,011000,2),(q_1,011000,3),(q_1,011100,4),(q_0,011100,5)$
- $(q_0,011000,0),(q_0,011000,1),(q_1,011000,2),(q_1,011000,3),(q_1,011100,4),(q_1,011110,5)$

Exercise Ergänzen Sie die Modellierung von Berechnungen um folgende fehlende Teilformeln bei den Transitionen:

Fall 1: Der Kopf bewegt sich nicht.
Fall 2: Der Kopf bewegt sich nach links und ist nicht auf der ersten Position.

Lösung

$\left(X_i^q \wedge X_{i+1}^{q'}\right) \wedge \underbrace{\left(\bigwedge\limits_{0\leq j<l}\left(X_i^j \rightarrow (X_{i+1}^j \wedge X_i^{j,b}\wedge X_{i+1}^{j,b'})\right)\right)}_{\text{Gleiche Kopfposition und $b\to b'$}}\wedge \underbrace{\left(\bigwedge\limits_{0\leq j<l}\left(\neg X_i^j \rightarrow \bigwedge\limits_{b\in B}(X_{i}^{j,b} \leftrightarrow X_{i+1}^{j,b})\right)\right)}_{\text{Symbole nicht an der Kopfposition bleiben gleich.}}$
$\left(X_i^q \wedge \neg X_i^0 \wedge X_{i+1}^{q'}\right)\wedge \underbrace{\bigvee\limits_{j<l}(X_i^{j}\wedge X_{i+1}^{j-1}\wedge X_i^{j,b}\wedge X_{i+1}^{j,b'})}_{\text{Kopf 1 nach links und $b\to b'$}}\wedge \underbrace{\left(\bigwedge\limits_{0\leq j<l}\left(\neg X_i^j \rightarrow \bigwedge\limits_{b\in B}(X_{i}^{j,b} \leftrightarrow X_{i+1}^{j,b})\right)\right)}_{\text{Symbole nicht an der $j$ten Kopfposition bleiben gleich.}}$

Exercise Betrachten Sie die Turingmaschine $M$ über dem Bandalphabet $B=\{0,1\}$ mit den Zuständen $Q=\{q_0,q_1\}$, dem Startzustand $q_0$ und mit der Transitionsfunktion $\delta=\{q_0,0\to q_0,0,R; q_0,1\to q_1,1,N; q_1,0\to q_0,0,N; q_1,1\to q_0,0,N\}$ mit dem initialen Bandinhalt $u=011$.

Geben Sie die Folge der ersten 6 Konfigurationen dieser Turingmaschine an.
Geben Sie für die gegebene Turingmaschine und $k=3$ Schritte die Menge aller Variablen der Modellierung von Berechnungen explizit an. Nehmen Sie dabei an, dass der Bandinhalt der Maschine nie länger als $\ell=4$ wird.
Geben Sie die Formeln $\text{States}$ und $\text{Symbols}$ aus der Modellierung von Berechnungen für die gegebene Turingmaschine und $k=3$ Schritte explizit an. Verzichten Sie hierbei auf die Metanotationen. Nehmen Sie dabei wiederum an, dass der Bandinhalt der Maschine nie länger als $\ell=4$ wird.

Modelling computations in propositional logic

From Learning Logic for Computer Science

Exercises