2
$\begingroup$

I'm following this document on on how to prove strong normalization for the simply typed lambda calculus. I understand how this proof works. The if-case of the proof is left to the reader as an exercise. I tried to solve this exercise, but I'm quite confused on how to continue.

This is what I've found by now:

Case:
$$\cfrac{ \Gamma\vdash e:\mathtt{bool}\qquad \Gamma\vdash e_1:\tau\qquad\Gamma\vdash e_2:\tau} {\Gamma\vdash \mathtt{if}\ e\ \mathtt{then}\ e_1\ \mathtt{else}\ e_2:\tau}$$

We know that $\gamma \vDash \Gamma$. Now we have to prove that $SN_\tau(\gamma(\mathtt{if}\ e\ \mathtt{then}\ e_1\ \mathtt{else}\ e_2))$ holds. By the definition of substitution we know that this is equivalent to proving that $SN_\tau(\mathtt{if}\ \gamma(e)\ \mathtt{then}\ \gamma(e_1)\ \mathtt{else}\ \gamma(e_2))$ holds.

The induction hypothesis tells us that $SN_{bool}(e)$, $SN_\tau(e_1)$ and $SN_\tau(e_2)$ holds.

But how can I continue from here?

PS: These are some of the definitions I've used.

$SN_\tau$ is a logical predicate. It is defined as follows:

$SN_{bool}(e) \equiv \bullet \vdash e : bool \space \land \space e \Downarrow$

$SN_{\tau_1\to\tau_2} \equiv \bullet \vdash e \land \space e \Downarrow \space \land \space (\exists e')(SN_{\tau_1}(e') \implies SN_{\tau_2}(e \space e')) $

$e \Downarrow \space \equiv (\exists v)(e \space \Downarrow \space v)$

$e \Downarrow v \equiv e \mapsto^\star v$

$\endgroup$
  • 1
    $\begingroup$ It would be convenient if you inlined the relevant definitions so people don't need to search through a 42 page document for them. $\endgroup$ – Derek Elkins Dec 14 '17 at 17:03
  • $\begingroup$ @DerekElkins I've included the relevant definitions in the question now $\endgroup$ – Pieter Verschaffelt Dec 14 '17 at 18:07
1
$\begingroup$

First, notice that the inductive hypothesis actually tells us that $\mathrm{SN}_{\mathit{bool}}(\gamma(e))$, $\mathrm{SN}_{\tau}(\gamma(e_1))$ and $\mathrm{SN}_{\tau}(\gamma(e_2))$ hold.

Since we know that $\mathrm{SN}_{\mathit{bool}}(\gamma(e))$ holds, by the definition of $\mathrm{SN}_{\mathit{bool}}$ we know that $\gamma(e) \Downarrow$. By the definition of $\gamma(e) \Downarrow$, we know that there exists a value $v$ such that $\gamma(e) \mapsto^* v$. Now you can proceed by case analysis on $v$.

For instance, suppose that $\gamma(e) \mapsto^* \mathrm{true}$. Then, by the evaluation rules we have that $\mathtt{if}\; \mathrm{true}\; \mathtt{then}\; \gamma(e_1)\; \mathtt{else\;} \gamma(e_2) \mapsto \gamma(e_1)$. By the inductive hypothesis, $\mathrm{SN}_{\tau}(\gamma(e_1))$ holds. Therefore $\mathrm{SN}_{\tau}(\mathtt{if}\; \gamma(e)\; \mathtt{then}\; \gamma(e_1)\; \mathtt{else\;} \gamma(e_2))$ holds by the lemma (SN preserved by forward/backward reduction).

$\endgroup$
  • $\begingroup$ Thank you very much! I understand how it works now :) $\endgroup$ – Pieter Verschaffelt Dec 16 '17 at 17:45

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.