[Editor's note: This is the complete text of yet another message by Bill Richter in this thread. I have added an editor's note.] From: Bill Richter (richter@math.northwestern.edu) Subject: Re: Clinger's sloppiness in his RichterFAQ Newsgroups: comp.lang.scheme Date: 2004-08-24 00:01:18 PST kmillikin@acm.org (Kevin Millikin) wrote in message news:<837a520f.0408230720.35ed4dbf@posting.google.com>... Kevin, I blew my response. You're doing DS, but missed this, because you didn't say "semantic domain" and "semantic functions" add & +. First I'll respond to Will, who responded to me (responding to you): I first prove my sem functions are Bill-compositional, which only requires that some equations be satisfied, mainly the one here E[ ((lambda (x) M) V) ] = Phi( E[ (lambda (x) M) ], E[ V ] ) Then by the proof of Schmidt's Thm 3.13, my sem functions E_i have a denotational definition. There's no opportunity for your "cheating" in this step: I just apply Thm 3.13 to the f_ij function I defined in the Bill-compositional phase, and, voila! Thm 3.13 gives me some functions that happen to be equal to my original E_i. [Editor's note: Bill's semantic functions are Bill-compositional, which is a notion Bill invented. Bill is counting on his readers to forget that Bill-compositionality does not imply compositionality. Bill's definition of his semantic functions is not compositional.] I'll respond to each of Will's 3 sentences: 1) Bill-compositionality is indeed my def, but I think it's the obvious interpretation of C-F's def of compositionality. 2) I counted on no forgetfulness: I addressed the matter directly: "I first prove my sem functions are Bill-compositional... Then by the proof of Schmidt's Thm 3.13, my sem functions E_i have a denotational definition." Will's verb "imply" is hard for me to parse. Bill-compositionality is a property of semantic functions, following C-F. But cls-compositionality is a property of function-definitions. So rather than say, "the sem functions have a cls-compositional def," I follow Nielson^2 and Slonneger-Kurtz and say "the sem functions have a denotational def." I guess I can say "compositional def" instead. 3) As I keep saying, Bill's first definition of his semantic functions is not compositional. But the new definition I just gave is compositional: I used Thm 3.13 to produce a compositional definition of my E_i, which of course I originally defined otherwise. [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.] Kevin, I'm going to rewrite what you wrote: One syntactic domain B_1 = N, which resembles the Natural numbers n in N n ::= 0 | n' ;; B-J use prime for successor One semantic domain D_1 = (N -> N) To give a denotational definition of a semantic function add: N ---> (N -> N) we need 2 f_ij functions: f_11 in (N -> N) ;; for 0 f_12: (N -> N) ---> (N -> N) ;; for ' You wrote add(0) = \M.M add(sN) = \M.s(add(N)(M)) which I turn easily into f_ij: f_11 = identity in (N -> N) f_12 = Phi: (N -> N) ---> (N -> N) Phi(alpha)(x) = alpha(x)', i.e. Phi(alpha) is the composite N -alpha--> N -'--> N ;; for alpha in (N -> N) So having defined the f_ij functions, there's a unique (by Schmidt's Thm 3.13) semantic function add: N ---> (N -> N) satisfying the equations add(0) = identity add(n') = add(n)' Clearly the function add looks a lot like add(n)(x) = n+x, but our N doesn't have a + op yet. At this point I don't quite follow you. You want to suppose we have a + op. But the obvious one to take is given by add, and that's obviously the correct answer, so I'll take it, as you seem to agree with that anyway. We define the binary op + : N x N ---> N, n + x := add(n)(x) And now to play my kind of games, so you define a new sem function: add(0) = \M.M add(sN) = \M.(sN + M) Let's change the names to protect the guilty, and call the new semantic function ADD: N ---> (N -> N) and you're defining it by the equations ADD(0) = identity ADD(n')(x) = n' + x Is this latter add function defined by structural induction on its argument? Two possible answers: 1. No, because it applies (+) to a subterm that is not a proper subterm of the argument, and (+) is the same function as add. 2. Yes, ... 1 might the correct "linguistic" or lexical answer. Clearly the equations above are not written in the standard compositional form. But I agree with you, that the answer is 2, because I don't think that's your question. I think you asked if ADD had a compositional definition. And the answer is yes, because (as you know) ADD = add, and add has a compositional definition. I'll prove that ADD = add: N ---> (N -> N). ADD(n')(x) = n' + x = add(n')(x) ;; by def of + So that means exactly that ADD(n') = add(n'), so ADD(n) = add(n) for every n in N that's a successor, and that means every n that's not 0. But you've already defined ADD(0) = identity = add(0). So clearly it follows (as you know well!!!) that the 2 functions are equal. \qed And since add has a compositional definition, so does ADD, because they're equal. You know the slogan, "What's mine is yours"? That's definitely true if you = me. We have the same things if we're equal. So ADD has everything add has. ADD has a compositional definition. So we'll now drop the upper case, since they're the same function. Now they even have the same name, but now I get lost: Now, given that one agrees with 2, does that mean that (+) is compositional? Again, two possible answers: I say this is a bad question, because + is a binary op, not a sem function. add is the adjoint or curry-fication of + (define (add x) (lambda (y) (+ x y))) But looking below, you seem to mean the un-curry-fication of +, which is just add again, so of course add has a compositional definition. I spent a lot of time answering the questions below & crossing them out and answering again. I don't know what you're asking. What you're calling + looks like add, with the first compositional definition. Kevin, you ended with some insults I won't respond to, because I didn't understand your +/add/compositionality biz, and because it's clear from your other post you didn't understand what I did. 2 guys who don't understand each other shouldn't flame each other on usenet. As Google keeps telling me, it's read by millions of people :)