From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=0.4 required=5.0 tests=BAYES_00,FORGED_MUA_MOZILLA autolearn=no autolearn_force=no version=3.4.4 X-Google-Thread: 103376,5412c98a3943e746 X-Google-NewGroupId: yes X-Google-Attributes: gida07f3367d7,domainid0,public,usenet X-Google-Language: ENGLISH,ASCII-7-bit Received: by 10.204.129.15 with SMTP id m15mr706860bks.2.1331504529280; Sun, 11 Mar 2012 15:22:09 -0700 (PDT) Path: t13ni126337bkb.0!nntp.google.com!news1.google.com!news4.google.com!fu-berlin.de!uni-berlin.de!individual.net!not-for-mail From: Niklas Holsti Newsgroups: comp.lang.ada Subject: Re: Verified compilers? Date: Mon, 12 Mar 2012 00:22:06 +0200 Organization: Tidorum Ltd Message-ID: <9s4mseFuoaU1@mid.individual.net> References: <9207716.776.1331054644462.JavaMail.geo-discussion-forums@ynaz38> <4edda5mav3cf$.149pbgyxl1wx5.dlg@40tude.net> <9rplcgF5a2U1@mid.individual.net> <1psd0g0womgxi.1sle7ol12x3d5.dlg@40tude.net> <9rsahhFmr3U1@mid.individual.net> <9rvdjvFfa8U1@mid.individual.net> <4pp58h1br5sp$.yylr20e5vzxb.dlg@40tude.net> <9s1s7tF6pcU1@mid.individual.net> <1oln2mjlozzh5$.1mxrd97lrgndo.dlg@40tude.net> Mime-Version: 1.0 X-Trace: individual.net f8UAukhUe/49+ewtgIM7+AT/XFtEEwkbnD0tuXDK02tNLFZxXe Cancel-Lock: sha1:JKbxAaNhmW0bVPE5K5HvdHBrAtI= User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.6; rv:10.0.2) Gecko/20120216 Thunderbird/10.0.2 In-Reply-To: <1oln2mjlozzh5$.1mxrd97lrgndo.dlg@40tude.net> Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit Date: 2012-03-12T00:22:06+02:00 List-Id: 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: > > ::=[] > > This does not define the meaning of 1234. It may hint the human reader that > has something to do with numbers. But numbers and their > properties are defined elsewhere (in mathematics). The mapping: > 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 () is defined as the value of the , times 10, plus the value of the on the right, or just as the value of the if there is no 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 symbol in your example production above. Just add the inductive rule for the production that defines , and you get a complete, finite, definition of the meaning of all possible 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 . @ .