# evan_tech

12:30 am, 14 Oct 03

### do my homework

So we're using this toy language in class, that has code like
x := 4; if x (y := 3); ntimes y (x := x + 1); while 1 (x := 2)
(ntimes e (s) runs statements s e times; getting the value of an undefined variable just gives you zero)

You can present programs theoretically with two values: H, representing the initial state of the variables, s, representing the program (where "s1; s2" is a statement, so s is just a statement).

Part of one of the questions on the assignment was to prove/disprove the following (where "H ; s" means "s with the context of H"):

For all H, e, and s, if H ; s terminates, then H ; ntimes e (s) terminates.
For all H, e, and s, if H ; ntimes e (s) terminates, then H ; s terminates.

I know I haven't provided much, but the language behaves pretty much as you'd expect. Can you prove or provide counterexamples? (I'm pretty sure of my answers, but they weren't what I/Albert expected.)

I thought it was interesting, anyway.

•  Slightly bored and this caught my interest. I think I'm right :)1)Let H be: x = 1, and e = 2Let s be:if x = 1 ( x := 2 );else ( loop_forever )then H ; s would terminate, but H ; ntimes e (s) would not. 2)This depends on how ntimes works. If ntimes actually decrements e before executing the statements Let H be: e = 5, x = 0Let s be: if e = 5 ( loop forever )ntimes e ( if e = 5 ( loop forever ) )As e becomes 4 before executing s, H ; ntimes e (s) will terminate.Executing s by itself will leave e at 5 so H ; s will not terminate.If ntimes decrements e after executing s, or if ntimes is a macro that simply writes s out e times and executes that code, then the statement is true. H;s is simply the same as the first iteration of H ; ntimes e (s). If H ; ntimes e (s) terminates, then certainly the first iteration terminates. reply to this
•  For 1) .. what he said :) For 2) .. well, logically, if ntimes e (s) terminated, then the first iteration must have terminated, therefore running the same statement only once *in the same context* must terminate. reply to this
•  2) A good observation. The loophole I found was that ntimes needn't necessarily run the statement even once.more discussion reply to this
•  Good point. Perhaps the answer is "true for all e > 0" :) reply to this
•  1) Good show. About an hour or so after supposedly "proving" this, the counterexample occurred to me and I then found the flaw in my proof.The trick is noting that H can change over the iterations.A simpler example is just:H = x=0s = if x (loop forever); x := 12) Regardless of how ntimes behaves:H = (whatever)s = loop forevere = 0Without the ntimes, it loops forever, but with it, it finishes immediately.The next part of the problem was:For all e, and s, if for all H, H ; s terminates, then H ; ntimes e (s) terminates.And I think that is true and came up with a sloppy proof. But judging from my success in the first one, I'm not sure whether it's any good. reply to this
•  I hadn't thought of that for the second one. Very nice. A very questionable counterexample... I doubt e is meant to be considered a modifiable variable, but why not :)let e = 2let s beif e > 2 ( loop forever ); e := 100Running s once works fine, but the second time through it will loop forever. reply to this 