I was reading a paper about implementing the statistical programming language R on the JVM, and encountered this notation I haven't seen before (I'm not formally CS-trained). What is the name of notational style? I've seen it before in other papers--usually as it related to functional programming and the REPL. enter image description here

  • 1
    $\begingroup$ See here1 and Backus-Naur form. $\endgroup$ Commented Dec 7, 2013 at 7:11
  • $\begingroup$ I had seen BNF before (Odersky did it in the Functional Programming Coursera), but usually it was written out into words, so I figured this was something different. Please paste your comment into a full answer and I'll accept it. $\endgroup$ Commented Dec 7, 2013 at 7:56
  • 3
    $\begingroup$ I believe that the fraction notation for rules of inference was introduced by [R. Smullyan, Theory of Formal Systems, 1961]. See also en.wikipedia.org/wiki/Formal_system as a starting point. $\endgroup$ Commented Dec 7, 2013 at 11:16
  • 4
    $\begingroup$ actually, the fractional notation was used already in Gentzen's paper (1934) on natural deduction and sequent calculus, which I think (but am not 100% sure) is the original source. $\endgroup$ Commented Dec 7, 2013 at 13:52
  • $\begingroup$ Yes, I was wrong, sorry. Smullyan also said so here, in comments: youtube.com/watch?v=P8VBeGl9Law I had rather badly misinterpreted a remark in another paper. $\endgroup$ Commented Dec 7, 2013 at 21:57

2 Answers 2


It is notation for Formal Proofs and specification of language grammar in Backus-Naur Form.


The individual statements of the form $A\Rightarrow B$ are sequents and the things that look like fractions are inference rules.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.