Semester 2, 2018

# Proof (Small Step and Big Step)

Here are the rules for our two semantics for arithmetic expressions.

First, the small step rules:

$\small \newcommand{\Plus}[2]{(\mathtt{Plus}\ #1\ #2)} \newcommand{\Times}[2]{(\mathtt{Times}\ #1\ #2)} \newcommand{\Let}[2]{(\mathtt{Let}\ #1\ #2)} \newcommand{\Num}[1]{(\mathtt{Num}\ #1)} \newcommand{\smapsto}{\stackrel{\star}{\mapsto}} \dfrac{ e_1 \mapsto e_1' }{\Plus{e_1}{e_2} \mapsto \Plus{e_1'}{e_2} }{S_1}\\ \dfrac{ e_2 \mapsto e_2' }{\Plus{\Num{n_1}}{e_2} \mapsto \Plus{\Num{n_1}}{e_2'} }{S_2}\\ \dfrac{ }{\Plus{\Num{n_1}}{\Num{n_2}} \mapsto \Num{(n_1 + n_2)} }{S_3}\\ \dfrac{ e_1 \mapsto e_1' }{\Times{e_1}{e_2} \mapsto \Times{e_1'}{e_2} }{P_1}\\ \dfrac{ e_2 \mapsto e_2' }{\Times{\Num{n_1}}{e_2} \mapsto \Times{\Num{n_1}}{e_2'} }{P_2}\\ \dfrac{ }{\Times{\Num{n_1}}{\Num{n_2}} \mapsto \Num{(n_1 \times n_2)} }{P_3}\\ \dfrac{ e_1 \mapsto e_1' }{\Let{e_1}{(x.\ e_2)} \mapsto \Let{e_1'}{(x.\ e_2)} }{L_1}\\ \dfrac{ }{\Let{\Num{n_1}}{(x.\ e_2)} \mapsto e_2[x := \Num{n_1} ] }{L_3}$

And the big step rules:

$\dfrac{ } {\Num{n} \Downarrow n}{N} \\ \dfrac{ e_1 \Downarrow v_1 \quad e_2 \Downarrow v_2} {\Plus{e_1}{e_2} \Downarrow (v_1 + v_2)}{S} \\ \dfrac{ e_1 \Downarrow v_1 \quad e_2 \Downarrow v_2} {\Times{e_1}{e_2} \Downarrow (v_1 \times v_2)}{P} \\ \dfrac{ e_1 \Downarrow v_1 \quad e_2[x := \Num{v_1}] \Downarrow v_2} {\Let{e_1}{(x.\ e_2)} \Downarrow v_2}{L} \\$

Now, to prove them equivalent, we have to prove two directions, to show that $$s \smapsto \Num{n}$$ iff $$s \Downarrow n$$, where $$\smapsto$$ (the reflexive transitive closure) indicates zero or more steps:

$\dfrac{ } {e \smapsto e}\mathsf{refl}\quad \dfrac{e \mapsto e' \quad e' \smapsto e''} {e \smapsto e''}\mathsf{trans}$

## 1 If $$s \Downarrow v$$ then $$s \smapsto \Num{v}$$

We will proceed by rule induction on the cases where $$s \Downarrow v$$.

### 1.1 Base Case ($$s = \Num{n}$$), from $$N$$

We must show that $$\Num{n} \smapsto \Num{n}$$, obvious by rule $$\mathsf{refl}$$.

### 1.2 Inductive Case ($$s = \Plus{e_1}{e_2}$$), from $$S$$

We know that $$e_1 \Downarrow v_1$$ and $$e_2 \Downarrow v_2$$, which gives us the inductive hypotheses:

• $$\mathsf{IH}_1$$ – $$e_1 \smapsto \Num{v_1}$$
• $$\mathsf{IH}_2$$ – $$e_2 \smapsto \Num{v_2}$$

Showing our overall goal:

\begin{array}{lclr} \Plus{e_1}{e_2} & \smapsto & \Plus{\Num{v_1}}{e_2} & \text{($\mathsf{IH}_1$ with $S_1$)}\\ & \smapsto & \Plus{\Num{v_1}}{\Num{v_2}} & \text{($\mathsf{IH}_2$ with $S_2$)}\\ & \smapsto & \Num{(v_1 + v_2)} & \text{($S_3$)} \end{array}

### 1.3 Inductive Case ($$s = \Times{e_1}{e_2}$$), from $$S$$

Extremely similar to $$\mathtt{Plus}$$, above.

### 1.4 Inductive Case ($$s = \Let{e_1}{(x.\ e_2)}$$), from $$L$$

We know that $$e_1 \Downarrow v_1$$ and $$e_2[x:=\Num{v_1}] \Downarrow v_2$$, which gives us the inductive hypotheses:

• $$\mathsf{IH}_1$$ – $$e_1 \smapsto \Num{v_1}$$
• $$\mathsf{IH}_2$$ – $$e_2[x:=\Num{v_1}] \smapsto \Num{v_2}$$

Showing our overall goal:

\begin{array}{lclr} \Let{e_1}{(x. e_2)} & \smapsto & \Let{\Num{v_1}}{(x. e_2)} & \text{(rule $L_1$ with $\mathsf{IH}_1$)} \\ & \smapsto & e_2[x := \Num{v_1}] & \text{($L_2$)} \\ & \smapsto & \Num{v_2} & \text{($\mathsf{IH}_2$)} \end{array}

Thus, by mathematical induction, we have shown one direction of the equivalence.

## 2 If $$s \smapsto \Num{v}$$ then $$s \Downarrow v$$

Doing rule induction on the assumption $$s \smapsto \Num{v}$$ leads to two cases.

### 2.1 Base case ($$s = \Num{v}$$), from $$\mathsf{refl}$$

We know that $$\Num{v} \Downarrow v$$ from rule $$N$$.

### 2.2 Inductive case ($$s \mapsto s'$$ and $$s' \smapsto \Num{v}$$), from $$\mathsf{trans}$$

We have the inductive hypothesis that $$s' \Downarrow v$$, so it suffices to prove the following lemma in order to discharge this case.

$\dfrac{s \mapsto s' \quad s' \Downarrow v}{ s \Downarrow v }$

## 3 Lemma: If $$s \mapsto s'$$ and $$s' \Downarrow v$$ then $$s \Downarrow v$$.

Written as a logical statement, this lemma is:

$\forall v.\ s \mapsto s' \land s' \Downarrow v \Rightarrow s \Downarrow v$

Equivalently, this can be stated as:

$s \mapsto s' \Rightarrow \forall v.\ s' \Downarrow v \Rightarrow s \Downarrow v$

This formulation lets us proceed by rule induction on the assumption $$s \mapsto s'$$, proving for each case for any arbitrary $$v$$:

$\forall v.\ \dfrac{s' \Downarrow v}{s \Downarrow v}$.

### 3.1 Base case from rule $$S_3$$

Here $$s = \Plus{\Num{n}}{\Num{m}}$$ and $$s' = \Num{n + m}$$.

We have to show that $$\Plus{\Num{n}}{\Num{m}} \Downarrow v$$ assuming that $$\Num{n + m} \Downarrow v$$. The only way that assumption could hold, looking at the rules of $$\Downarrow$$, is if $$v = n + m$$ from rule $$N$$. Therefore we must show that $$\Plus{\Num{n}}{\Num{m}} \Downarrow n + m$$, which is trivial from rules $$S$$ and $$N$$.

### 3.2 Inductive case from rule $$S_1$$

Here $$s = \Plus{e_1}{e_2}$$ and $$s' = \Plus{e_1'}{e_2}$$. We know that $$e_1 \mapsto e_1'$$, giving the inductive hypothesis that:

$\forall v.\ \dfrac{e_1' \Downarrow v}{e_1 \Downarrow v}{\mathrm{IH}}$

We must show that $$\Plus{e_1}{e_2} \Downarrow v$$ assuming that $$\Plus{e_1'}{e_2} \Downarrow v$$. Looking at the rules for $$\Downarrow$$, the only way that $$\Plus{e_1'}{e_2} \Downarrow v$$ could hold is if $$v = x + y$$ and $$e_1' \Downarrow x$$ and $$e_2 \Downarrow y$$ (by rule $$P$$). By the inductive hypothesis, we have that $$e_1 \Downarrow x$$. Therefore, $$\Plus{e_1}{e_2} \Downarrow v$$ as required.

### 3.3 Inductive case from rule $$S_2$$

Here $$s = \Plus{\Num{n}}{e_2}$$ and $$s' = \Plus{\Num{n}}{e_2'}$$. We know that $$e_2 \mapsto e_2'$$, giving the inductive hypothesis that:

$\forall v.\ \dfrac{e_2' \Downarrow v}{e_2 \Downarrow v}{\mathrm{IH}}$

We must show that $$\Plus{\Num{n}}{e_2} \Downarrow v$$ assuming that $$\Plus{\Num{n}}{e_2'} \Downarrow v$$. Looking at the rules for $$\Downarrow$$, the only way that $$\Plus{\Num{n}}{e_2'} \Downarrow v$$ could hold is if $$v = n + y$$ and $$e_2' \Downarrow y$$ (by rule $$P$$). By the inductive hypothesis, we have that $$e_2 \Downarrow y$$. Therefore, $$\Plus{\Num{n}}{e_2} \Downarrow v$$ as required.

### 3.4 Cases for $$\mathtt{Times}$$

All analogous to the cases for $$\mathtt{Plus}$$.

### 3.5 Inductive case from rule $$L_1$$

Here $$s = \Let{e_1}{(x.\ e_2)}$$ and $$s' = \Let{e_1'}{(x.\ e_2)}$$. We know that $$e_1 \mapsto e_1'$$, giving the inductive hypothesis that:

$\forall v.\ \dfrac{e_1' \Downarrow v}{e_1 \Downarrow v}{\mathrm{IH}}$

We must show that $$\Let{e_1}{(x.\ e_2)} \Downarrow v$$ assuming that $$\Let{e_1'}{(x.\ e_2)} \Downarrow v$$. Looking at the rules for $$\Downarrow$$, the only way for that assumption to hold is if there is some $$v_x$$ such that $$e_1' \Downarrow v_x$$ and $$e_2[ x := \Num{v_x} ] \Downarrow v$$. By the inductive hypothesis we have that $$e_1 \Downarrow v_x$$ and therefore we have that $$\Let{e_1}{(x.\ e_2)} \Downarrow v$$ from rule $$L$$.

### 3.6 Base case from rule $$L_2$$

Here $$s = \Let{\Num{n}}{(x.\ e_2)}$$ and $$s' = e_2[x:=\Num{n}]$$. We must show that $$\Let{\Num{n}}{(x.\ e_2)}$$ assuming that $$e_2[x:=\Num{n}] \Downarrow v$$. This can be shown trivially by application of the rule $$L$$.

2018-11-16 Fri 19:37