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.68.231.138 with SMTP id tg10mr1985723pbc.7.1331714215701; Wed, 14 Mar 2012 01:36:55 -0700 (PDT) Path: h9ni24483pbe.0!nntp.google.com!news1.google.com!goblin2!goblin.stu.neva.ru!news.internetdienste.de!news.tu-darmstadt.de!fu-berlin.de!uni-berlin.de!individual.net!not-for-mail From: Niklas Holsti Newsgroups: comp.lang.ada Subject: Re: Verified compilers? Date: Wed, 14 Mar 2012 10:36:51 +0200 Organization: Tidorum Ltd Message-ID: <9sb3l3Fs4oU1@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> <9s4mseFuoaU1@mid.individual.net> Mime-Version: 1.0 X-Trace: individual.net yWmh5CaDrC3MNFUJJdmc8QSfCxCu+ds6cp5Qv6PDS3XL2HRPl2 Cancel-Lock: sha1:23HAZNPzivF//nvXedaAtO4HnLY= 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: Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit Date: 2012-03-14T10:36:51+02:00 List-Id: On 12-03-12 11:43 , Dmitry A. Kazakov wrote: > 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. A string is a string, yes. We are talking about ways to define the meaning of strings, in various languages. >> 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 must be able to prove that the two forms of the program, P and P', have the same meaning. Either you have a definition of the meaning of the program, from which you show that meaning(P) = meaning(P'), or a set of modification (rewriting) rules R that by definition or assumption do not change the meaning, and then you show that P can be transformed to P' by applying these rules. IMO grammars (including attribute grammars) are a very practical way define either the meaning or the rewriting rules. > 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. Nah. Anything a program can do, is by definition computable. A legal program source text always has a computable meaning, with one exception: non-termination, which is why the meaning of a program is defined as a possibly non-terminating computation, not as the end result. But this is a debate about the "meaning of meaning". The original question was whether the research in formal languages and parsing is good and useful (my view) or useless (your view). I don't see any hope for agreement. >> 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? Why do all language definitions currently use grammars? Is it just bad influence from adacemic screwballs, inertia, and delusion? Grammars are declarative, attribute grammars almost so, at least much more so than "parse tables". >> 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? You have to give rules for it, and these rules make the "positional notation" definition of the meaning of a numeric literal string much more complex. It is easy to do it informally, by saying something like "ignore underscores when you count positions", but doing it rigorously (mathematically) is more complex. > I heard of no one who had any > difficulty in understanding what Ada numeric literals mean. I am not talking about intuitive understanding, but about the rigorous definition of the meaning (which is not really rigorous in the Ada LRM, of course, since numeric literals are considered single tokens with values described by English sentences). > You have much worse problems with Ada, e.g. > > : loop ... end loop; > > where must be equivalent to. 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. What "problem"? A context-free grammar cannot enforce the two labels to be equivalent, true. An attribute grammar can, and a Van Wijngaarden grammar can. A yacc-generated parser can. >> 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. Now you are using "meaning" with a different meaning, as in "what is the program used for". Out of scope. >>> 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. For what? For denying the usefulness of grammars? Would you really define the Ada language by a "manual" that lists all possible Ada programs? I guess the 1983 version would allow programs up to a certain size, the 1995 version would allow longer and therefore more programs, and so on... > 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. Exactly. But since our present computers can deal with very large numbers and programs indeed, the mathematical and technical methods we use for handling programming languages and programs cannot depend on this finiteness, but must use methods that apply to numbers and programs of unbounded size, but still of constrained form. Grammars are good for that, IMO. -- Niklas Holsti Tidorum Ltd niklas holsti tidorum fi . @ .