Theorem: All expressions contain a constant or variable. Proof: By induction on the height of an arbitrary expression e. Base case: Height h = 0 If an expression has height 0, it's a variable or a constant. Therefore it contains one. Inductive case: Height h > 0 If an expression e has height h > 0, then it is either e1+e2 or e1*e2 for some e1 and e2. In either case, e1 has height at most h-1. So by induction e1 has a constant or variable. So so does e. Proof: By induction on the structure of an arbitrary expression e. There are four cases: If e is a variable, then it contains a variable or constant. If e is a constant, then it contains a variable or constant. If e is e1+e2 for some e1, then by induction e1 contains a variable or constant. So so does e. If e is e1*e2 for some e1, then by induction e1 contains a variable or constant. So so does e. ====================================================== EvalsTo(H,e,c) // a more conventional and wordy relation metasyntax ====================================================== In answer to a question about making our language nondeterministic e ::= ... | random ------------------- H ; random V c ====================================================== Theorem: For all H and e there is exactly one c such that H;e V c. Proof: By induction on the structure of e. Case: e is a constant: Then the only rule that applies is Const. And exactly one constant, namely e, can be produced. Case: e is a variable: Then the only rule that applies is Var. And exactly one constant, namely H(e), can be produced. Case: e is e1+e2 for some e1 and e2: Then the only rule that applies is Add. And e1 and e2 are smaller expressions. So by induction there is exactly one c1 and exactly one c2 such that H;e1 V c1 and H;e2 V c2. Blue-plus produces exactly one constant for any c1 and c2. Case: e is e1*e2 for some e1 and e2: Then the only rule that applies is Mult. And e1 and e2 are smaller expressions. So by induction there is exactly one c1 and exactly one c2 such that H;e1 V c1 and H;e2 V c2. Blue-times produces exactly one constant for any c1 and c2. ============================================================== An alternate approach to small-step inference rules for while H; e V c c <= 0 H; e V c c > 0 ---------------------- ------------------------------- H; while e s -> H; skip H; while e s -> H; s; while e s