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.220.229 with SMTP id pz5mr5931826pbc.5.1331229747071; Thu, 08 Mar 2012 10:02:27 -0800 (PST) Path: h9ni3233pbe.0!nntp.google.com!news2.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: Thu, 08 Mar 2012 20:02:25 +0200 Organization: Tidorum Ltd Message-ID: <9rsahhFmr3U1@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> Mime-Version: 1.0 X-Trace: individual.net vmuQGacm3n50SdnUy0Dk7QQrnK1GjwyN/eZiTiqy3XO+CheYFW Cancel-Lock: sha1:aFYul1tG3gEynuEM1/RThKucyhI= 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: <1psd0g0womgxi.1sle7ol12x3d5.dlg@40tude.net> Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit Date: 2012-03-08T20:02:25+02:00 List-Id: 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 . @ .