12:30 am, 14 Oct 03

### do my homework

So we're using this toy language in class, that has code like

(

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.

`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.

daeva1)

Let H be: x = 1, and e = 2

Let 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 = 0

Let 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.

billemonFor 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.

evanmore discussion

billemonevanThe trick is noting that H can change over the iterations.

A simpler example is just:

H = x=0s = if x (loop forever); x := 1

2) Regardless of how ntimes behaves:

H = (whatever)

s = loop forever

e = 0

Without 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.

daevaA very questionable counterexample... I doubt e is meant to be considered a modifiable variable, but why not :)

let e = 2

let s be

if e > 2 ( loop forever ); e := 100

Running s once works fine, but the second time through it will loop forever.