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

Lauri Alanko <la@iki.fi> responded to Kevin Millikin
<kmillikin@acm.org> in message
news:<cgc2mu$nph$1@oravannahka.helsinki.fi>...

   > So, if you define E' by structural induction using a Phi function
   > that is defined in terms of E, and if E' = E, and if "functions
   > don't have preferred definitions", then you defined E' using a
   > Phi function that is defined in terms of E'.
   >    > And everyone knows you can't do that.
      Um, so by this reasoning, if I first define 
   
   f(x) =_def x * x
   
   and then
   
   g(x) =_def f(-x)
   
   then, since it turns out that g = f (extensionally), I have been
   defining g in terms of itself? And this is illegal?
   
Thanks for the support, Lauri!  I think there's a reason why you're
understanding me the best here: you're the youngest; you've had point
set Topology the most recently (Will was the best of us I think).

Kevin actually noticed an ambiguity about the word define (didn't you
point that out, Lauri?), so I'll respond to Kevin's here:

   In article <837a520f.0408222048.27ad1822@posting.google.com>, Kevin
   Millikin <kmillikin@acm.org> wrote:

   > Everyone knows you can't define E by structural induction on a
   > Phi that's defined in terms of E!  But I'm not doing that. 
   > Everyone knows you can't define E by structural induction on a
   > Phi that's defined in terms of E!  But I'm not doing that.

   Of course you are.

I suppose, strictly speaking, you're correct, Kevin.  But you just
noticed an ambiguity of the word define, which has 2 meanings:

One meaning of define is: let's refer to this set by this variable.

Another meaning of define is "the E_' are defined by structural
induction by the f_ij."  And that's got a very precise meaning:

Call E_i' the unique functions proved to exist by Schmidt's Thm 3.13,
given the input of the f_ij functions.

So "defined by structural induction" means "use Schmidt's Thm 3.13."
As long as that's what we mean, there's no opportunity for the bogus
mutual recursion that I've so often been accused of here on cls.

Above, Lauri point out how your contradiction dissolves into laughter
if we only use the first meaning of define (call this set `f'),
instead of mixing this meaning with "defined by structural induction".

The rest of my post is probably overkill, but I wrote it before I
grokked your arg, so I'll leave it.  Redundancy is sometimes good.

   Your "proof" that your notion of compositionality is equivalent to
   the accepted notion of compositionality crucially relies on it.  On
   June 23:

   > That is, suppose I can define a function E without structured
   > induction, and then later construct the various Phi functions that
   > satisfy what I think the compositionality equations are. So e.g.
   > Phi: M x M ---> M & forall X & Y, E[ (X Y) ] = Phi( E[ X ], E[ Y ] )
   > Now forget E altogether, and let's use my Phi functions to build
   > a new function E' by structured induction using my (already
   > constructed) Phi functions.  So isn't E'
   > function-definition-compositional, and don't we see by structured
   > induction that E' = E?

   And then on June 24:

   > As I proved in my last post, my definition is equivalent to
   > yours.  Given my E & Phi functions, use the Phi functions to
   > define by structural induction a new function E', which is
   > compositional by your definition.  Then by structural induction,
   > we see E' = E.

   So, if you define E' by structural induction using a Phi function
   that is defined in terms of E, and if E' = E, and if "functions
   don't have preferred definitions", then you defined E' using a Phi
   function that is defined in terms of E'.

   And everyone knows you can't do that.

Hah, that's pretty clever!  You're reading me pretty carefully.  But
do you see now why I'm OK?  The issue is the word "define".  Let's do
your paragraph again, highlighting define, adding subscripts:

   So, if you DEFINE E_i' by structural induction using some f_ij
   function

Mathematically it means exactly this: Call E_i' the unique functions
proved to exist by Schmidt's Thm 3.13, given the f_ij.

   that is DEFINED in terms of E_i, 

There's a formula defining f_ij in terms of the E_i.  To be precise:
Phi = f_14: Value x Value ---> Value_bottom
For U, V in Value, 
Phi(U, V) = E[ P[y <- V] ], if U = (lambda (y) P), 
            bottom,         otherwise
where E_1 is E composed with a quotient map, as Will wrote.

   and if E_i' = E_i, 

Yes, by the uniqueness of Schmidt's Thm 3.13

   and if "functions don't have preferred definitions", 

Yes, as I keep saying.  Thanks!

   then you DEFINED E_i' using some f_ij functions that are DEFINED in
   terms of E_i'.

You mixed up the 2 different defines, and your timing is funny.
The first define says we're going to run Thm 3.13 on the f_ij.

But the variables E_i' hadn't been "assigned" when we ran Thm 3.13 on
the f_ij.  There weren't any sets that we were calling E_i' at the
time in the proof when we invoked Thm 3.13.  I'm gaining sympathy to
Will's talk about lexical scope, unbound variables and quantifiers....

But even ignoring the time angle, the 2nd define has nothing to do
with structural induction.  And that's the only way to get into
trouble: by bogus structural induction.  Repeat: we never get bogus
structural induction if we restrict our structural induction
activities to invoking Schmidt's Thm 3.13.