Erik Naggum <erik@naggum.no> wrote:
+---------------
| * rpw3@rigden.engr.sgi.com (Rob Warnock)
| | While it is certainly possible to create an editor that guarantees
| | that an initially valid SGML document remains valid after every
| | subsequent allowed editing step, Godel's Proof suggests that there
| | will always be some valid SGML documents which it is impossible
| | to create using such an editor.
|
| in what way is a mathematical proof a _process_ that resembles editing?
+---------------
In a proof you start with a set of axioms and transform them step by step
with permitted rules of inference to produce theorems, which augment the
set of axioms. If by following this process recursively you derive the
thing-to-be-proved, then you've proved it to be true. If you derive the
negation of the thing-to-be-proved, then you've proved it to be false.
If you fail to do either, then... well, you've failed to do either.
In a ("fascist") structuring editor, you start with a valid structure
(or structured document, such as SGML), and step-by-step select & apply
individual permitted transformations, each one of which takes a valid
structure and produces another valid structure to replace it. If, though
this process, you manage to get the structure (or document) to the point
where you wanted to go (wherever that was), then you win. If you fail...
well, then you fail.
In the first case, Godel proved that (if the proof system is consistent)
there are some true statements that can be expressed within the system
that cannot be proved (from within the system) to be true (or false).
In the second case, I hypothesized that there are some legal SGML
documents that a human using a strict structuring editor cannot write
from scratch (from the grammar's start symbol), at least, not in any
practical sense.
I readily admit the analogy is a bit weak (but IMHO still more
appropriate than the Christopher Browne article I was replying to).
+---------------
| Godel's Incompleteness Theorem isn't a trivial statement of a problem
| with all sorts of complex systems. is very carefully constrained to say
| something about proofs _inside_ a complex system.
+---------------
Yes, I know that. [Although Gregory Chaitin's restatement of it in
terms of "complexity" makes it somewhat more approachable, e.g.,
<URL:http://www.cs.auckland.ac.nz/CDMTCS/chaitin/georgia.html>
<URL:http://www.cs.auckland.ac.nz/CDMTCS/chaitin/unm2.html>
<URL:http://www.cs.auckland.ac.nz/CDMTCS/chaitin/rov.html>
for starters...]
+---------------
| the above statement from Rob Warnock sounds like New Age flirting with
| quantum physics to me. it sounds profound because what it flirts with is
| profound, while it's really just unfounded and confused opinion.
+---------------
Again, it was in reply to Christopher Browne's article <URL:news:slrn7pl9fo.
tro.cbbrowne@knuth.brownes.org> which claimed that Godel's proof implied:
"...that it may be *impossible* to create an editor that *guarantees*
that (for instance) an SGML document is valid at every step."
I certainly don't believe *that*! ...that is, if "SGML validity" has any
decidable meaning in the first place. (Which I surely *hope* it does, but
then, you're far more an expert on that than I.)
+---------------
| in other words: I'd really like to see some evidence that there exists a
| valid string in a regular syntax that cannot be produced by the grammar.
+---------------
Is SGML a "regular" syntax? And what exactly do you mean by "regular" here?
Certainly not "regular expression". "Context-free" perhaps? LL(k)? LALR(k)?
Or something more general still? (Hopefully no full context-sensitive?)
Anyway, not to bicker. That's not really the issue. What I was trying to
say to Browne was:
1. That *of course* it's possible to have an editor guarantee that an
SGML document is valid at every step [assuming "SGML validity" has any
meaning]. Simply run the document through your full "SGML validator"
after every editing step, and if it fails, beep, print an error message,
and forcefully undo the most recent editing step.
2. However, just because there may be an algorithmic way to validate (or not)
a piece of text purporting to be SGML, there's no guarantee that there's
any effective procedure for *getting* from "here" to "there" [where
"here" is the (presumably-valid) SGML you started the editing session
with and "there" is whatever goal you (a human) are trying to get to]
using the "editing steps" available in the editor.
3. I would claim that generating one production of the SGML grammar per
editing step is a totally unwieldy human interface, and anyway, how would
you *select* which one to generate (expand) at each step? (E.g., if SGML
has any ambiguity in the grammar at all, the combinatorics explode.)
[I'm assuming of course that you don't *have* the desired end result
already, otherwise you could just run it through an SGML parser and
the walk the parse tree in the editor step-by-step to "create" it...]
4. Thus, depending on the primitive transformation steps the editor *does*
permit you, there may well be valid SGML texts [that even pass the
automated validator in the editor!] that no human could use that editor
to write from scratch (from the SGML "start" symbol) in any practical sense.
The analogy to Godel's Proof seemed obvious to me (especially when
considering Chaitin's notion of "elegant programs" and their unprovability).
But maybe that still sounds like just more "New Age quantum-babble" to you.
If so, I apologize, and will shut up now.
-Rob
-----
Rob Warnock, 8L-855 rpw3@sgi.com
Applied Networking http://reality.sgi.com/rpw3/
Silicon Graphics, Inc. Phone: 650-933-1673
1600 Amphitheatre Pkwy. FAX: 650-933-0511
Mountain View, CA 94043 PP-ASEL-IA