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=-1.3 required=5.0 tests=BAYES_00,INVALID_MSGID autolearn=no autolearn_force=no version=3.4.4 X-Google-Language: ENGLISH,ASCII-7-bit X-Google-Thread: 103376,6a9844368dd0a842 X-Google-Attributes: gid103376,public From: jsa@organon.com (Jon S Anthony) Subject: Re: seperate keyword and seperate compilation with Gnat? Date: 1996/07/11 Message-ID: #1/1 X-Deja-AN: 167854060 sender: news@organon.com (news) references: <31D95D93.28D8D15B@jinx.sckans.edu> organization: Organon Motives, Inc. newsgroups: comp.lang.ada Date: 1996-07-11T00:00:00+00:00 List-Id: In article dewar@cs.nyu.edu (Robert Dewar) writes: > "I was not saying that the statement _should_ have been in the > standard. I can actually accept that the RM as it stands is clear > enough on the issue. My only point is (and it _still_ is) that the > statement is FAR clearer than what the RM actually says." > > But you are looking at things in isolation, which is always misleading. No, I'm not looking at it in isolation. > If you intend to use your approach here, then you must consider the > full changes to the RM to accomodate this approach. If you simply add I didn't really have an "approach" per se in mind when I mentioned this. But, yes, I think you could do much better from the perspective of clarity. However, that might not be a "good thing" for a "reference manual" (as the Algol68 report indicates) and so I am willing to say that the current RM is a reasonable compromise. > your statement as normative text, then it is redundant, and redundancy, > while useful in tutorial material is the enemy of precise definition. Well here we just plain disagree. In fact, this statement is positively wog-boggling. Using your apparent "criteria" here, you would have to say that the statement of any theorems in a mathematical treatise are somehow counter to the precision and clarity of exposition of the material. They are clearly "redundant" in the strictly formal sense, i.e., they are deducible from the definitions, axioms (and perhaps various meta information - interpretations, models and whatnot). Such a view is clearly crazy. So, I presume you would claim that is not what you meant (even though that is clearly what you are saying). So, perhaps you meant one should "draw the line" somewhere? Where? No propositions? How about no lemmas? Maybe we should drop corollaries? After all, don't they just "obviously" follow from their corresponding theorems and are thus clearly redundant and "thus" empty of content? No? I thought not... Highly precise and formal works (more formal and precise than the RM was ever dreamed to be in the wildest fantasies of those involved) are absolutely _FULL_ of this sort of "redundancy". In fact, it is a hallmark of such works. > So that means you have to remove stuff to add your statement. I don' > t see how that would work, since your negative statement still seems > pretty content free to me in definitional terms. It's clearly not content free. "Redundancy" does not imply content free. For good measure, it is worth noting here that certain tautologies (formal logical equivalences) are among some of the most important theorems in mathematics. The fact that something is "redundant" is at times _startlingly_ surprising. > But it would be interesting to see how you would rewrite the whole > section. I very much doubt it would be clearer, but of course one > cannot be sure without seeing the entire section rewritten. Yes, you cannot be sure about this until it was attempted, but it would not surprise me at all. The real issue is that it would take considerable effort and the resulting pay off would likely not be sufficient to justify such effort, i.e., as I mentioned previously, the RM as written is good enough. /Jon -- Jon Anthony Organon Motives, Inc. 1 Williston Road, Suite 4 Belmont, MA 02178 617.484.3383 jsa@organon.com