From ... From: Erik Naggum Subject: Re: returning from a function (Ex: Re: some small proposed changes to standard) Date: 1999/07/27 Message-ID: <3142069374347774@naggum.no>#1/1 X-Deja-AN: 505765259 References: <199907210420.VAA04718@pacific> <7njrck$60a4d@fido.engr.sgi.com> <3142057178277430@naggum.no> <7nk5hq$6tou6@fido.engr.sgi.com> mail-copies-to: never Organization: Naggum Software; +47 8800 8879; http://www.naggum.no Newsgroups: comp.lang.lisp * 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 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. | 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?