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.9 required=5.0 tests=BAYES_00 autolearn=ham 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/12 Message-ID: X-Deja-AN: 168106962 sender: news@organon.com (news) references: <31D95D93.28D8D15B@jinx.sckans.edu> organization: Organon Motives, Inc. newsgroups: comp.lang.ada Date: 1996-07-12T00:00:00+00:00 List-Id: In article bobduff@world.std.com (Robert A Duff) writes: > Jon S Anthony wrote: > >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). > > But those math textbooks always label those as "theorems", to make it > clear that these are not axioms, but can be derived. And they usually > show the proof, or an outline of the proof. Or they "exercise the > interested student". ;-) Sure. And? > The rules of the RM proper are entirely definitions and axioms. > Anything that's a theorem is put in a NOTE, so you know it's not a > basic fact, but can be derived from other facts. OK, fine. This makes sense. It would probably have been good to actually state this point explicitly, but whatever (or maybe it is and I just can't find it). Also, it is worth noting that the rules (like axioms) are only of peripheral interest and only to the extent that they _actually_ imply what you _really_ want. Unless you are studying axiom systems for the sake of studying axiom systems (like I did...), but that is clearly not true in this context. > So, I would have strongly objected to your suggestion as an RM rule, but > I would have considered it as a NOTE. Fine - as I pointed out I did _not_ say that it should have been. > For a NOTE (as for a theorem in a math text), you include it if it > seems interesting enough, and doesn't make the book too big, and so > forth. All highly subjective considerations. Well, another thing that is very important is that often (in fact typically) the theorems are more important than the axioms/defs. Why? Simple. They typically contain the sort of stuff that is more interesting and several (in fact, clearly an infinite number of) different axiom systems can be constructed to produce the _desired_ result, i.e., working backwards is a very typical thing in this sort of context. Boatloads of these may have redundancy in the axioms (they are not independent). Basically the only really interesting ones are those that are minimally independent and strong enough to "produce" the "important stuff" (cover the subject). Now, do you really want to claim that the rules of the RM are in fact "minimally independent and cover the extent of the subject"? I don't think so. The thing is far to fuzzy to go that far out on a limb. So, throwing in "theorems" left, right, and center is probably a pretty damn good idea. Except, you will say, "Hey, this is not that kind of formal work. It is going to be read and attempted to be used by ordinary joe-blows. And besides the damn thing is big enough as it is!" True. I guess what that means is that it should have been split into two different volumes. The "engineering volume" and the "formal volume". I suppose that was too much work. Oh well... > Lots of people suggested lots of NOTES, and it was always a judgement > call as to whether that particular fact was interesting enough to the > general reader. There's always Ada textbooks, which have lots more > theorems than the RM. No, they do not. They have various programming examples, suggestions, usage notes, some "rule repetition", various "religious" discussions, high-fives, I-told-you-sos, this, that, and the next thing. But they virtually never have theorems about the language. This is true of _any_ programming language textbook. Why? Simple. The subject matter isn't the language it's how to use it to construct programs. The structure or "theory" of the language is of only the most peripheral concern and usually anecdotal at best. > >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. > > True, but they always make a clear distinction between basic facts > (axioms) and interesting redundant facts (theorems). First: Yes. And???? Second: Well, assuming the axiom stuff is mentioned at all. Note that most working mathematicians do not go around deducing stuff from axioms using mathematical logic as the mechanism in all its detail. That would be a complete waste of time and just plain stupid. Flip open a "typical" (not a logic book or set theory book or other "foundational like" book) mathematics book and you will not see much of this so called "rule stuff" mentioned except in passing. > >the RM as written is good enough. > > Nice to know. ;-) Indeed it is. /Jon -- Jon Anthony Organon Motives, Inc. 1 Williston Road, Suite 4 Belmont, MA 02178 617.484.3383 jsa@organon.com