9
$\begingroup$

Usually I see that in the structural operational semantics representation for the while loop, the program state don't change:

$(while \> B \> do \>S, \sigma) \rightarrow (if \>B \> then \>S; (while \> B \> do \>S) \> else \> SKIP, \sigma)$

For me, this not intuitive, if the state don't change (i.e. the status of the memory stays the same) then $B$ will continue to stay true and the program will never terminate.

Can anyone please explain why the state don't change in this rule?

Improve this question
$\endgroup$
1
  • $\begingroup$ Note that this is only correct if we can assume that $B$ does not have side-effects. This is not true in most programming languages. $\endgroup$
    – Raphael
    Commented Oct 17, 2016 at 8:59

3 Answers 3

Reset to default
10
$\begingroup$

In programming language semantics, the notion of program state is not a vague philosophical notion, but a very precise mathematical one. A state $s$ in this small-step operational semantics is a partial function

$$ s : \mathbf{Var} \hookrightarrow \mathbb{Z} $$

that records the values of the variables. So if $s\, x = v$, then variable $x$ has value $v$. The state is necessarily a partial function, since it only makes sense to record the values of variables that actually occur.

The unfolding axiom

$$ \langle \texttt{while}\; b\; \texttt{do}\; S,s \rangle \Rightarrow \langle \texttt{if}\; b\; \texttt{then}\; S; \texttt{while}\; b\; \texttt{do}\; S \; \texttt{else skip},s \rangle$$

is simply telling us that we unfold a while-loop into a conditional statement, one of whose branches contains the loop. No variables will change their value because of this, and for this reason the state does not change.

Improve this answer
$\endgroup$
10
$\begingroup$

The state can change in subsequent reduction steps because on the right hand side of

$$ \langle while\ B\ do\ S, \sigma \rangle \quad\rightarrow\quad \langle if\ B\ then\ ( {\color{red}{S}};\ while\ B\ do\ S )\ else\ skip, \sigma\rangle $$

the $while$-loop is guarded (preceeded) by $S$. The computation of $S$ may change the state so that the condition $B$ can evaluate to $\mathsf{false}$.

Improve this answer
$\endgroup$
2
  • $\begingroup$ So, this means that the state change should be expressed in other rules to which S could be potentially reduced in a concrete program? $\endgroup$
    – El Marce
    Commented Oct 16, 2016 at 12:32
  • $\begingroup$ @ElMarce Yes. I suggest to go through a simple example e.g. $x := 2;\ while\ x > 0\ do\ x := x - 1$ and see how this works. $\endgroup$
    – Martin Berger
    Commented Oct 16, 2016 at 12:47
9
$\begingroup$

The state $\sigma$ does not change when we consider $B$ to decide whether to perform one iteration of the loop, but it can change later when we run the body $S$. And so, the next time we consider $B$, there can be a change of $\sigma$.

Improve this answer
$\endgroup$
4
  • $\begingroup$ This explanation, while essentially correct, does not refer to what states are (namely a function that tells us the values of varialbes) and what a state change signifies (namely that the value of at least one variable changes). $\endgroup$
    – Hans Hüttel
    Commented Oct 17, 2016 at 18:42
  • $\begingroup$ Indeed, it is irrelevant what states are or how they are implemented for the purposes of my answer. The explanation holds regardless. And moreover, it is actually wrong to say that "states are really functions" because theat is only one way to model them mathematically. There are other possible models. And let us not confuse mathematical models with how hardware works. $\endgroup$
    – Andrej Bauer
    Commented Oct 17, 2016 at 18:52
  • $\begingroup$ But the question is concerned with a specific small-step operational semantics, for which the notion of a state is well-defined. $\endgroup$
    – Hans Hüttel
    Commented Oct 17, 2016 at 18:54
  • $\begingroup$ I never said it was not. I am just saying that your remark is unecessary, because my explanation holds without explicit mention of how state is modelled. Perhaps you detected that the OP did not know that state was a map from variables to values. Good for you, you got your answer accepted, and I did not. Congratulations. Why you are now forcing your mode of answer on me is beyond my comprehension. Why precisely do you feel the need to make my answer be like yours? My answer makes sense without the remarks that you think are necessary. Perhaps someone will come by looking for my answer one day. $\endgroup$
    – Andrej Bauer
    Commented Oct 17, 2016 at 18:57

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.