Subject: Re: returning from a function (Ex: Re: some small  proposed  changes to standard)
From: Erik Naggum <erik@naggum.no>
Date: 1999/07/27
Newsgroups: comp.lang.lisp
Message-ID: <3142069374347774@naggum.no>

* rpw3@rigden.engr.sgi.com (Rob Warnock)
| 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.

  sure, but where are the axioms of editing?  insert and delete?  and how
  are they related to the formal system under scrutiny?  as far as I know,
  SGML doesn't have such axioms to begin with, and production of a string
  from a grammer is not quite a transformation, it's a _production_.  so I
  think this is a stretch.

| 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.)

  *snicker*  yes, it has a decidable meaning.  SGML ain't _that_ bad.

  I found the statement you quote flimsy and impossible to argue against.

| Is SGML a "regular" syntax?  And what exactly do you mean by "regular" here?

  yes, SGML's DTDs defines a regular syntax, "regular" being defined as
  LL(0), or that any rule of grammar can only add tokens at the end of the
  string.

| Certainly not "regular expression".

  um, that's the idea.  why "certainly not"?

| 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.

  <aside>and an SGML validator can return "this is not an SGML docuemnt" as
  its only error message, which is more useful than most of the other error
  messages you'll try to recover from.</aside>

| 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?

  the DTD grammar is fairly well constrained.  the approach isn't all that
  useful for writing DTDs, only the element structure of the document.

  consider a Lisp editor that does the same thing.  suppose you have an
  empty buffer, which is a fully valid Lisp source file.  if you insert to
  parens, (), you still have a valid Lisp source file, and I'll maintain
  that invariant.  inside the (), any function or special form in the
  prevailing package is allowed.  suppose you type a function name, the
  appropriate number of argument slots should be indicated and the document
  is at this point invalid until all slots have been filled in.  optional
  arguments could easily be indicated by a shaded slot or whatever.
  keyword arguments could be indicated by a key which expands to the list
  of available keywords when clicked on, like a menu of choices, etc.
  suppose you type LET instead of a function name.  a LET form is valid if
  it has an empty binding clause and an empty body, so the buffer would
  have to contain at least (LET ()).  the inner () is straight-forward to
  insert automatically, and any bindings inside it would know what they
  were, too, which could even be used to "verify" that any free variables
  were importable from the outer environment.  that's how a Lisp
  syntax-sensitive editor would work.  SGML makes this easier, since it
  allows far less choice.

| 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.

  I still don't buy this.

| But maybe that still sounds like just more "New Age quantum-babble" to you.
| If so, I apologize, and will shut up now.

  ok.  ;)

#:Erik
-- 
  suppose we blasted all politicians into space.
  would the SETI project find even one of them?