Re: Verified compilers?

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

On Mon, 12 Mar 2012 00:22:06 +0200, Niklas Holsti wrote:

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

The point is that "1234" is meaningless. Whatever way you parse that
string, it is still nothing but a string.

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

No. They are computing transformations invariant to the meaning.

Consider the source code of a program. You can modify it without knowing
what it does, while keeping it doing the same thing. You can translate a C
program into Ada without understanding it. A compiler does just same. There
is no dwarf sitting in the box who understands Ada. There is nobody in.

> First, the meaning must be strictly defined; 
> second, it must be practically computable.

No. Programs deal with incomputable meanings most of the time. Real
numbers, integer numbers, clock, user input are all incomputable.

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

No. The meanings are attached to the strings.

But what you said is already sufficient to ditch grammars, since you said
that it is rather the rules which carry the "meaning." Therefore I can take
whatever algorithm and attach "meaning" to its transitions/states. From
this point of view your grammars are just an algorithm among others. Why
specifically grammars? Why the way of programming using grammars should be
any better than one using tables, or whatever?

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

Then I don't understand your point about trees defining the meaning.

>> 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 same can be said about a piece of paper and pencil, files, keyboards,
displays etc. I don't understand your argument.

> 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 what is the problem to exclude them? I heard of no one who had any
difficulty in understanding what Ada numeric literals mean. The problem you
describe has nothing to do with defining their meaning. It has to do with
your way of programming the parser.

You have much worse problems with Ada, e.g.

   <label-1> : loop ... end loop <label-2>;
 
where <label-1> must be equivalent to <label-2>. It is no problem to any
human reader to understand what does this mean. It is no problem to a
recursive descent parser. All Ada compilers handle it effortlessly. It is
only a problem for the *language* you chosen. Take another one, end of
story.

> What role does the number 
> 137 play in the meaning of the 137th token in the program?

Depends on what that program does. The meaning of a program is specific to
the domain, none of the compiler's business.

> So I still 
> wonder how you can define meaning without parsing, for languages more 
> complex than numeric literals.

Here it is: "acceptable to the customer." Troublesome as it is, but there
is no other way.
 
> If you want to compute with meanings, they must be computable, which 
> usually means they must be constructive. Counterexample?

Pi

[ Meanings are not computed, they are assigned to the computational states,
absolutely voluntarily, of course ]

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

I still do not see how this may support grammars, or the point that when
Ada compiler sees "Pi" it must compute Pi, or that ARM's syntax annex
defines Pi?
 
> I feel that you are not really getting any meaning from what I write, 
> and vice versa, a bit.

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

Because this the killer argument. No computer can parse infinite language
or compute incomputable. If you want to handle such stuff [and you must all
the time!] you have to map it onto some finite/computable framework and
deal within the latter. You certainly lose something while doing this. And
it is again incomputable to reason about what was lost.

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