PL QE2015
Claim
For all expression , state
and
, and integer
.
If then there is a state
,
.
Proof
First if we take a close look of the rule here, this semantic is a undeterministic semantic, which means each original step may cause 2 different state, to be more clear in claim actually means a set of state because in rule
Choice ' s side condition we can clear see 2 different state generated at same time. In following proof we will assume this. If you think in claim just means a particular state then this claim not hold when in rule
Choice contain environment change expression.
Induction on derivation of original semantic ():
Num,Varare trivial base case,are not changed which means there is always
(satisfy
ANumandAVar)make claim holdsIncis also a trivial base case. we can always findmake claim holds.
Addis an inductive case, in this case by this rule we can know, we can know in the
(similar for
)created by the step result of
, there must exist some
, which
can step to. so all precedence in rule
aAddis true, and we can apply this step rule to find some-
Choiceis interesting case.by inductive hypothesis we can know that if
then we can have
, meanwhile by the rule of this semantic it is not hard to see, this semantic has progress properties, which means express
will not stuck at somewhere so we can always evaluate
have
. Then we can apply rule
aChoiceand if we letin the inference of
aChoice, and letin
Choicerule we can found, there is always a, 2 different semantic agree on, and at this time we can find a
. Claim hold.
so because of above all cases we can see claim holds.
