Exercise sheet 7 question 1

grafik
whats the reason for the multiple [subst] after the third line?
i dont understand why its 3 substitutions instead of one
is it because of the brackets that get added with each while loop ?

Hi,

yes, the [Subst] rule says that you are replacing the first statement inside a block by another. A block is also a statement itself. So, if you have nested blocks and something changes in the inner block (for example, by a subst), then you have not only changed the first statement in the inner block, but also the inner block itself. Therefore, you have also changed the first statement in the outer block (which is the inner block), which again must be done by using [Subst]. So once you have multiple nested block statements, you probably need multiple [Subst] as well.
A good thing is, that we have a shortcut for this: instead of writing [Subst] n times, you can also just write [Subst]^n.

Hope this answered the question.
Lisa :smiley:

1 Like

In general, if confused about the number of [Subst]s, draw an inference tree.

For the state with three [Subst]s, this looks like this:

image

As you can see, we need three [Subst]s to unwrap all the blocks.

1 Like