Qual é a parada problema decidível para ir para idiomas limitado sobre o valor mais alto de constantes e variáveis?

Question

Isso é obtido a partir de um exame antigo da minha universidade que eu estou usando para me preparar para o próximo exame:

Dado é o idioma $ ext{Goto}_{17}^c \subseteq ext{Goto}$.Esta linguagem contém exatamente aqueles $ ext{Goto}$ programas em que não constante é sempre acima $17$ nem qualquer variável sempre acima $c$.

$Goto$ aqui descreve o conjunto de todos os programas escritos na $Goto$ linguagem composta dos seguintes elementos:

Com as variáveis $v_i \in \mathbb{N}$ e constantes $c \in \mathbb{N}$
Atribuição: $x_i := c, x_i := x_i \pm c$
Salto Condicional:se(Comparação) goto $L_i$
Haltcommand:parar

Atualmente, estou lutando com a formalização de uma prova, mas é isso que eu vim de tão longe, resumiu muito casualmente:Para qualquer programa deste conjunto de nós sabe que é finito.Um finito programa contém um número finito de variáveis e uma quantidade finita de estados, ou linhas para se estar.Como tal, há uma quantidade finita de configurações em que este processo pode ser.Se deixamos a execução do programa, pode-se manter uma lista de todas as configurações que temos visto.Isto é, a combinação de todas usado variável-valores e o estado do programa.Se deixarmos a execução do programa, deve haver uma de duas coisas que acontece, eventualmente:O programa pára.Neste caso, vamos voltar SIM e decidiram que ele pára.O programa atinge uma configuração que tenha sido gravado antes.Como o idioma é determinista, isto significa que temos de ter ido um loop completo que exatamente vai repetir agora.

Nenhum outro caso pode existir como que significaria que nós continue correndo sempre finito código, sem a repetição de uma configuração.Isso significa que depois de cada etapa, entre a nossa lista de infinito etapas, há uma nova configuração.Isto significa que há infinitas configurações, o que é uma contradição.

Isso está correto?Além disso, como mais uma prova formal olha se é?Se não, como seria correto prova olhar?

Answer 1

Há um número finito de estados diferentes (o conjunto de valores das variáveis e o contador de programa).O seu "limitado goto programas" são apenas um (sujo) de forma a descrever um determinista finitos autômato.

Ou apenas a razão que o programa de estados finitos, sem dúvida, é possível mapear todas as possíveis não-repetição de cálculos (por algo, como uma amplitude primeira pesquisa de gráfico de estados e vizinhos).