Repräsentierbarkeit von Registerprogrammen/Über p-adische beta Funktion/Fakt/Beweis

Beweis

Es sei ${}A_{P}$ der das Programm repräsentierende Ausdruck im Sinne von Fakt in den Variablen ${}r_{0},\ldots ,r_{m},r_{0}',\ldots ,r_{m}'$ (zur Notationsvereinfachung schreiben wir also ${}r_{0}$ statt ${}z$ und ${}r_{0}'$ statt ${}z'$.). Es sei ${}\vartheta$ der Ausdruck (in den vier freien Variablen $p,n,i,r$), der die ${}\beta$-Funktion arithmetisch repräsentiert. Der Ausdruck

$\vartheta (p,n,i,r)$

ist also genau dann wahr in ${}\mathbb {N}$, wenn ${}\beta (p,n,i)=r$ ist. Diese Beziehung verwenden wir für ${}i=s(m+1)+j$ (bzw. $i=(s+1)(m+1)+j$) und ${}r=r_{j}$ (bzw. $r=r'_{j}$) und ${}j=0,\ldots ,m$. Daher ist der Ausdruck (in den freien Variablen $p,n,s,r_{j},r_{j}'$)

$T(p,n,s):=\vartheta (p,n,s(m+1),r_{0})\wedge \ldots \wedge \vartheta (p,n,s(m+1)+m,r_{m})\wedge \vartheta (p,n,(s+1)(m+1),r'_{0})\wedge \ldots \wedge \vartheta (p,n,(s+1)(m+1)+m,r'_{m})\,$

bei Interpretation in ${}\mathbb {N}$ genau dann wahr, wenn die ${}\beta$-Funktion ${}\beta (p,n,-)$ für die ${}m+1$ aufeinander folgenden Zahlen (eingesetzt in die dritte Komponente der ${}\beta$-Funktion) ${}s(m+1),s(m+1)+1,\ldots ,s(m+1)+m$ gleich ${}r_{0},r_{1},\ldots ,r_{m}$ und für die ${}m+1$ aufeinander folgenden Zahlen ${}(s+1)(m+1),(s+1)(m+1)+1,\ldots ,(s+1)(m+1)+m$ gleich ${}r'_{0},r'_{1},\ldots ,r'_{m}$ ist. An der mit ${}s(m+1)+j$ bezeichneten Stelle in ${}T(p,n,s)$ steht die ${}(m+1)$-fache Addition der Variablen ${}s$ mit sich selbst plus die ${}j$-fache Addition der ${}1$.

Mit diesem Ausdruck soll der Konfigurationsübergang beim ${}s$-ten Rechenschritt beschrieben werden. Da man die Registerbelegung beim ${}s$-ten Rechenschritt nicht von vornherein kennt, muss man den Übergang mit Allquantoren ansetzen. Der Ausdruck

$E(p,n,s):=\forall r_{0}\forall r_{1}\ldots \forall r_{m}\forall r_{0}'\forall r'_{1}\ldots \forall r'_{m}(T(p,n,s)\rightarrow A_{P})\,$

besagt, dass der durch ${}p,n,s$ über die ${}\beta$-Funktion kodierte Konfigurationsübergang durch das Programm bewirkt wird.

In analoger Weise ist der Ausdruck (in den ${}m+2$ freien Variablen $p,n,x_{1},\ldots ,x_{m}$)

$D(p,n)(x_{1},\ldots ,x_{m}):=\vartheta (p,n,0,1)\wedge \vartheta (p,n,1,x_{1})\wedge \ldots \wedge \vartheta (p,n,m,x_{m})\,$

(bei inhaltlicher Interpretation) genau dann wahr, wenn ${}\beta (p,n,0)=1$ und ${}\beta (p,n,j)=x_{j}$ für ${}j=1,\ldots ,m$ ist. Der Ausdruck (in den $m+3$ freien Variablen $p,n,t,y_{1},\ldots ,y_{m}$)

$F(p,n,t)(y_{1},\ldots ,y_{m}):=\vartheta (p,n,t(m+1),h)\wedge \vartheta (p,n,t(m+1)+1,y_{1})\wedge \ldots \wedge \vartheta (p,n,t(m+1)+m,y_{m})\,$

ist genau dann wahr, wenn ${}\beta (p,n,t(m+1))=h$ und ${}\beta (p,n,t(m+1)+j)=y_{j}$ für ${}j=1,\ldots ,m$ ist.

Somit besagt der Ausdruck

$\psi _{P}=\exists p\exists n\exists t{\left(D(p,n)(x_{1},\ldots ,x_{m})\wedge \forall s(1\leq s<t\rightarrow E(p,n,s))\wedge F(p,n,t)(y_{1},\ldots ,y_{m})\right)}\,,$

dass das Programm mit der Startkonfiguration ${}(1,x_{1},\ldots ,x_{m})$ anhält und dabei die Konfiguration ${}(h,y_{1},\ldots ,y_{m})$ erreicht.

Zur bewiesenen Aussage