World's most popular travel blog for travel bloggers.

How to prove the following properties of Small-step semantics?

, , No Comments
Problem Detail: 

I have to prove the following 2 properties of the Small-step semantics of the WHILE programming language:

  • If $\langle C_1; C_2, s\rangle \rightarrow^k s'$ then there is a state $s''$ and natural numbers $k_1$ and $k_2$ such that $\langle C_1;s \rangle \rightarrow^{k_1} s''$ and $\langle C_2; s'' \rangle \rightarrow^{k_2} s'$ where $k_1 + k_2 = k$.
  • If $\langle C_1, s \rangle \rightarrow^k s'$ then $\langle C_1; C_2, s \rangle \rightarrow^k \langle C_2, s'\rangle$.

I am not quite sure which kind of induction I should use. I am not asking for a full proof, I would rather appreciate some hints on which kind of induction I should use in this case. Thanks in advance!

Asked By : trojan
Answered By : Martin Berger

I suggest to proceed by induction on $k$. For the inductive basis and step you'll have to look at all the possible cases that the relevant reduction step $\langle C, s \rangle$ can be derived.

Best Answer from StackOverflow

Question Source :

3200 people like this

 Download Related Notes/Documents


Post a Comment

Let us know your responses and feedback