Re: seperate keyword and seperate compilation with Gnat?

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

In article <dewar.836964568@schonberg> 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