Re: regular expression operators in CF grammars

The auhtor(s) of SLK Parsers write:
> Correctness proofs for good algorithms are usually not that difficult.


While in most cases, this is true. In the case of ELR parsers, it is
not. In fact, if you read the posting from Sönke Kannapinn, you could
conclude that most (if not all) ELR parsing papers have serious flaws
in their algorithms and proofs.


> Would you be surprised to learn that 4 of 22 grammars were
> misclassified in the Ph.D. thesis on which one of these tools was
> based?


No, I would not. In my experience, most papers have a few errors,
occassionally serious ones. However, in most of such papers, the
errors do not actually detract from the correctness of the result if
one is willing to do the work to independently validate and correct
the flaws. As far as I can tell academic papers are just like
programs, they need to be debugged. The only difference is that when
a program is debugged, usually the corrected version replaces the
previous flawed one, with papers the errata is rarely available.


> This would be a compelling argument for EBNF if we could be sure
> that the method produces correct results.


Hmmm, and therein lies the rub. I believe the relevant quote from
Knuth goes something to the effect, "beware this program may have bugs
as I have only proven it and not tested it" which must be paired with
the quote "testing can only prove the existence of bugs and never
their absence".


The fact is that my favorite ELR parser generator uses unpublished
algorithms that differ in some substantial ways from any of the
published ones. It also implements combinations of features that are
not present anywhere else. I have reason to believe that
fundamentally the algorithms that it uses are sound and correct.
However, I know they have never been entirely nor rigorously proven,
especially not in the combination that they are used together in
Yacc++, but that is the price for doing things that no one has ever
tried.


And, of course, it would be better if Yacc++ had a stronger more
rigorous theoretical footing, epsecially if that footing eliminated
some bugs. However, it is more important (in my estimation) that
Yacc++ be extended to solve those problems where there isn't yet a
complete solution.


But, that's just my opinion.....
-Chris


*****************************************************************************
Chris Clark Internet : compres@world.std.com
Compiler Resources, Inc. Web Site : http://world.std.com/~compres
3 Proctor Street voice : (508) 435-5016
Hopkinton, MA 01748 USA fax : (508) 435-4847 (24 hours)
------------------------------------------------------------------------------

Return to the comp.compilers page.
Search the comp.compilers archives again.