Re: seperate keyword and seperate compilation with Gnat?

[jsa@organon.com (Jon S Anthony)]

In article <DuEEtI.Cou@world.std.com> bobduff@world.std.com (Robert A Duff) writes:

> Jon S Anthony <jsa@organon.com> 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