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