18
$\begingroup$

In the paper "A Conflict-Free Replicated JSON Datatype", I encountered this notation for formally defining "rules":

Some of the "rules" shown in the paper][1

What is this notation called? How do I read it?

For example:

  • the DOC rule doesn't have anything in its "numerator" — why not?
  • the EXEC and GET rules appear to have two separate terms above the line, what does that mean?
  • the VAR rule stands out a bit as well, since while many other rules use some sort of arrow (which I would take to mean "implies") up top this one only seems to be saying that x is an element of something.
  • almost everything is peppered with an initial Ap, which the text describes as "the state of replica p is described by Ap, a finite partial function" — how would a savvy reader of this notation tend to "see" that part of every rule?

This site did suggest a related question that has some very similar-looking notation, over on the question What is the significance of ⟨B, s⟩ -> ⟨B', s'⟩ as the initial rule in this question about small-step semantics? — this is tagged as Operational semantics, and that does seem to be a strong lead. Is that indeed the framework under which I should be interpreting these figures? Could you easily summarize this in "crash course" form so that, even if I can't verify the correctness of their proofs, I could at least get a bit more understanding of what they are saying in this section?

$\endgroup$
25
$\begingroup$

This is a standard notation for an inference rule. The premises are put above a horizontal line, and the conclusion is put below the line. Thus, it ends up looking like a "fraction", but with one or more logical propositions above the line and a single proposition below the line. If you see a label (e.g., "LET" or "VAR" in your example) next to it, that's just a human-readable name to identify the particular rule.

You might also see this referred to as natural deduction or Gentzen-style natural deduction.

This is a common notation in the programming languages literature. You'll see it all over the place. It's very convenient for the kinds of conclusions and recursive-structured proofs that arise in that field.

You'll see this notation used to express axioms/rules. You can think of each axiom as a template with "meta-variables" (e.g., expr); you can replace each meta-variable with some syntax from the programming language (e.g., any expression that is valid in the programming language), and you'll get an instance of the rule. The inference rule promises that if all of the propositions are above the line are true (for some instance of the template, where you consistently replace each metavariable with the same value throughout the rule), then the proposition below the line will be true, too.

$\endgroup$
  • 2
    $\begingroup$ One notable use is specifying Hindley-Milner type inference: this answer to “What part of Milner-Hindley do you not understand?” walks through how to read and use that set of rules. $\endgroup$ – DylanSp Aug 18 '16 at 12:56
  • $\begingroup$ One small correction: the premises and conclusions are judgements, not propositions. Propositions are a specific form of judgement. Along those lines, judgements are evident, not true (because the notion of truth is difficult to define and not really of interesting for programming language semantics). $\endgroup$ – gardenhead Aug 18 '16 at 14:38
7
$\begingroup$

Here is a very informal explanation that might help people unfamiliar with formal notations to get a foot in the door. It does not replace a formal definition!

The Ap is the state of your system or your running program. "State" can mean a lot of things but in this case it seems to include a list of all defined local variables and their values. Why is Ap a function? Because that's a convenient way to express variable assignments: Ap(x) gives the value of variable x.

Now, let's take the rule EXEC as an example. It defines the semantics of executing a command cmd1 followed by a command cmd2, i.e., what happens with the state Ap of the system when executing cmd1 followed by cmd2.

  • Above the line: These are the premises. What they say: "Let cmd1 be a command. If you execute the command cmd1 when your system is in state Ap, your system will end up in a new state Ap'."
  • Below the line: Here the rule describes what it means to execute two commands cmd1 and cmd2 sequentially. What it says: "Assuming your system is in state Ap, executing cmd1 and then cmd2 means to execute cmd2 when your system is in state Ap'" (remember that Ap' is the state that you get after executing cmd1, as defined in the premises).

The other rules describe the semantics of the individual commands and expressions. For example, the VAR rule describes what it means to "execute" a variable: If x is a local variable (above the line), then what does it mean to evaluate/execute the variable x? It's written below the line: When your program is in state Ap, evaluating x gives you the value of x, i.e. Ap(x).

I hope that helps.

$\endgroup$
  • $\begingroup$ Thanks, this is a great help to understanding and exactly what I was looking for! However it does leave my first question unanswered: does this notation have a name, generally and/or in this particular context? My guess was "Operational semantics", but the other answer here so far says they are just plain "inference rules". I guess if I ask a two part question I deserve to get the answers split up, but now I'm torn between which one to accept :-) $\endgroup$ – natevw Aug 19 '16 at 16:53
  • 1
    $\begingroup$ @natevw They are inference rules. Operational semantics is just one of the many things that are commonly expressed with inference rules. $\endgroup$ – Gilles 'SO- stop being evil' Aug 19 '16 at 21:03

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.