How does one prove that Big Step semantics and Small Step semantics are equivalent for IMP?

Question

I know there is this paper but I wanted to do a special case proof for just IMP for fun. So the theorem is:

$$ \langle P , \sigma \rangle \to_{Big} \langle \{ \} , \sigma' \rangle \iff \exists N \in \mathbf N: \langle P , \sigma \rangle \to^N_{Small} \langle \{ \} , \sigma' \rangle $$

in words; the program P in state $\sigma$ evaluates to the empty block IFF there exists a certain number of small step steps inference steps that arrives us to the same configuration, the empty program in state $\sigma'$. Note $\langle P, \sigma \rangle$ stands for a program configuration with state $\sigma$. I am assuming both small step and big step have the same sort of configuration, which might be a big assumption and hard to formalize in real code...

I am happy with just an outline/sketch since a rigurous proof might be too much work probably and I'd rather get something than nothing.

I want to focus on $\Rightarrow$ (big to small). I think one of my main difficulties is finding such an $N$ that works. But conceptually to me I think I would break the proof by induction on the program P. The program has 6 constructors/cases:

1. Empty Block {}
2. Block B which is just $\{ S \}$
3. Assignments $x = AExp ;$
4. Sequences $S_1 ; S_2$ where $S_i$ is a statement.
5. while statements $ While \ (BExp) \ do \ S $.
6. ifElse statements $If \ (BExp) \ do \ S_1 \ Else \ S_2 $.

for the first case 1) its simple we have $\langle \{ \} , \sigma' \rangle$ on the RHS for big step and on the LHS $\langle \{ \} , \sigma' \rangle$ for small step, which are the same configuration. Done.

3) For the case assignment case we have to show that the AExp expressed uin the semantics, say big step or small step evaluates to the same as the "aeval" function that recursively just evaluates a real arithmetic expression. Not sure how I can make this more rigorous but at least it is a start.

Things with Boolean expression in them also need the same beval equivalence with boolean evaluation equivalence in their corresponding semantics.

However when things involve statements I am honestly not sure what one would need to argue to show they are equivalent. Do we do induction again on each statement and then proceed by apply the inference rules as many times as possible and show they evaluate to the same final state and empty block? Or what does one need to do? Then especially, how does one find the $N$?

---

The inference rules I had in mind are just any standard IMP semantics:

• http://fsl.cs.illinois.edu/images/b/b3/CS522-Spring-2011-PL-book-bigstep.pdf
• http://fsl.cs.illinois.edu/images/6/65/CS422-Spring-2015-02c-SmallStep.pdf
• https://softwarefoundations.cis.upenn.edu/plf-current/Smallstep.html
• http://www.cs.cornell.edu/courses/cs6110/2009sp/lectures/lec05-fa07.pdf
• http://web.cse.ohio-state.edu/~bond.213/6341/Operational-6.pdf
• https://www.seas.harvard.edu/courses/cs152/2010sp/lectures/lec03.pdf

Answer 1

Don't proceed by induction on $P$, i.e. by structural induction on the syntax of programs. This is because structural induction is quite weak, and is likely to fail on while loops.

Look at the inference rules for the big step semantics for while, in particular at the while-true rule which handles the case where the guard is true. In such case, you'll see that in one of the premises we have the same while loop. Roughly, the rule defines the behaviour of while in terms of itself.

(I didn't check your own rule, and used mine instead, but it should be simple to adapt the reasoning to yours.)

$$ \dfrac{ \sigma\models \phi \quad \langle c, \sigma \rangle \to_b \sigma' \quad \langle while\ \phi\ do\ c, \sigma' \rangle \to_b \sigma'' }{\langle while\ \phi\ do\ c, \sigma \rangle \to_b \sigma''} $$

If we proceed by structural induction, when we handle such case, we only get an induction hypothesis for $c$, wince it is a subterm of $while\ \phi\ do\ c$. That however provides no help in coping with he last premise involving the $while$ itself.

The solution is to use the induction principle generated by the rules for $\to_b$, instead. Doing that, when handling the rule above, we have two induction hypotheses, namely that the small step semantics

1. reduces $\langle c, \sigma \rangle$ to some $\sigma'$ state in some $N$ steps
2. reduces $\langle while\ \phi\ do\ c, \sigma' \rangle$ to some $\sigma''$ state in some $M$ steps

Exploiting those properties, it is possible to show that, using (something like) $N+M+1$ steps, we can reduce $\langle while\ \phi\ do\ c, \sigma \rangle$ to $\sigma''$ using small steps.

The other rules can be handled in a similar way.

When you write such proofs, I strongly suggest to always check the while-true case first, since that's the "hardest". Checking it first helps avoiding wasting effort on other simpler (but long) cases, only to discover that the proof can not be completed and all the work done has to be thrown away.

---

Assume we have these as the inference rules for the big step semantics. (If rules omitted) $$ \begin{array}{c} \dfrac{ }{\langle skip, \sigma \rangle \to_b \sigma} \qquad \dfrac{ \langle e, \sigma \rangle \to_e v }{\langle x:=e, \sigma \rangle \to_b \sigma[x\mapsto v]} \\ \dfrac{ \langle c_1, \sigma \rangle \to_b \sigma' \qquad \langle c_2, \sigma' \rangle \to_b \sigma'' }{\langle c_1;c_2, \sigma \rangle \to_b \sigma''} \\ \dfrac{ \sigma\models \lnot\phi \quad }{\langle while\ \phi\ do\ c, \sigma \rangle \to_b \sigma} \qquad \dfrac{ \sigma\models \phi \quad \langle c, \sigma \rangle \to_b \sigma' \quad \langle while\ \phi\ do\ c, \sigma' \rangle \to_b \sigma'' }{\langle while\ \phi\ do\ c, \sigma \rangle \to_b \sigma''} \end{array} $$

We immediately get the following induction principle.

Let $p(c,\sigma,\sigma')$ be any property of a command and two states. To prove that $$ \forall c,\sigma,\sigma'.\ \langle c \sigma \rangle \to_b \sigma' \implies p(c,\sigma,\sigma') $$ it suffices to check all of the following:

1. $\forall \sigma.\ p(skip,\sigma,\sigma)$
2. $\forall x,e,\sigma,v.\ \langle e, \sigma \rangle \to_e v \implies p(x:=e, \sigma, \sigma[x\mapsto v])$
3. $\forall \sigma,\sigma',\sigma''.\ p(c_1, \sigma, \sigma') \land p(c_2, \sigma', \sigma'') \implies p(c_1;c_2, \sigma, \sigma'')$
4. $\forall \phi,c,\sigma.\ \sigma\models \lnot\phi \implies p(while\ \phi\ do\ c, \sigma, \sigma)$
5. $\forall c,\phi,\sigma,\sigma',\sigma''.\ \sigma\models \phi \land p(c, \sigma, \sigma') \land p(while\ \phi\ do\ c, \sigma', \sigma'') \implies p(while\ \phi\ do\ c, \sigma, \sigma'')$

Note that in item 4 we get the induction hypotheses on the subterms, very much like what would happen using structural induction.

In step 5, instead, we get both an induction hypothesis on the subterm $c$, and (crucial!) another induction hypothesis on the $while$ itself (on different states).

For your case, choose a suitable property $p(c,\sigma,\sigma')$ such as "there is some natural $N$ for which $c,\sigma$ terminates in $N$ small steps in stale $\sigma'$".