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

Aus Wikiversity
Zur Navigation springen Zur Suche springen
Beweis

Es sei der das Programm repräsentierende Ausdruck im Sinne von Fakt in den Variablen (zur Notationsvereinfachung schreiben wir also statt und statt .). Es sei der Ausdruck (in den vier freien Variablen ), der die -Funktion arithmetisch repräsentiert. Der Ausdruck

ist also genau dann wahr in , wenn ist. Diese Beziehung verwenden wir für (bzw. ) und (bzw. ) und . Daher ist der Ausdruck (in den freien Variablen )

bei Interpretation in genau dann wahr, wenn die -Funktion für die aufeinander folgenden Zahlen (eingesetzt in die dritte Komponente der -Funktion) gleich und für die aufeinander folgenden Zahlen gleich ist. An der mit bezeichneten Stelle in steht die -fache Addition der Variablen mit sich selbst plus die -fache Addition der .

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

besagt, dass der durch über die -Funktion kodierte Konfigurationsübergang durch das Programm bewirkt wird.

In analoger Weise ist der Ausdruck (in den freien Variablen )

(bei inhaltlicher Interpretation) genau dann wahr, wenn und für ist, und der Ausdruck (in den freien Variablen )

ist genau dann wahr, wenn und für ist.

Somit besagt der Ausdruck

dass das Programm mit der Startkonfiguration anhält und dabei die Konfiguration erreicht.

Zur bewiesenen Aussage