Re: Verified compilers?

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

On 12-03-11 11:47 , Dmitry A. Kazakov wrote:
> On Sat, 10 Mar 2012 22:35:09 +0200, Niklas Holsti wrote:
>
>> On 12-03-10 12:36 , Dmitry A. Kazakov wrote:
>>>
>>> 1234 is an example of a language (of decimal literal).
>>
>> Or an example of octal literals, or hexadecimal literals, or telephone
>> numbers. The meaning is not intrinsic in the string; it must be defined
>> by other means.
>
> Which only supports my point.

What point is that? You have lost me. Or I you.

> Yes, meaning is a mapping of which string is the argument. The way this
> mapping is computed (if computable) is irrelevant.

All language-processing programs, compilers and so on, compute with the 
meanings of strings. First, the meaning must be strictly defined; 
second, it must be practically computable. (Of course this means that 
there are important restrictions on the kinds of meanings that 
language-processing programs can handle -- they must often be "weakened" 
meanings. For example, during compilation, the meaning of a program is a 
"computation", not the end result of that computation.)

>> The grammar, and the corresponding
>> parse trees, are tools for defining the strings in the language, and the
>> meaning of each string.
>
> No, only the former. Example:
>
>     <numeral>  ::=<decimal-digit>[<numeral>]
>
> This does not define the meaning of 1234. It may hint the human reader that
> <numeral>  has something to do with numbers. But numbers and their
> properties are defined elsewhere (in mathematics). The mapping:<numeral>
> corresponds to the number from the set X identified by the means Y must be
> stated additionally to the grammar.

A plain grammar does not define meaning, agreed. The meaning is defined 
by rules attached to the grammar productions. In this example, the rule 
use numbers and their mathematical proprerties; for your example 
production, the rule would say that the meaning -- the value -- of the 
grammar symbol on the left (<numeral>) is defined as the value of the 
<decimal-digit>, times 10, plus the value of the <numeral> on the right, 
or just as the value of the <decimal-digit> if there is no <numeral> on 
the right.

Attribute grammars (which I include in the general term "grammars", but 
perhaps you don't) are one formalization of such rules.

>
>>>      +
>>>     / \
>>>    4  +
>>>       / \
>>>      *
>>>     / \
>>>    3  10
>>>
>>> This one? There is a countable infinity of such trees. A German would say
>>> that this is twelve hundred, four and thirty (12,4,3). A way different
>>> structure then?
>>
>> Yes, the grammar of (decimal) literals can be written in several ways,
>> and all of these grammars can be attributed to define the same meaning
>> (numerical value) of the string (of course they can also be attributed
>> in different ways, to define different meanings). So what? I never
>> claimed that the grammar is unique, just that grammars and parse trees
>> are IMO the unique known method to define the meanings of complex sentences.
>
> 1. If not unique, then you cannot claim that the structure of a particular
> tree is inherent to the language. It is not.

I've never claimed that -- see the quote to which you are replying! The 
parse tree depends on the grammar and the sentence, as I'm sure you know.

> 2. If same grammar may be used with different meanings, then the grammar
> does not define any of them.

See above. The grammar is the scaffold on which the meaning is defined, 
by attribute computations or in other ways.

>>> The meaning has nothing to do with parsing.
>>
>> Ok, if you can define the meaning in some other way, and not by parsing.
>> How do you define it?
>
>     http://en.wikipedia.org/wiki/Positional_notation
>
> does not even use the word "grammar" when describes positional notation.

As I said in an earlier post, literal numbers are one of the few 
languages for which meaning can be defined by induction on the length of 
the string, which is the same as the positional notation definition.

But defining meaning by positional notation does not work so well for 
the numeric literals in Ada. You would have to exclude underscores from 
the position numbering, and also handle the optional base specification.

And it is just ridiculous to consider something like positional notation 
for defining the meaning of an Ada program. What role does the number 
137 play in the meaning of the 137th token in the program? So I still 
wonder how you can define meaning without parsing, for languages more 
complex than numeric literals.

> (Of course parsing is involved, e.g. your browser will parse the page in
> order to render it. But that defines neither the meaning of this page nor
> the meaning of numerals.) Maybe our disagreement lies in that you think
> that all definitions have to be constructive? They should not.

If you want to compute with meanings, they must be computable, which 
usually means they must be constructive. Counterexample?

> Anyway I can
> always skip parsing and define meaning by brute force:
>
> "1" means 1
> "2" means 2
> "3" means 3

If you include "0" and continue up to "9", you have the definition of 
the meaning of the <decimal-digit> symbol in your example production 
above. Just add the inductive rule for the production that defines 
<numeral>, and you get a complete, finite, definition of the meaning of 
all possible <numeral>s.


> ...
>
>>> In fact parsing has to be validated against the meaning.
>>
>> Why? If you define the meaning without using parsing, why is that
>> validation necessary?
>
> Because the meaning exists independently on the parsing, thus I must show
> that the result of translation corresponds to the meaning. "1234" must be
> translated into 1234, because that is the meaning of "1234". Not otherwise.

Mere parsing does not give a translation (unless you consider the parse 
tree as a translation, which it is, of course). If you are producing the 
translation during parsing, or by a traversal of the parse tree, 
validation is easier if you define the meaning, too, as a function of 
the parse tree.

Look, I agree, of course, that the natural number 1234 exists, without 
referring to the string "1234" or any grammar. That is mathematics. But 
in computing, we are dealing with myriads of different languages, with 
different domains of meaning, and we need computational definitions of 
the meaning of sentences, at least for the aspects of "meaning" that are 
involved in the specification, implementation, and validation of our 
programs.

>>>>>> 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.
>>>>
>>>> Operator precedence, perhaps? See earlier post...
>>>
>>> I didn't mean variations of operator precedence generating different
>>> results. I meant that 2*3+4*5 = 26 is a statement to be proven. It is
>>> either true or false (or undecidable). 26 is the value of the formula.
>>
>> The truth of the formula depends on the meaning assigned to the
>> expressions in the formula. Before one can prove anything, one must
>> define the proof rules, including the rules for modifying sentences
>> (expressions) while preserving their meaning.
>
> Yes.
>
>> The latter rules are
>> derived from the rules that define the meaning of an expression based on
>> the structure (parse tree) of the expression, and the properties of the
>> operators in the expression.
>
> No, it is based on algebraic properties of numbers.

Which is what I said -- algebra is about expressions and operators.

I feel that you are not really getting any meaning from what I write, 
and vice versa, a bit.

> All computers are finite and all programming languages are effectively
> finite both in the terms of the source code length and the number of states
> compiler programs may have.

This argument is one of the last recourses when you have no good answer. 
Finity, finity, all is finity.

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