From: Bill Richter (richter@math.northwestern.edu)
Subject: Re: Clinger's sloppiness in his RichterFAQ
Newsgroups: comp.lang.scheme
Date: 2004-08-22 22:17:12 PST

spam_depository2004@yahoo.com (Johnny) responded to me in message
news:<2a56f6a3.0408221257.7983c981@posting.google.com>...

   Bill, why don't you write *one* article that includes your theorem
   (that Clinger disagrees with) as well as ALL definitions, lemmas,
   etc.  Make it complete, but as short as possible (but no
   shorter). Math is a precise discipline and once you state your
   theorem and proof, you are either right or you are wrong. You might
   also want to post it to comp.theory for better peer review.

Sounds good, Johnny, but we're arguing about things like the meaning
of Schmidt's Thm 3.13, the difference between C-F's and Nielson^2's
def of compositionality, whether functions have definitions, and if a
function have 2 definitions, one denotational and one not.  I don't
actually know what Will's positions on these issues are.  If I knew
Will's positions, I bet we wouldn't have anything to argue about. It's
long enough for a dvi file now, as Shriram suggested long ago.

I already used Will's alert criticism of my response to Kevin
Millikin's criticism of my post.  But I see Will has another response:

   [Editor's note: The first two sentences of the paragraph above
   assert that Bill did not define E by structural induction.  That
   means Bill's definition of E is not compositional.  The third
   sentence states that Bill's E_1 is just the composition of E with a
   quotient map.  Therefore Bill's definition of E_1 is not
   compositional either.]

These facts aren't in dispute, now that I understand that the
cls-definition of compositionality is a property of definitions, and
not C-F's property of the semantic functions themselves.  Modulo E not
being a sem function anyway.  Yes, my original definition of my E_i
sem functions was not a denotational definition.  My theorem (1-line
proof due to Schmidt's Thm 3.13) is that my E_i however do have a
denotational definition: take my f_ij and crank out some sem functions
via Schmidt's Thm 3.13.  By Schmidt's uniqueness, and my already
proved Bill-compositionality of my E_i, these 3.13-constructed sem
functions must equal my original E_i.

I'm glad to see that Will included my suggested disclaimer.   But

   (By the way, this is not my home page, 

OK, I goofed.

   and none of my other web pages link to this one. Also, my PhD was
   awarded by the mathematics department at MIT upon completion of
   their doctoral program in pure mathematics.)

Why doesn't Will say this on his home page?  Doesn't Will also have an
undergraduate Math degree from UT?  Why doesn't he write a paragraph
to the effect of how his study of pure Math has helped him in CS?

Turns out my semantics for Nielson^2's While gave a straight
denotational definition, and didn't use Bill-compositionality.  I
think the only difference between my definition and Nielson^2's is
that I didn't use the CPO least fixed point method to define the
Phi function for curly-S[while b do S], but instead used my 
induction/subset-ZFC Lemma that I used to show that my E (and 
similarly, F-F's |--->>_v) was well defined.  Will complains I 
cite Boolos & Jeffrey too often, but that's all I get out of B-J:
they define partial recursive functions without mentioning any CPO
least fixed point techniques. I can construct their functions with
my induction/subset-ZFC Lemma, which I think is so standard that
nobody bothers to ever mention it.