Sheet 7, Task 7

In the solution, the [While] rule is applied without [Subst]. Why is that the case? Thanks!

Take a look at the while rule in Definition 6.3.4: Operational Semantics of C0:

\frac{}{\langle \text{while}(e)~s \mid \sigma \rangle \to \langle \text{if} (e) ~\{s~\text{while} (e)~s\} \text{ else } \{\} \mid \sigma \rangle }[\mathsf{While}]

This rule simply says: When evaluating the program (stepping through the execution), we evaluate the while by evaluating a condition where the consequence is the block with the body and the while again and the alternative is the empty block.
More naturally (and looking ahead in the execution): If the expression holds, execute the body and then repeat and go back to the while statement as we might not be done yet. Otherwise, there is nothing to do (a while where the condition is wrong is not executed).

This is the whole rule to evaluate the statement.

In comparison, the [Subst] rule applies to blocks:
If we want to evaluate a block of statements, we first take a step in the first one for evaluation.
If we no longer transform the first statement stepwise. That is, we are done with it and have evaluated it to the “end”, we apply the [Exec] rule which does the last finished step. Afterward, we are left with the remaining statements in the block for further execution.

The fundamental difference is that the [While] rule tells us how to transform the while statement to do execution steps there and the [Subst] rule tells us how to do steps in a block.

Your confusion might stem from the fact that both rules often appear together.
This is due to the fact, that we often have [While] statements in blocks.
If we have a block and the first statement of the block is a while, we usually execute [Subst] to say: to execute this block of statements, look at the first one (the while) and let’s see how we can do further execution steps in this statement.
Then we use the [while] rule to do the transformation step from the while to the if.
The resulting block will now have the if as the first statement of the block and awaits further execution.

Due to the rules, we also introduce blocks that need additional [Subst] rules later on.
For instance, every time we continue execution in a while, we add a block with the consequence of the if.

2 Likes

Because we are not in a block, so we do not need [Subst] to work inside that block since again, there is no such block.

I again recommend drawing the inference tree. It looks like this:

image

No [Subst] needed, since the while statement is the top-level statement when drawing the syntax tree.

2 Likes