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

Problem Detail: 

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?

Asked By : natevw

Answered By : RmS

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.

Best Answer from StackOverflow

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