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$
1
  • 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$ Feb 7, 2015 at 9:43

1 Answer 1

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$

This site is temporarily in read-only mode and not accepting new answers.

Not the answer you're looking for? Browse other questions tagged .