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
andGET
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?