[Solved]: Double, down facing arrow in operational semantics

With starting state $s$, program $M$ evaluates to $P$ and the resulting state is $s’$.

This is a very general framework for expressing the operational semantics of a program, and it means that if you can build a finite derivation tree with $s vdash MDownarrow P, s’$ at the base, then you have shown that the program $M$ is well-defined and evaluates to $P$. Let’s give an example. Say $s$ is the state in which variable $b$ is sent to true and $n$ is sent to $2$, which I will write ${bmapsto mathrm{true}, nmapsto 2 }$. Then the following should be derivable: $${bmapsto mathrm{true}, nmapsto 2 }vdash mathrm{if} b mathrm{then} n+1 mathrm{else} 0 Downarrow 3, {bmapsto mathrm{true}, nmapsto 2 }$$ Note that in your question, the rule: $$frac{s_0 vdash M_1 Downarrow P_1, s_1 ; … ; s_{n-1} vdash M_n Downarrow P_n, s_n}{s_0 vdash M Downarrow P, s_n}$$ Means:

If, starting from state $s_0$, $M_1$ reduces to $P_1$ and new state $s_1$, and starting with state $s_1$ $M_2$ reduces to $P_2$ and new state $s_2$ etc. then starting from state $s_0$, $M$ reduces to $P$ with new state $s_n$.

In particular, the order in which you do the reduction is important: the state may change after the evaluation of $M_1$, which in turn will influence the evaluation of $M_2$, etc. This is why in a language with state (side-effects), the order of evaluation of arguments passed to a function is important: we may get a different result depending on which argument we evaluate first. In Haskell, laziness makes it impossible to know which arguments will be evaluated first (or at all!), so having side effects is pretty much out of the question. I suggest reading the classic Types and Programming Languages, by Benjamin Pierce, which treats all of this in much detail.