Registermaschine/Einzelbefehle/Arithmetische Repräsentierung/Textabschnitt

Definition

Den Programmzeilen ${}B_{1},\ldots ,B_{h}$ eines Registerprogramms mit ${}m$ Registern werden die folgenden arithmetischen Ausdrücke ${}A_{1},\ldots ,A_{h}$ in den freien Variablen ${}z,r_{1},\ldots ,r_{m},z',r'_{1},\ldots ,r'_{m}$ zugeordnet.

1. Bei ${}B_{\ell }=i+$ setzt man

   $A_{\ell }:=(z=\ell )\rightarrow (z'=z+1)\wedge (r_{1}'=r_{1})\wedge \ldots \wedge (r_{i-1}'=r_{i-1})\wedge (r_{i}'=r_{i}+1)\wedge (r_{i+1}'=r_{i+1})\wedge \ldots \wedge (r_{m}'=r_{m}).$

2. Bei ${}B_{\ell }=i-$ setzt man

   $A_{\ell }:=(z=\ell )\rightarrow (z'=z+1)\wedge (r_{1}'=r_{1})\wedge \ldots \wedge (r_{i-1}'=r_{i-1})\wedge ((r_{i}=0)\rightarrow (r'_{i}=r_{i}))\wedge (\neg (r_{i}=0)\rightarrow (r_{i}'+1=r_{i}))\wedge (r_{i+1}'=r_{i+1})\wedge \ldots \wedge (r_{m}'=r_{m}).$

3. Bei ${}B_{\ell }=C(ij)$ setzt man

   $A_{\ell }:=(z=\ell )\rightarrow ((r_{i}=0)\rightarrow (z'=j))\wedge (\neg (r_{i}=0)\rightarrow (z'=z+1))\wedge (r_{1}'=r_{1})\wedge \ldots \wedge (r_{m}'=r_{m}).$

4. Bei ${}B_{\ell }=B_{h}=H$ setzt man

   $A_{h}:=(z=h)\rightarrow (z'=z)\wedge (r_{1}'=r_{1})\wedge \ldots \wedge (r_{m}'=r_{m}).$

Hierbei werden die natürlichen Zahlen ${}\ell$ und ${}j$ in den arithmetischen Ausdrücken durch die entsprechenden Summen ${}1+\cdots +1$ repräsentiert, die Abfrage am ${}i$-ten Register schlägt sich in der Variablenbezeichnung nieder.

Wie bei der Programmabbildung ist es sinnvoll, für alle Programmzeilennummern (also auch für $\ell >h$) einen arithmetischen Ausdruck zu haben. Dazu setzen wir

$A_{h+1}:=(z\geq h+1)\rightarrow (z'=z)\wedge (r_{1}'=r_{1})\wedge \ldots \wedge (r_{m}'=r_{m})$

(wobei $z\geq h+1$ eine Abkürzung ist). Zu einem gegebenen Programm bestehend aus den Programmzeilen ${}B_{1},\ldots ,B_{h}$ betrachtet man die Konjunktion der soeben eingeführten zugehörigen arithmetischen Repräsentierungen, also ${}A_{P}=A_{1}\wedge A_{2}\wedge \ldots \wedge A_{h}\wedge A_{h+1}$. Dieser Ausdruck repräsentiert die Programmabbildung.

Lemma

Es sei ${}P$ ein Registerprogramm mit den Programmzeilen ${}B_{1},\ldots ,B_{h}$ und ${}m$ Registern mit den zugehörigen arithmetischen Ausdrücken ${}A_{1},\ldots ,A_{h}$ in den freien Variablen ${}z,r_{1},\ldots ,r_{m},z',r'_{1},\ldots ,r'_{m}$. Es sei ${}A_{P}=A_{1}\wedge \ldots \wedge A_{h}\wedge A_{h+1}$.

Dann ist ${}A_{P}$ eine arithmetische Repräsentierung der Programmabbildung ${}\varphi _{P}$.

Beweis

Die Variablen ${}z,z',r_{j},r_{j}'$ seien durch die natürlichen Zahlen ${}\ell ,\ell ',n_{j},n_{j}'$ belegt. Wir müssen zeigen, dass die Gleichheit

${}\varphi _{P}(\ell ,n_{1},\ldots ,n_{m})=(\ell ',n'_{1},\ldots ,n'_{m})\,$

genau dann gilt, wenn

$\mathbb {N} \vDash A_{P}(\ell ,\ell ',n_{1},\ldots ,n_{m},n'_{1},\ldots ,n'_{m})$

gilt. Der Ausdruck ${}A_{P}$ gilt genau dann, wenn sämtliche Ausdrücke ${}A_{1},A_{2},\ldots ,A_{h},A_{h+1}$ gelten. Es sei ${}\ell$ fixiert. Dann gelten sämtliche ${}A_{k}$, ${}k\neq \ell$, automatisch, da für diese Ausdrücke der Vordersatz nicht gilt. Die Gültigkeit von ${}A_{P}$ bei dieser Belegung bedeutet also, dass der Nachsatz in ${}A_{\ell }$ gelten muss. Sowohl ${}\varphi (\ell ,-)$ als auch der Nachsatz von ${}A_{\ell }$ drücken die Wirkungsweise des Befehls ${}B_{\ell }$ aus, daher gilt die Abbildungsgleichheit genau dann, wenn ${}A_{\ell }$ wahr ist.

$\Box$