Julin S (Apr 16 2022 at 16:18): Julin S (Apr 16 2022 at 16:18):Hi. I was going through the small step semantics illustrated with Coq at https://github.com/coq-community/semantics/blob/master/little.v
There I am having trouble understanding one of the constructors.
It's a type representing a small step evaluation for a loop:
| SOS4 :
forall r b i, beval r b true ->
sos_step r (while b i) (sequence i (while b i)) r
With type annotations:
| SOS4 :
forall (r:env) (b:bexpr) (i:instr), beval r b true ->
sos_step r (while b i) (sequence i (while b i)) r
(where bexpr denotes a boolean expression.
So this constructor represents the case where the condition for the loop is still true.
How can we be sure that the environment remains same after the execution of the instruction i?
That's what this constructor indicates, right?
Given an environment r, loop condition b and instruction i as the loop body, result would be the _same_ environment.
What am I missing here?
Li-yao (Apr 16 2022 at 16:31):The instruction i has not been executed yet.
Julin S (Apr 16 2022 at 16:35):Maybe a dumb question, but when will i be evaluated?
Li-yao (Apr 16 2022 at 16:39):At the next step.
while b i -> sequence i (while b i) -> sequence i' (while b i) -> ... -> sequence skip (while b i) -> while b i
Ah.. I think I get it now. Thanks!
Notification Bot (Apr 16 2022 at 16:41):Julin S has marked this topic as resolved.
Last updated: Apr 19 2024 at 16:01 UTC