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

Problem Detail: 

What is the meaning of the double, down facing arrow $\Downarrow$ in the context of operational semantics? Here's the example formula that uses it:

$$\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}$$

It would be also beyond priceless if you could explain in words what do other pictograms of this formula mean. I feel that $\vdash$ here doesn't mean what it usually means in logic (is provable from). However the general form of this formula is the derivation rule (I can understand it from the context). It is a rather general derivation rule though (it is followed by few other more specific examples which use all the same pictograms).

The source of the formula: On Exceptions versus Continuation in the Presence of State by Hayo Thielecke. It cites several other sources, but I couldn't find the explanation of the symbols used.

Asked By : wvxvw

Answered By : cody

The language of inference rules are much more general than what is usually given in Logic. Indeed you can look at systems with rules of the shape

$$ \frac{\Theta_1\ldots \Theta_n}{\Theta}$$

Where the $\Theta_i, \Theta$ are some kind of statement and ask: what are all the possible $\Theta$ I can get by repeated application of these rules?

In the above case, $s \vdash M \Downarrow P, s'$ expresses the statement:

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 M\Downarrow 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 $\{b\mapsto \mathrm{true}, n\mapsto 2 \}$. Then the following should be derivable:

$$\{b\mapsto \mathrm{true}, n\mapsto 2 \}\vdash \mathrm{if}\ b\ \mathrm{then}\ n+1\ \mathrm{else}\ 0 \Downarrow 3, \{b\mapsto \mathrm{true}, n\mapsto 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.

Best Answer from StackOverflow

Question Source : http://cs.stackexchange.com/questions/16201