[Editor's note:  This is the complete text of yet another message
by Bill Richter in this thread, responding to Johnny, Neil Van
Dyke, and Kevin Millikin.  I have added an editor's note at the
very end.]

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

kmillikin@acm.org (Kevin Millikin) wrote in message news:<837a520f.0408230720.35ed4dbf@posting.google.com>...

First let me respond to Neil Van Dyke & Johnny:

   spam_depository2004@yahoo.com (Johnny) writes:
   > Bill, why don't you write *one* article that includes your theorem
   > (that Clinger disagrees with) 

   Seconded!  I'll admit that I long ago got confused as to the point
   of the Richter-semantics discussion.

I don't know what Will disagrees with!  It's starting to seem like
Will is grading me: docking me points for this or that.  Rather than
saying: "I didn't know that, that might be interesting", or "That's
false, here's a counterexample."  Now I know I'm right: this stuff
ain't that hard.  But I don't know that it'd be interesting to CS
folks.  For me to write a paper nicely, I'd need some feedback like
that: "That'd be interesting, because we thought it was false."  Or
"We still think it's false!"  I don't know what Will thinks is false.
We don't seem to be communicating at all well.  

And Neil, the point of the RS discussion is whether you can use OpS
techniques to define total compositional semantic functions.  I, Will,
MB, and soon Daniel have defined such total OpS-ized functions.  The
only question is these total functions are compositional, or if they
have compositional definitions.  And this is 99% a matter of the
definition of compositionality. So as long as folks want to rap about
compositionality, this is a good place for it.  Be nice if we could
keep the discussion civil, but maybe we're heading that way.

   Let me elaborate.  Consider the grammar:
   
   N ::= 0 | sN
   
   and the function:
   
   add(0)  = \M.M
   add(sN) = \M.s(add(N)(M))

Sure, Kevin, so inductively, we see that add(n)(x) = n + x.
  
   defined by structural induction on the syntax of N-terms.  

   Now, consider that we defined a function (+) on N-terms, and then
   defined:
   
   add(0)  = \M.M
   add(sN) = \M.(sN + M)
   
   (Bill's construction is more complicated, because he interprets
   structural induction as *requiring* recursion on all proper
   subterms, rather than *forbidding* recursion on terms that are not
   proper subterms.)

That's a misunderstanding I corrected in a response to you.  You're
right: to do structural induction, you can recur on proper subterms
and nothing else, in exactly the sense of Thm 3.13.  I wasn't using
structural induction when you flagged me, so I was OK then. I'll
delete your mentions below of this.
   
   Is this latter add function defined by structural induction on its
   argument?  Two possible answers:

Kevin, I'm not up on this, I wish you were doing some kinda DS, with
semantic functions, instead of this, but I'll try: You're defining

add: N ---> (N -> N)

by add(0) = identity 

add(n')x = n' + x

using prime for S, as B-J do.  To me, Bill-compositionality would mean
here that

add(n') = Phi( add(n) )

for some function Phi: (N -> N) ---> (N -> N)

And cls-compositionality would mean that Phi was used to give an
inductive definition of add. So is that true?  What's Phi?  Looks like

Phi( x |---> x+n) = x |---> x+n+1 

I get it:  Phi(f)= S \circ f, 

i.e. the composition 

N -f--> N -S--> N.

So I say it's true: your new add is compositional (in C-F's sense): it
has a denotational definition.

   
   1. No, because it applies (+) to a subterm that is not a proper
   subterm of the argument, and (+) is the same function as add.

I reject 1: I say it's just a clever misinterpretation of what proper
subterm means.  This is what recur on proper subterm means:

add(n') = Phi( add(n) )

in my Schmidt 3.13 understanding (tho that's about sem functions).

The fact that you can rewrite this in a non-proper-subterm fashion

    add(sN) = \M.(sN + M)

is just a tribute to your cleverness & sense of humor.
  
   2. Yes, because it has the proper form (in fact, it's not even
   recursive!).  Some Bill-obfuscation could transform the function
   definition (with corresponding changes to the grammar for N) into a
   form that *was* recursive without actually doing any useful work in
   the recursion; but I don't insist on that.

Hah, I did that above (although I didn't change the grammar)!  But I
peeked ahead and see that we're in agreement!  2 is true. Great.

You're right, there's a non-recursive def of add: add(n)x = n + x.
   
   Now, given that one agrees with 2, does that mean that (+) is
   compositional?  

I don't even know what that means.  We defined a function add assuming
there was an operation + on N.  I'll assume you meant to use your
original def of add, that just used S:

   add(0)  = \M.M
   add(sN) = \M.s(add(N)(M))

By induction (structural if you like!), this defined a function 

add: N ---> (N -> N)

and by adjointing (or uncurrying) we define a function 

+: N x N ---> N

(+ n x) = add(n)x

But I don't know what it means to say this + is compositional.

   (+)(0)  = \M.M
   (+)(sN) = \M(sN + M)

That looks like an important confusion between my add & + above: 
add: N ---> (N -> N)
+: N x N ---> N

So I'll quit. 
   
   That is, of course, where Bill's proof of the equivalence of two
   notions of compositionality goes wrong.  

The proof is fine, and now that I answered your earlier post, maybe
you'll be able to read my proof.

   He claims that there exists a definition of (+) by structural
   induction on its argument, but he has failed to produce a
   definition of (+) by structural induction on its argument.

I can't follow this objection.  You'll have to fix me above first.
   
   As an aside, another thing that I find mildly amusing is that Bill
   uses Schmidt's theorem 3.13 to prove the existence of a function
   that we know exists (he's already constructed it); 

That's false, as I've posted: I only use Thm 3.13 to show that my
already constructed sem functions have a denotational definition.

   and the uniqueness of the solution to a system of equations whose
   solution (if there is one) is unique by definition (the equations
   don't have any variables!).  (I know, that's not *exactly* what he
   does, but near enough to give me a chuckle.)

That sure sounds false, but I can't parse it :) Let's try again: I
showed that for certain E_i & f_ij that these equations hold:

E_i( Option_ij ) = f_ij ( E_ij1(S_ij1),..., E_ijk(S_ij{k_ij}) )

OK.  Now consider all possible solutions in functions BB_i of the
equations 

BB_i( Option_ij ) = f_ij ( BB_ij1(S_ij1),..., BB_ijk(S_ij{k_ij}) )

Schmidt's Thm 3.13 says there's a unique family of solutions { BB_i }.
So my original solution { E_i } must be equal to anyone else's
solution.  And there is another solution that folks are keen on: the
solution given by structural induction!  Hence my E_i are equal to
this structural-induction-defined solution.  Hence my E_i have a
denotational definition.

But (having posted this now for the N-th time), let's recall that I
now say that the only meaning of 
"BB_i are defined by structural induction by the f_ij" 
is that 
the BB_i are the unique family of functions produced by Thm 3.13.  

So I used extra words.  Once we know the E_i satisfy the equations, we
know the E_i are defined by structural induction by the f_ij.

[Editor's note:  Bill's definition of E is not compositional, so
he introduced an irrelevant structural induction by using Schmidt's
Theorem 3.13 to define a family of identity functions E_i (for i > 1)
while defining E_1 = E.  His definition of the identity functions
is compositional, and E_1 is E composed with identity functions,
so he concludes that his definition of E_1 is compositional.]