What is this fraction-like "discrete mathematics"–style notation used for formal rules?

Question

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

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?

Answer 1

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.

Answer 2

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.