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?
DOCrule doesn't have anything in its "numerator" — why not?
GETrules appear to have two separate terms above the line, what does that mean?
VARrule 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?