My point was, that if you specify the Markdown grammar using PEG, you will mandate all implementers to use PEG toolchain (whichever they choose out of many) to build a conforming implementation.
Moreover, PEG-based parser generators produce extremely complex parsers which are very difficult to reason about for humans. Even parsers created using different PEG toolchains might have a different corner-case behavior because PEG grammar is not universally suitable to express Markdown syntax. See jgmâs comments above.
There was peg-markdown and lunamark output on Babelmark2 in the past. They are both based on PEG and even written by the same author (jgm) and yet I saw differences in their corner-case behavior. I cannot prove it now, because seemingly peg-markdown is not there anymore.
You cannot compare PEG with ABNF. ABNF is much easier to understand or implement a parser based on it.
Iâm not interested in ratholing on the relative merits of PEG versus other formalisms until weâve figured out which class of language STMD actually falls into. jgmâs complaint about âisnât the same as having a single PEG grammarâ is vacuous, because PEGs are closed under composition. Iâd have to compare the peg-markdown grammar and the lunamark grammar to determine why they have different corner-case behaviour, but the most likely reason is that theyâre not actually implementing the same grammar (the equivalence of two arbitrary PEGs is undecidable, so to be sure that theyâre implementing the same grammar, they have to express identical rules) and the next most likely reason is that the parser generators themselves differ in corner-case behaviour (typically having to do with differing opinions on how to handle left-recursion). Both of these are implementation flaws, not flaws in PEG itself. (If you want to argue that the fact that PEG generator implementors canât agree on how to handle left-recursion is a show-stopper, Iâll accept that.)
In any case, Iâve finished a preliminary pass on a mostly ABNF grammar; I say âmostlyâ because itâs more like an L-attributedboolean grammar, and RFC5234 doesnât have notation for attributes or for disjunction. Itâs still multi-stage, following the lines â blocks â inlines sequence described in the spec. Iâm going to do a second pass to make sure I got the precedences correct and sanity-check the rules for lists and blockquotes, and probably do a prototype in hammer, and then Iâll push to my fork.
Proving a grammar unambiguous is in the general case undecidable; Hopcroft, Motwani and Ullman show this by equivalence to the Post correspondence problem in Introduction to Automata Theory, Languages and Computation. But every language that can be parsed with a deterministic pushdown automaton is unambiguous, and IIRC there are some other techniques as well.
I read through your STOKE paper, and Iâm a little confused as to how transformation correctness would translate to this use case; is the generator function essentially the grammar itself? (I have a bad habit of thinking of grammars as discrete Markov chains, so I may be confusing myself.) Either way, though, itâs a really clever way of looking at the problem and I wouldnât mind exploring it further.
I think Iâve gotten this one down to an L-attributed boolean grammar (CFG plus conjunction and negation), and if I understand Okhotinâs paper correctly, it sounds like itâs actually fairly easy to determine whether a boolean grammar is ambiguous or not. (I might well be wrong here, though.)
Single word exclamation, accompanied by a gesture where the hand is swept palm down over the head from front to back with about three inches clearance.
Indicates that the post just read was too sophisticated for the reader and has gone âway over their headâ.
So admittedly, STOKE was never intended for parsing, but for compiler optimization (e.g. as an alternative to running GCC -O3). But the MCMC algorithm used in STOKE can be driven by basically any cost function, so it seems to me that if you made the cost function something like edit distance, then you could potentially find all ASTs which render to the same string (of which there should hopefully be exactly one).
Youâre right though that walking the space of ASTs is not so very different from doing a random walk over a CFG (or other grammar), so perhaps this doesnât provide any net benefit. Most likely, I have muddled my thinking. I guess my impression was that:
People here seem to be pessimistic about the feasibility of writing a formal grammar
On the other hand, walking the space of ASTs seems not so hard by comparison
And at any rate, the spec itself is phrased constructively (in terms of how to build blocks out of inlines and other blocks, etc.), so such an algorithm would have a convenient correspondence to the spec
I suspect the sticking point would probably be making sure that the transformation rules satisfy all the requirements for MCMC (e.g. ergodicity), which is easy enough with straight-line assembly and not so obvious with an arbitrary AST.
I will go read the Okhotin paper to try grok the rest of your posts, but I am hopeful that you will be successful.
I should have noted in my last post that MCMC itself is just an optimization; as long as you can enumerate all possible ASTs and render each one you can still write the algorithm⌠it might just take the rest of eternity to get around to the string you happen to be interested in parsing. I might give this a go to see exactly how hard it is and whether e.g. inline syntax makes this difficult.
Well, my thinking was, itâs certainly possible for a random walk (esp. w/MCMC, which I have played with a little and like a lot) to outperform a traditional parser for sufficiently complicated grammars. (âHow complicated?â is an interesting question and I wonder if anyoneâs investigated it.) Youâre right about ergodicity, though; Iâm going to have to chew on that one. I hope you do give it a try and Iâm interested to see your results.
Whatâs the status here? Does anyone currently work on a formal grammar? Has anyone tried and given up? If so, where was the main problem? Is there a more recent thread on this?
To me it looks as if the âmatch number of backticks resp. tildes, no matter how many there areâ specification of a fenced code block would be particularly difficult to express. Looking at the Wikipedia category âFormal Languagesâ for likely candidates, I found indexed grammars to be the most promising. One could use the index stack to count various kinds of things, most notably the number of characters in a code fence, or the number of spaces required to line up a list item. Counting two things in parallel (i.e. spaces and fence characters) would already be tricky, I think, so the translation would be far from obvious.
So far I know very little about indexed grammars. In particular I know of no tools making use of these, and I know of no methods to decide whether a given index grammar is ambiguous. So this may need some more research. If someone found a way to make standard context free grammars or something close to that work for CommonMark, that would of course be great, but I have my doubts.
In a comment on Vanilla-flavored Markdown as basis for state machine spec, @riking conjectured that CommonMark would have to be Chomsky 0. If that were indeed the case, indexed grammars would be bound to fail as well, since they are only Chomsky 1. However, I donât yet see the argument why this has to be Chomsky 0.
For the sake of completeness: Indian parallel grammars sounded like a good candidate for CommonMark as well. The parallel rewriting of non-terminals can be used to insert matching fences, or matching indentation at the beginning of lines. I canât see a way to forbid longer runs of backticks inside a fenced code block using this formalism, though. I know of no approach which would combine such parallelism with conjunctions.
@gagern Iâd love to have a formal grammar; I just donât know how to do it.
A while back I wrote a couple of PEG grammars for Markdown: peg-markdown (in C) and lunamark (in lua).
I had to work around various rough edges (the backtick code spans were one of them, and I think I just supported up through 5 backticks). Iâm not happy with either of these efforts.
Iâm not familiar with some of the more esoteric grammars you mention in your post, so if you want to investigate this, it would be welcome. I think itâs possible to use the Pumping Lemma to prove that the grammar for backtick code spans is not context-free.
Only because you specifically asked about me mentioning some formal grammar work: This was (long ago and not related nor updated to CommonMark) based using (ISO 14977 standard) EBNF, augmented with a simple parameterization facility, so that one can specify ârule schemesâ, so to say.
If youâre interested, drop me a line, to âmh, commercial at, tin-pot, full stop, netâ. [ I canât comment or post here. ]
I just started doing research in conjunction with my own attempt to write a CommonMark PEG grammar Lua, and ran across this attempt at an EBNF for CommonMark. At this point I have no idea about the completeness or correctness, but itâs clearly an interesting foray. It seems to have cropped up a month or two after the last activity in this thread.
I just started doing research in conjunction with my own
attempt to write a CommonMark PEG grammar
Lua, and ran across this attempt at an EBNF for
CommonMark.
At this point I have no idea about the completeness or
correctness, but itâs clearly an interesting foray. It seems to
have cropped up a month or two after the last activity in this
thread.
I can see at a glance that this is not even close to being right.
Just look at the rule for emphasis and compare to the commonmark
spec.
As someone who has written two PEG grammars for markdown
implementations (jgm/peg-markdown and jgm/lunamark on GitHub),
Iâm skeptical that this can be done for commonmark.
Iâm resurrecting a zombie thread for what might be a silly idea: For the backtick problem, how about we consider any consecutive backticks as a single token? For example, ````` (five backticks) would be considered as a single terminal symbol, say, `5. And we will have rule schemes like anything trapped inside two `ns will be considered as inline code blocks for any integer n >= 1. I havenât checked but this might be the same idea from what @tin-pod mentions as EBNF with parametrization. I wonder what could be other rough corners for formalizing CommonMark.