Example 6.5.2 - Question about [Subst]

Unbenannt

Why do we use only [Scope] in the first step, but [Scope][Subst] in the third step? From looking at it, it seems like it’s basically the same step. Thanks for your answers in advance

Jannik

Because the second occurrence is inside of a block.
Whenever you have a block, there are only limited options:

  • [Exec], when the first instruction in that block is executed
  • [Subst], when the first instruction in the block is replaced with another one
  • [Empty]
  • [Scope] when we have a block with variable declarations

So, in the first occurrence, we have a single block with variable declarations which we need to handle. We use [Scope].

In the second occurrence, we first need to deal with the outer block. Since the rule we want to apply for the inner block is [Scope], which replaces the block with a modified one, the correct rule for the outer block is [Subst].

If you’re still not sure about this, it might be helpful to draw derivation trees for each step.

1 Like

Just so I understand correctly, whenever we do anything in a block, not only do we use whatever rule is needed to execute the next step, but we “implicitily” replace the block by a new block that is the same one as before but with whatever changes we made by the other rules we used.

well, not implicitly! that’s why we need [Subst] :wink:

Consider a block {a = 1; b = 2; c = 3;}.
The first statement is an assignment, and, by itself, would step to just a state with no remaining code.
Therefore, the block steps to {b = 2; c = 3;} (by [Exec]).

So the statement {a = 1; b = 2; c = 3;} steps to {b = 2; c = 3;}.
You’ll note that we started with one statement and ended up with a different one!

If this happens within an outer block, we then need [Subst] for the outer block because we substituted the first statement in that block ({a = 1; b = 2; c = 3;}) with its result after one step ({b = 2; c = 3;}).

All of this happens because our semantics rules are defined on single statements only. When this statement is a block, our rules say how the block behaves based on how its statements would behave. However, we still need to use the rules for blocks (as listed above) in addition to the inner ones.

We can’t just magically make changes to our statement and declare that this is okay, we need to have a rule which allows this!

Ok I understand, thanks. That’s why i said “implicitily”, still the wrong wording i guess :sweat_smile: Basically what i meant to say is when we want to execute the first statement of a block we won’t get around the substitution, thus the substitution is “implied”. Just for clarificationd :smiley: