COMP[39]161 Concepts of Programming Languages
Semester 2, 2018

Proof (Small Step and Big Step)

Table of Contents

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

Announcements RSS