Big Step Semantics

We give a proof for the first bullet. The rest are similar. If \[ \langle \sigma, e \rangle \rightarrow^{*} \langle \sigma', n\rangle \] then, we have a series of transitions of length \(\geq 1\) \[ \langle \sigma, e \rangle \rightarrow \langle \sigma'', e'' \rangle \rightarrow \langle \sigma''', e''' \rangle \cdots \rightarrow \langle \sigma', n \rangle \]

Now, how will we transform \(\langle \sigma, e + e_2 \rangle\) into \(\langle \sigma', n + e_2\rangle\)? Well, first, we know that \(\langle \sigma, e \rangle \rightarrow \langle \sigma'', e'' \rangle\) is a premise of \(\text{LAdd}\). So we can apply \(\text{LAdd}\) in order to reach the conclusion: \[ \langle \sigma, e + e_{2} \rangle \rightarrow \langle \sigma'', e'' + e_{2} \rangle \] Now, starting from \(\langle \sigma'', e'' + e_2 \rangle\), we repeat until we have reached \(\langle \sigma', n + e_{2} \rangle\)

This just comes from the fact that \(\rightarrow^{*}\) is the transitive closure of \(\rightarrow\).

This will be a structural induction proof on the big step semantic rules. The predicate that we will be trying to prove is: \[ P(e) \overset{\triangle}{=} \langle \sigma'', e'' \rangle \rightarrow \langle \sigma, e \rangle \wedge \langle \sigma, e\rangle \Downarrow \langle \sigma', n \rangle \Rightarrow \langle \sigma'', e''\rangle \Downarrow \langle \sigma', n \rangle \] We'll write out how to do it for the case of the \(\text{Mul}\) big step semantics rule.

By the structural induction hypothesis, we have: \[ P(e_1) \overset{\triangle}{=} \langle \sigma'', e_1'' \rangle \rightarrow \langle \sigma, e_1 \rangle \wedge \langle \sigma, e_1\rangle \Downarrow \langle \sigma', n_1 \rangle \Rightarrow \langle \sigma'', e_1''\rangle \Downarrow \langle \sigma', n_1 \rangle \] and \[ P(e_2) \overset{\triangle}{=} \langle \sigma'', e_2'' \rangle \rightarrow \langle \sigma, e_2 \rangle \wedge \langle \sigma, e_2\rangle \Downarrow \langle \sigma', n_2 \rangle \Rightarrow \langle \sigma'', e_2''\rangle \Downarrow \langle \sigma', n_2 \rangle \] We want to prove \(P(e_1 * e_2)\): \[ P(e_1*e_2) \overset{\triangle}{=} \langle \sigma'', e'' \rangle \rightarrow \langle \sigma, e_1*e_2 \rangle \wedge \langle \sigma, e_1*e_2\rangle \Downarrow \langle \sigma''', n \rangle \Rightarrow \langle \sigma'', e''\rangle \Downarrow \langle \sigma''', n \rangle \] So, we assume that we have \(\sigma'',e''\) so that \(\langle \sigma'', e'' \rangle \rightarrow \langle \sigma, e_1* e_2 \rangle\). But looking at the small step semantics rules, there are only two transitions that match this form: \(\text{LMul}\) and \(\text{RMul}\). We handle the case for \(\text{LMul}\). The case for \(\text{RMul}\) is similar. In the case of \(\text{LMul}\), we have \(e'' \overset{\triangle}{=} e_1'' * e_2\), so \(\langle \sigma'', e_1'' * e_2 \rangle \rightarrow \langle \sigma, e_1 * e_2 \rangle\). For this conclusion, we must have the premise \(\langle \sigma'', e_1'' \rangle \rightarrow \langle \sigma, e_1 \rangle\).

By assumption (remember that we are proving an implication, so we need to assume the premises), we have \(\langle \sigma, e_1*e_2 \rangle \Downarrow \langle \sigma', n\rangle\). The premises which must hold for this conclusion include \(\langle \sigma, e_1 \rangle \Downarrow \langle \sigma', n_1 \rangle\). Then, by our inductive hypothesis, we have \[\langle \sigma'', e_1'' \rangle \Downarrow \langle \sigma', n_1 \rangle\].

The other premises that must hold for the conclusion of \(\text{Mul}\) is \(\langle \sigma', e_2 \rangle \Downarrow \langle \sigma''', n_2 \rangle\) and \(n = n_1*n_2\). These are still true. So together with the last line of the previous paragraph, by the \(\text{Mul}\) rule, we have \(\langle \sigma'', e_1'' * e_2 \rangle \Downarrow \langle \sigma''', n \rangle\). Which is what we wanted.