Registermaschine/Einzelbefehle/Übergang/Arithmetische Repräsentierung/Textabschnitt

Lemma

Die Programmzeilen eines Registerprogramms mit ${}m$ Registern bzw. die zugehörige Programmabbildung lassen sich folgendermaßen mit den Variablen ${}z,r_{1},\ldots ,r_{m},z',r'_{1},\ldots ,r'_{m}$ arithmetisch repräsentieren (dabei sei ${}\ell$ die aktuelle Programmzeile).

1. ${}B_{\ell }=i+$ wird arithmetisiert durch

   $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. ${}B_{\ell }=i-$ wird arithmetisiert durch

   $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. ${}B_{\ell }=C(i,j)$ wird arithmetisiert durch

   $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. ${}B_{\ell }=B_{h}=H$ wird arithmetisiert durch

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

Beweis

Die arithmetische Repräsentierbarkeit der Programmabbildung ${}\varphi _{P}$ bedeutet, dass ${}\varphi _{P}(z,r_{1},\ldots ,r_{m})=(z',r'_{1},\ldots ,r'_{m})$ genau dann gilt, wenn die entsprechende arithmetische Aussage ${}A_{z}$ in ${}\mathbb {N}$ gilt. Genau so wurden aber die ${}A_{z}$ definiert.

$\Box$

Zu einem gegebenen Programm bestehend aus den Programmzeilen ${}P_{1},\ldots ,P_{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}.$

Die Aussage ${}A_{P}$ ist somit für eine Variablenbelegung (der Variablen $z,z',r_{j},r_{j}'$ mit Werten in ${}\mathbb {N}$) genau dann gültig, wenn ${}\ell =z^{\mathbb {N} }>h$ ist (da dann keine Bedingung der einzelnen konjugierten Aussage erfüllt ist) oder wenn ${}\ell \leq h$ ist und ${}A_{\ell }$ erfüllt (d.h. dass die Konklusion in $A_{\ell }$ erfüllt ist) ist, und dies ist nach dem Lemma genau dann der Fall, wenn die (Variablen)-Belegung von ${}z'$ die Programmzeilennummer ist, die durch den aktuellen (durch die Belegung von ${}z$ festgelegten) Befehl ${}B_{\ell }$ als nächste Programmzeile aufgerufen wird, und wenn die Belegungen der ${}r_{i}'$ die aus diesem Befehl resultierenden Belegungen der ${}r_{i}$ sind.