5
$\begingroup$

I'm reading a computer science paper, this one: https://arxiv.org/abs/1608.03960. It uses certain notation in one of the illustrations (Figure 9, page 8 in the PDF version) that I don't understand how to interpret. Attaching here as well for better visibility:

$$ \text{EXEC} ~ \frac{\text{cmd}_1 : \text{CMD} \quad A_p, \text{cmd}_1 \implies A^\prime_p}{A_p, \langle \text{cmd}_1 ~ ; ~ \text{cmd}_2 ~ ; \ldots \rangle \implies A^\prime_p, \langle \text{cmd}_2 ~ ; \ldots \rangle} $$

I've tried to search for this online, but haven't come up with anything. I'd appreciate if someone explain it to me, particularly these questions:

  1. Does this notation has an official or widely recognized name?

  2. What's the relationships between expression above and below the horizontal line?

  3. What's the meaning of $\Rightarrow$, long arrow?

  4. What's the meaning of two expressions being separated by a comma, as in $A_p, cmd_1$? How is it different from two expressions separated by a blank space, as in $$\mathrm{cmd}_1, \mathrm{CMD}\ \ \ \ \ \ \ \ A_p, \mathrm{cmd}_1\,?$$

Here's another example from the paper:

$$ \text{VAR} ~\frac{x \in \text{dom}(A_p)}{A_p, x \implies A_p(x)}$$

  1. What's the meaning of $dom(A_p)$ here?
$\endgroup$
  • 1
    $\begingroup$ Look up "inference rule". Usually the rule is used to "inductively" define something by listing the "premises" above the line and stating the "consequence" under the line. Alternatively, in a relative less common case, the rule could also be use to define "coinductively". BTW, I definitely remember seeing another question on this site asking basically the same thing but on different document. $\endgroup$ – Apiwat Chantawibul Nov 12 '17 at 1:05
  • 1
    $\begingroup$ The long arrow is likely the relation being defined. With out me looking at the original paper. I read: "if there is a command called $ cmd_1$ and it is known that $ A_p, cmd_1$ relates to $ A'_p $ then the relation below must also holds. $\endgroup$ – Apiwat Chantawibul Nov 12 '17 at 1:17
  • $\begingroup$ @Billiska thanks for your response. I'm still having problems understanding the notation, unfortunately. I'll update the question with further points that are not clear. $\endgroup$ – Haspemulator Nov 12 '17 at 9:44
5
$\begingroup$

Answering your questions one by one:

  1. The rules are part of an operational semantics, which defines how to evaluate expressions.
  2. The notation with the horizontal line is an inference rule: if all the logical statements above the line are true, then you can conclude that the statement below the line is also true.
  3. The arrow is a predicate that indicates that the left hand side can be evaluated (or reduced) to the right hand side.
  4. The expressions separated by a comma form a tuple; for example, $A_p, cmd_1$ is a pair consisting of $A_p$ and $cmd_1$.
  5. $\mathrm{dom}(f)$ returns the domain of the function $f$, that is, the set of values $x$ for which $f(x)$ is defined.

In these rules, $A_p$ is a state object: a function that maps variable names to values. (Think of it a bit like the heap on which you can allocate objects, and where the variable names are pointers.) The VAR rule performs variable lookup in that state:

  • If the statement above the line is true: $x \in \mathrm{dom}(A_p)$, that is, the function $A_p$ is defined for the argument $A_p(x)$,
  • Then the statement below the line is true: $A_p, x \Longrightarrow A_p(x)$, that is, the expression $x$ in the state $A_p$ can be evaluated to $A_p(x)$, which is just the value of the function $A_p$ when you pass in the variable name $x$ as argument.

Hope that helps. For more details, lecture notes on operational semantics (e.g. these from Cambridge) will further explain the notation.

$\endgroup$
4
$\begingroup$

The expressions are in the general form of sequents, which are a way of writing down proofs. A rule of the form

$$\frac{\ X\ }{Y}$$

means that, if you can prove that $X$ is true, then you've proven that $Y$ is true. A word written to the left or right of the rule is just that rule's name. As such, proofs are read from the bottom. It's also possible to have multiple statements on the top line, as in $$\frac{\ X_1\quad X_2\ }{Y}\,.$$ This means that proving both $X_1$ and $X_2$ proves $Y$. The meaning is the same as $$\frac{\ X_1\land X_2\ }{Y}$$ but the point is that, in a full proof, you'll need to supply separate proofs of $X_1$ and $X_2$: $$\frac{\ \frac{\ \vdots\ }{X_1}\quad \frac{\ \vdots\ }{X_2}\ }{Y}\,.$$ Written out in a little more detail, you might have $$\frac{\ \frac{\ \vdots\ }{X_1}\quad \frac{\ \vdots\ }{X_2}\ }{\frac{\ X_1\land X_2\ }{Y}}\,,$$ which means the following. I have some proof of $X_1$ (which is just written as dots) and some proof of $X_2$ (ditto). This allows me to conclude that $X_1\land X_2$ is true and, from that, I can conclude $Y$. I think that covers your questions 1, 2 and half of 4. Your remaining questions are about the specific logic used in the paper, and I'll leave that to somebody with domain expertise.

$\endgroup$
  • $\begingroup$ Thanks, this clarifies some of the points. However, the point no.3, about the meaning of long arrow, is a crucial one that stops me from completely understanding the paper. Ideally, I'd like to know how the first expression from my question (one named EXEC) is read in plain English. I hope this will be enough to understand the rest of examples. $\endgroup$ – Haspemulator Dec 14 '17 at 14:56
1
$\begingroup$

Sorry for my inability to recall a better resource, plus I did not want to write out a textbook.

Here is a book which I learned the concept from using a hard copy of: Introduction to Bisimulation and Coinduction by Davide Sangiorgi

Luckily, I found a lecture slide which is based on that book. Take a look starting from page 56 titled "Mathematical induction".

$\endgroup$

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.