Bring the homework to class or email it to rjsimmon@cs.
Writing up this assignment (LaTeX, Word, ASCII, whatever) is HIGHLY
ENCOURAGED. If you think you have perfect handwriting and want to try handing
in a handwritten assignment, you are welcome to try, but you'll only get one
chance.
I have also made a version of this assignment,
along with proofs of all the lemmas, available
here.
This file is essentially a very explicit written proof that can be
checked by the SASyLF proof checker.
You do NOT need to use SASyLF, you do not need to learn
SASyLF. Take a look or ignore at your choosing.
Addition language syntax
In the first two classes, we worked with an exremely simple expression language
with the following syntax:
e ::= n | e + e
Big step transition
In the first class, we looked at a "big-step" definition of how to evaluate
any such expression to a number.
I am using
e => e' instead of the down-facing arrow (LaTeX \Downarrow)
because ASCII doesn't have that symbol.
e1 => n1
e2 => n2
n1 + n2 = n3
------------------ eval-plus
e1 + e2 => n3
------------------ eval-num
n => n
Small step transition
In the second class, we considered the following "small-step" definition of
how to evaluate numbers to values. First, we had to define what a value was,
which only takes one rule if we only have one kind of a value!
----------- val-num
n value
... and then we could define the small-step transition relation.
I am using
e -> e' because I think
e |-> e' is ugly in ASCII, LaTeX uses \mapsto.
e1 -> e1'
-------------------- step-plus1
e1 + e2 -> e1' + e2
e1 value
e2 -> e2'
-------------------- step-plus2
e1 + e2 -> e1 + e2'
n1 + n2 = n3
-------------------- step-plus
n1 + n2 -> n3
Multi-step transition
We also talked about how to define the
reflexive-transitive closure of the step relation:
-------------------- multi-z
e ->* e
e1 -> e2
e2 ->* e3
-------------------- multi-s
e1 ->* e3
Assignment:
Prove: if
e => e' (big step), then
e ->* e' (little step).
You can use the following five lemmas without proving them;
however, you
should be able
to prove all five lemmas yourself. One is straightfowardly true, the
other four are true by induction.
- If e1 -> e2 and e2 ->* e3 then e1 ->* e3 (step-star)
- If e1 ->* e2 and e2 -> e3 then e1 ->* e3 (star-step)
- If e1 ->* e2 and e2 ->* e3 then e1 ->* e3 (star-star)
- If e1 ->* e1', then e1 + e2 ->* e1' + e2 (compat-plus1)
- If e1 value and e2 ->* e2', then e1 + e2 ->* e1 + e2' (compat-plus2)