2
$\begingroup$

I'm doing a course in Computer Programming Languages and I'm trying to prove the following (roughly following Pierce's Types and Programming Languages book):

if $t \rightarrow^* t'$ then $if\; t\; then \; t2 \; else \; t3 \rightarrow^* if\; t'\; then \; t2 \; else \; t3$

I'm a little confused about where to start; as far as I know, I'm supposed to define a base case, then prove it via induction.

I've started my proof by assuming these base cases:

$P(\frac{}{true \rightarrow^* true})$ and $P(\frac{}{false \rightarrow^* false})$.

I'm stuck at this point, and I don't really how know to proceed.

edit: I've added the syntax in an effort to clear things up.

Snapshot of semantics provided

$\endgroup$
  • 3
    $\begingroup$ Presumably this is talking about a small-step semantics (but how are we to know which), and thus the title is rather misleading. Without knowing the semantic rules, we can only guess what you are looking at. That said, I would use induction over the length over the reduction sequence $t\to^*t'$. $\endgroup$ – Dave Clarke Feb 7 '15 at 9:43
4
$\begingroup$

The induction should be on the derivation of $t \to^* t'$:

  • If $t \to t'$ in one step, then we get the desired result by the E-IF rule.

  • Suppose $t \to^* t'$ because $t \to t'' \to^* t'$. By the E-IF rule we have $$(\mathtt{if}\;t\;\mathtt{then}\;t_2\;\mathtt{else}\;t_3) \to (\mathtt{if}\;t''\;\mathtt{then}\;t_2\;\mathtt{else}\;t_3)$$ and by the induction hypothesis $$(\mathtt{if}\;t''\;\mathtt{then}\;t_2\;\mathtt{else}\;t_3) \to^* (\mathtt{if}\;t'\;\mathtt{then}\;t_2\;\mathtt{else}\;t_3).$$ These two together give us the desired $$(\mathtt{if}\;t\;\mathtt{then}\;t_2\;\mathtt{else}\;t_3) \to^* (\mathtt{if}\;t'\;\mathtt{then}\;t_2\;\mathtt{else}\;t_3).$$

$\endgroup$

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.