# Definition of "deterministic" semantics in While language

I came across this definition in my book but I'm not sure that I understand it correctly.

Isn't this the same as saying: $$\langle S, s\rangle \rightarrow s = \langle S, s\rangle \rightarrow s$$ implies that $$s=s$$? Why do they use a different prime symbol here even though they are the same statement $$S$$ being executed on the same state $$s$$.

2nd Question: How does this statement by the author above allow us to "uniquely determine a final state s' if (and only if) the execution of S terminates"

I think I'm missing the point here because this definition came after Induction on the Shape of Derivation Trees.

3rd Question: How will this proof help us perform induction on the shape of derivation trees?

• 1st Equality of a state with itself is implicit, the statement would be silly.
– user16034
May 15, 2023 at 6:16
• 2nd This is a definition, there is nothing "allowed".
– user16034
May 15, 2023 at 6:17
• Please heed How to reference material written by others. May 15, 2023 at 14:39

## 1 Answer

I've come back to this as I solved it but forgot to post my reasoning. The statement above simply states that if we execute a statement S on a state s twice, the resulting state should be the same. Hence, we can "determine" the final result unambiguously.