0
$\begingroup$

This is taken from an old exam of my university that I am using to prepare myself for the coming exam:

Given is a language $\text{Goto}_{17}^c \subseteq \text{Goto}$. This language contains exactly those $\text{Goto}$ programs in which no constant is ever above $17$ nor any variable ever above $c$.

$Goto$ here describes the set of all programs written in the $Goto$ language made up of the following elements:

With variables $v_i \in \mathbb{N}$ and constants $c \in \mathbb{N}$
Assignment: $x_i := c, x_i := x_i \pm c$
Conditional Jump: if(Comparison) goto $L_i$
Haltcommand: halt

I am currently struggling with the formalization of a proof, but this is what I have come to so far, phrased very casually: For any given program in this set we know that it is finite. A finite program contains a finite amount of variables and a finite amount of states, or lines to be in. As such, there is a finite amount of configurations in which this process can be. If we let this program run, we can keep a list of all configurations we have seen. That is, the combination of all used variable-values and the state of the program. If we let the program run, there must be one of two things that happens eventually: The program halts. In this case, we return YES and have decided that it halts. The program reaches a configuration that has been recorded before. As the language is deterministic, this means that we must have gone a full loop which will exactly repeat now.

No other case can exist as that would mean that we keep running forever on finite code without repeating a configuration. This means after every step, among our list of infinite steps, there is a new configuration. This would mean that there are infinite configurations, which is a contradiction.

Is this correct? Furthermore, how would a more formal proof look if it is? If not, how would a correct proof look?

$\endgroup$
  • $\begingroup$ Please define what Goto$_{17}^c$ represents in the question and what Goto represents. $\endgroup$ – D.W. Jul 19 at 8:16
  • $\begingroup$ @D.W. Everything should be in order now. $\endgroup$ – Vladis Becker Jul 19 at 8:35
  • $\begingroup$ The text of your question does not contain the question you are trying to answer or the theorem you are trying to prove. Please edit to provide that information. $\endgroup$ – D.W. Jul 19 at 8:42
  • $\begingroup$ We discourage "please check whether my answer is correct" questions, as only "yes/no" answers are possible, which won't help you or future visitors. See here and here. Can you edit your post to ask about a specific conceptual issue you're uncertain about? As a rule of thumb, a good conceptual question should be useful even to someone who isn't looking at the problem you happen to be working on. If you just need someone to check your work, you might seek out a friend, classmate, or teacher. $\endgroup$ – D.W. Jul 19 at 8:43
  • $\begingroup$ I really fixated on the constants part of this and missed the part where it mentioned that variables also can't go above 17. That's actually the critical part here. Even if constants could be as large as possible, as long as variables somehow can only ever by 17 at most the theorem holds. $\endgroup$ – Jake Jul 20 at 20:34
2
$\begingroup$

There is a finite number of different states (the set of values of the variables and the program counter). Your "limited goto programs" are just a (messy) way to describe a deterministic finite automaton.

Or just reason that the program states being finite, it is certainly possible to map out all possible non-looping computations (by something like a breadth first search of the graph of states and neighbours).

| cite | improve this answer | |
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.