Re: Verified compilers?

[Niklas Holsti <niklas.holsti@tidorum.invalid>]

On 12-03-08 11:25 , Dmitry A. Kazakov wrote:
> On Wed, 7 Mar 2012 18:42:23 -0600, Randy Brukardt wrote:
>
>> As far as LR parsing is concerned, that's the most general practical parsing
>> scheme. There are many legitmate BNFs that cannot be parsed using recursive
>> descent.
>
> There are also ambiguous BNFs, which means that BNF is not so formal as it
> may appear.

Ambiguity has nothing to do with formality.

If you think of a grammar only as defining a language (a set of 
strings), ambiguity is irrelevant; it only means that some sentence can 
be derived in more than one way from the start symbol, but that has no 
effect on the language, as a set of strings.

Ambiguity is only harmful when you want to use the grammar to parse a 
sentence into a parse/derivation tree, and then want to use the tree for 
something, for example to evaluate the meaning of the sentence.

If you define (as one always does) the meaning of a sentence as a 
mathematical function of the sentence's parse tree, and if (because of 
ambiguity) the sentence has several parse trees, the meaning also 
becomes ambiguous -- unless you can prove that the "meaning function" 
has the same value for all the parse trees for the same sentence.

> The point is that I don't care about that or about restricting
> it to a certain class etc. Because there is no value in such activity at
> all. BNF is good for *informal* description of the language syntax.

There is nothing informal about BNF, if it is used correctly.

-- 
Niklas Holsti
Tidorum Ltd
niklas holsti tidorum fi
       .      @       .