Re: Verified compilers?

["Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>]

On Thu, 08 Mar 2012 20:02:25 +0200, Niklas Holsti wrote:

> On 12-03-07 22:17 , Dmitry A. Kazakov wrote:
>> On Wed, 07 Mar 2012 19:49:04 +0200, Niklas Holsti wrote:
>>
>>> On 12-03-07 11:12 , Dmitry A. Kazakov wrote:
>>>
>>>> I was always wondering why people bother to study grammars, LR, LL parsers
>>>> and other useless stuff.
>>>
>>> Grammars and the notion of parsing (derivations) rigorously define what
>>> a given string of characters means, in some formally defined language.
>>
>> No. A grammar defines some formal language: a set of strings.
> 
> Ok, I was being too brief. You are right that a grammar defines a 
> language. But notice that I was also speaking of parsing and 
> derivations, not just grammars.
> 
> If you want to define the meanings of the sentences of a language in a 
> rigorous way, you have basically two options:
> 
> 1. Define the meaning operationally, by giving a standard interpreter, a 
> black box, for example a Turing machine, that accepts the language, and 
> define that the actions of that machine, while reading a sentence, are 
> the meaning of that sentence. (From your point of view, the meaning 
> could be the "translation" that appears on the output tape.)
> 
> 2. Define the meaning mathematically in some way. Note that by 
> "mathematically" I don't necessarily mean formally proven math, but 
> mathematically precise definitions with the usual amount of hand-waving 
> and shortcuts.

1 and 2 are same to me. In all cases it is an input for some machine. An
inference system based on Peano axioms or whatever, is no less a machine
than the Turing one. The only difference is in the computational power of
such machines.

> As far as I know, all methods -- formal or informal -- for defining the 
> meaning of sentences in formal languages are based on how the sentence 
> is derived, or equivalently how it is parsed.

No. 1234 has the same meaning for Ada parser, human reader and an OCR
system.
 
> How else could you explain why "2*3+4*5" means 26, and not 70, nor 
> something else?

Explain? It is a subject of proof. There are more than one way to do it.
BTW the "meaning" you are advocating for looks rather something like
23*45*+.

> In practice, the role of the parse/derivation tree appears in the fact 
> that parser/compiler generators let you attach "semantic actions" to 
> grammar productions, and often help you to consider larger parts of the 
> derivation by passing information around the parse/derivation tree in 
> well-defined ways. Attribute grammars are one example.

Parsing tree is just a less ambiguous representation of the program. You
don't even need to generate it in order to evaluate 2*3+4*5 using a finite
state machine. And you certainly do not need it when using your head or
calculator.

>> The grammar defines only syntax.
> 
> No, it also defines the structure, through the parse/derivation tree.

I was talking about formal languages. Do you want to say that the trace of
productions applied during parsing is the program semantics?

It is amusing to read how LRM Annex P tries to describe operator precedence
by syntactical means. This is a remnant of a delusion shared by some that
formal languages could describe, if not natural languages, but at least
machine languages. I thought nobody seriously believes in this now. Care to
carve a grammar where

   declare
      X : Integer := 1.0 + 2;

would be a syntax error?

I took my journey in the opposite direction. If you look at the grammar:

   http://www.dmitry-kazakov.de/ada/components.htm#12.2

It has just one production rule.

>> Furthermore the merits of formal grammar definitions are debatable, because
>> the complexity of grammar descriptions usually make it impossible to judge
>> if a given string do belong to the formal language or not.
> 
> Entirely wrong. Can you give an example of this impossibility?

Are you claiming that if I gave you a random set of production rules and a
random string you could tell me [in 30 seconds time] if that string belongs
to the language?

>> Maybe, but they are totally irrelevant for the grammars of real programming
>> languages.
> 
> No, they are relevant. For example, you want limited look-ahead to make 
> parsing fast, and for most "little languages" for which you implement a 
> parser manually, you want the language to be suitable for recursive 
> descent parsing.

Really? Comp.compilers is busy with silly questions how do I modify the
grammar [a list of productions follows] to parse [a description] by parser
X. How is this activity different from programming? People willingly choose
a bad programming language [of productions] for what reason? Why not to do
parser straight in Ada? I do.

>> On one hand these classes do not capture real differences
>> between syntaxes of programming languages.
> 
> What sort of "real differences" do you mean?

Like between C++ and Ada.

>> On the other hand, the classes
>> they do describe have no other practical interest than torturing students
>> of CS classes.
> 
> I don't want to become too personal, but have you had a Horrible 
> Experience with some poor formal-languages class that has left a 
> permanent scar in your mind? My wife had something like that; she was 
> among the first students of computer science in our university, and the 
> teachers at that time were also beginners. I think most of the students 
> were mystified by the course.

No. Actually I enjoyed the subject for its simplicity compared to "hard"
mathematics, and for its elegance too. I have a weakness to all sorts of
formalisms, which is typical to Russian mathematical school. My major was
mathematics.

I didn't want to become a programmer, it just happened to me during 5th or
6th semester. That time I was exposed to the classical Aho and Ullmann.
"Ahoullmann" we called it, which in Russian has a frivolous connotation,
though with a note of awe and respect. This fully applied to me, I could
not believe my eyes. Is it really so bad? How anybody could do anything out
of this horror?

I was saved by David Gries. He is a really great man, who deserves all
possible fame and respect. His book on compiler construction opened my
eyes. Another great book that shaped my attitude to formal languages was
Griswold, Poage, Polonsky introduction to SNOBOL4. It helped me to
understand what patterns actually are, and ultimately, why all of them,
even the ones of SNOBOL are bad.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de