Registermaschine/Einzelbefehle/Arithmetische Repräsentierung/Definition

Arithmetische Ausdrücke für Befehle

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}).$