Re: Optional features considered harmful

W. Eliot Kimber (kimber@passage.com) wrote:

> But note that general text entities *don't actually do point 3*.  General
> text entities *ARE NOT REUSABLE*.  In fact, the only way to have re-usable
> SGML documents, as James has pointed out, is to make them documents
> syntactically (even if the objects may be semantically subparts of documents).
> 
> While external text entities are a useful convenience for single-person
> authoring, they are not useful as a general mechanism for managing SGML
> data as re-usable objects.  

Although I would agree that external text entities have a whole host of
problems and that hyper-link provides a better re-use model, external text
entities can be managed quite well via a component model.  If you can decide 
what your re-usable components are before you author them--which is necessary
in a large authoring environment--you can setup systems for managing and
validating these components.  So, I wouldn't rule out external text entities
for reuse unless we demanded HyTime and created a *required* application
convention to handle inclusion of information.

As an aside, according to Church's thesis and the Godel Incompleteness Theorems
documents with external text entities that are variable are never verifiable.
Documents with hyper-links to variable documents are, of course, verifiable.

The argument goes something like this:

1. Those things that are computable in our sense are those things that are
   computable by humans or machines given that limitations on time and speed
   are overcome. (Church's Thesis)

2. Godel's theorem states: There is no consistent, complete, axiomatizable 
   extension of Q--where Q is in our case the set of functions necessary
   to parse an SGML document.  In our sense, extensions include asking the
   question "will this document parse under all instances of entity x that
   conform to constraints y".

3. If the constraints y on entity x allow x to have infinite variants, then
   proof (program) of the question of validation is not both complete and
   consistent at the same time.  You can never validate an infinite number
   of variants but you could attempt to prove that the document will
   always be valid.

4. Thus, although one could be bright enough to prove that for all variants
   of a particular x, this particular document is valid, it is not necessary
   that such a proof exists or that such axioms that make up the proof will
   apply in all cases.

5. Hence, there is no program that can prove that a document containing
   a set of variant external entities can be proven, given a set of constraints
   on the external text entities, that the resultant document is valid.

In a sense, the hyper-linked approach gets us closer to a verifiable system
in that each component--variable or not--can be validated independent of
each other.  The approach would be simpler to saying: 

  "You can either compile all your C++ code at once and, if everything
   compiles, you get your program, or you can break your code into verifiable
   modules and compile them separately.  There is no guaranty that they
   will fix together or that the resultant program--while valid C++--will
   be semantically correct.  Unfortunately, you will never be able to verify
   the semantics of your program unless you can get it compile and link!"
  
See "Computability and Logic" by George S. Boolos and Richard C. Jeffrey
for a much better description of the above.

==============================================================================
R. Alexander Milowski     http://www.copsol.com/   alex@copsol.com
Copernican Solutions Incorporated                  (612) 379 - 3608

Received on Friday, 25 October 1996 10:48:45 UTC