Re: Verified compilers?

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

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.

The first "meaning ex machina" option is very undesirable, IMO, so we 
are left with the second option. Since most languages have an infinite 
number of sentences, of unbounded length, the only practical way to 
define the meaning of a sentence is by some form of induction. Induction 
based on the length of the string works only for some simple languages, 
such as the language of integer literals -- you can define the meaning 
(value) of a single digit, and also the how the meaning changes when one 
more digit is added to a digit string. But this does not work for most 
languages we use. The only alternative left is structural induction, but 
where is the structure of a string of characters?

The structure is in the parse tree (derivation tree) defined by the 
grammar for this sentence.

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.

How else could you explain why "2*3+4*5" means 26, and not 70, nor 
something else? Rules like "do multiplication before addition" are fuzzy 
and only lead to "meaning ex machina"-like definitions.

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.

> The meaning (program language semantics) is defined informally

There are various levels of "meaning" and semantics, for example static 
semantics and dynamic semantics.

When one uses a parser/compiler generator to implement a programming 
language, the static semantics is often defined formally in the grammar 
and associated rules. The dynamic semantics is usually not, or is 
defined by a translation to some other form (intermediate or machine 
code), but even here the translation is driven and defined by the 
parse/derivation tree.

> The grammar defines only syntax.

No, it also defines the structure, through the parse/derivation tree.

> 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?

> Normally BNF is all one needs to define syntax.

As was already replied, BNF (in its many forms) is a formal grammar 
description formalism.

> 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.

> On one hand these classes do not capture real differences
> between syntaxes of programming languages.

What sort of "real differences" do you mean?

> 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.

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