0
$\begingroup$

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!

$\endgroup$
0
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ thank you for your answer. I think I figured it out already, using the same approach as you suggested. $\endgroup$ – trojan Apr 4 '14 at 16:47

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.