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$ Dec 7 '13 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$ Dec 7 '13 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$ Dec 7 '13 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$ Dec 7 '13 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$ Dec 7 '13 at 21:57

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, privacy policy and cookie policy

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