Evan Martin (evan) wrote in evan_tech,
Evan Martin

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.

  • socks5 proxying flash via ssh

    Suppose you're in Germany and want to watch some Flash-based videos that are IP-limited to the US for whatever reason. At first you'd think you could…

  • use chrome as your emacs browser

    The emacs-configured browser is used for operations like previewing your markdown buffer ( markdown-preview; C-c C-c p in markdown-mode). I still…

  • recovering a disk clobbered with dd

    I managed to accidentally dd 600mb over my primary disk; I haven't done that in many years. Adam thankfully pointed out that my data should be…

  • Post a new comment


    default userpic
    When you submit the form an invisible reCAPTCHA check will be performed.
    You must follow the Privacy Policy and Google Terms of use.