[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*To*: "Richard P. Gabriel" <rpg%inferno@lucid.com>*Subject*: Re: BEGIN in Scheme's Abstract Syntax*From*: ramsdell@linus.mitre.org*Date*: Fri, 31 May 91 13:52:58 -0400*Cc*: rrrs-authors@altdorf.ai.mit.edu*Full-Name*: John D. Ramsdell*In-Reply-To*: Your message of "Fri, 31 May 91 08:27:10 PDT." <9105311527.AA05230@inferno>*Posted-Date*: Fri, 31 May 91 13:52:58 -0400

I am quite pleasently surprised that such a dry proposal evoked any response at all! >> Well, in my day, we we able to pretty easily reduce slightly more >> complex syntax to a slightly more simple version for our proofs. I >> guess this is too much to ask the playboy mathematicians of today. Let me tell you the motivation for my suggestions. I am working on a project to produce a verified implementation of Scheme. One property that we require is that any answer produced by our implementation must be the same as the one predicted by Scheme's denotational semantics. The proof of this property is complicated because of the many cases that must be considered. One of the first actions we took was, in your words, to "reduce slightly more complex syntax to a slightly more simple version for our proofs". In other words, we have a version of the semantics that incorporates the changes I proposed. I am of the opinion that the simplications to the semantics that we found were appropiate for the Verified Lisp project make the semantics simpler and easier to understand for all readers. There are many times when changing a theory to make proofs easier, also makes the theory easier to understand. I suggest this is one example. John PS. What `till my wife hears I was called a "playboy mathematician"!

**References**:**BEGIN in Scheme's Abstract Syntax***From:*Richard P. Gabriel <rpg%inferno@lucid.com>

- Prev by Date:
**Re: BEGIN in Scheme's Abstract Syntax** - Next by Date:
**Scheme standard published** - Prev by thread:
**Re: BEGIN in Scheme's Abstract Syntax** - Next by thread:
**Scheme standard published** - Index(es):