¿Por qué el problema de detención es decidible para los idiomas gotoimos limitados en el valor más alto de las constantes y las variables?

Question

Esto se toma de un antiguo examen de mi universidad que estoy usando para prepararme para el próximo examen:

Dado es un idioma $ \ texto {goto} _ {17} ^ C \ subesteq \ texto {goto} $ . Este lenguaje contiene exactamente aquellos $ \ texto {goto} $ programas en los que no hay constante nunca más arriba $ 17 $ ni ninguna variable nunca más arriba $ C $ .

$ goto $ aquí describe el conjunto de todos los programas escritos en el $ goto $ lenguaje compuesto de los siguientes elementos:

con variables $ v_i \ in \ mathbb {n} $ y constants $ c \ in \ mathbb {n} $
Asignación: $ x_i:= c, x_i:= x_i \ pm C $
Salto condicional: si (comparación) goto $ l_i $
HaltCommand: Halt

Actualmente estoy luchando con la formalización de una prueba, pero esto es lo que he llegado hasta ahora, expresado muy casualmente: Para cualquier programa dado en este conjunto, sabemos que es finito. Un programa finito contiene una cantidad finita de variables y una cantidad finita de estados, o líneas para estar. Como tal, existe una cantidad finita de configuraciones en las que este proceso puede ser. Si dejamos que este programa funcione, podemos mantener una lista de todas las configuraciones que hemos visto. Es decir, la combinación de todos los valores variables utilizados y el estado del programa. Si dejamos que el programa se ejecute, debe haber una de las dos cosas que ocurren eventualmente: El programa se detiene. En este caso, devolvemos sí y hemos decidido que se detiene. El programa llega a una configuración que se ha registrado antes. A medida que el lenguaje es determinista, esto significa que debemos haber ido un bucle completo que repetirá exactamente ahora.

No puede existir otro caso, ya que eso significaría que seguimos funcionando para siempre en el código finito sin repetir una configuración. Esto significa después de cada paso, entre nuestra lista de pasos infinitos, hay una nueva configuración. Esto significaría que hay configuraciones infinitas, que es una contradicción.

es este correcto? Además, ¿cómo se vería una prueba más formal si es? Si no, ¿cómo se vería una prueba correcta?

Answer 1

Hay un número finito de estados diferentes (el conjunto de valores de las variables y el contador del programa).Sus "Programas GOTO LIMITADOS" son solo una forma (desordenada) de describir un autómata finito determinista.

O simplemente razón de que el programa estable es finito, es ciertamente posible trazar todas las computadoras posibles que no sean en bucle (por algo como una primera búsqueda en amplitud de la gráfica de estados y vecinos).