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

Re: BEGIN in Scheme's Abstract Syntax



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"!