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

Aus Wikiversity
Zur Navigation springen Zur Suche springen
Repräsentierbarkeit des Halteproblems

Für ein Programm für eine Registermaschine

gibt es einen arithmetischen Ausdruck , der genau dann (bei der Standardinterpretation in den natürlichen Zahlen) gilt, wenn das Programm anhält.

Genauer gesagt: Wenn das Programm Programmzeilen besitzt und Register verwendet, so gibt es einen arithmetischen Ausdruck in freien Variablen

derart, dass
genau dann gilt, wenn das Programm bei Eingabe von nach endlich vielen Schritten bei der Konfiguration anlangt

(und insbesondere anhält).

Zum Beweis, Alternativen Beweis erstellen