4
$\begingroup$

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.

$\endgroup$
6
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ Thanks, I've actually red Pierce's book, but he doesn't use this particular symbol :) At least not in the chapters that I remember. But now, I think that this is what he would call a "big evaluation step", is that correct? (sorry, I might be a little blurry on terminology, but I think there were two ways to do reduction, one in minimal discrete steps and the other one in "big" steps). $\endgroup$ – wvxvw Oct 18 '13 at 19:09
  • $\begingroup$ Yes as lewellen says, this is a "big-step". Note that abstract machines are usually closer in their description to big-step semantics, but small-step semantics are more suited to certain kinds of mathematical analysis (like termination). $\endgroup$ – cody Oct 18 '13 at 20:35
  • 1
    $\begingroup$ Pierce mostly (or exclusively) uses small step reduction semantics because these are more suitable for type soundness proofs. $\endgroup$ – Dave Clarke Oct 18 '13 at 20:52
3
$\begingroup$

There are two systems of operational semantics: small-step and big step. The symbol $\Downarrow$ is used in the latter to denote "this term evaluates to that final value". E.g., $t \Downarrow v$. There is a short discussion of the system in Pierce's Types and Programming Languages pages 42-43.

The $\vdash$ is used to imply that if the types on the left hand side are true, then the ones on the right hand side can be derived. Further explanation is given in Pierce's book.

$\endgroup$
  • $\begingroup$ Oh, thanks, I've not seen your answer before I commented on cody's answer. Yes, I have the book, but I've only skimmed through it a while ago. $\endgroup$ – wvxvw Oct 18 '13 at 19:14

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.