This is a selection from messages that Dr Bill Richter has posted
to comp.lang.scheme.

================================================================

19 June 2004:

The standard miscommunication between mathematicians and physicists
goes like this: The physicists writes down a complicated Lagrangian to
integrate, and the mathematician says, "What's the range and domain of
your Lagrangian as a function?"  And that ends the discussion, but
this problem is apparently being solved in String Theory these days....

I'm not sure if E is compositional, because of this automatic
renaming.  Even if E is compositional, it might be awkward to discuss.
So I recommend that we don't insist that compositionality be part of
the definition of a DS semantic function, as some authors do.

================================================================

26 June 2004:

Good try, Joe, but you didn't actually do so.  I didn't use
transfinite induction, but I made heavy use of the ZFC subset axiom.
Strong induction over the integers and transfinite induction aren't
separate ZFC axioms that are independent from the others.  Both
induction results are consequences of the basic ZFC axioms....

================================================================

29 June 2004, quoting Clinger:

> In that case, your definition of E doesn't need to be compositional,
> and I have no idea why you have been arguing that it is.  For more
> than two years now.

For 2 reasons: 

many DS authors (such as Nielson) insist on compositionality as part
of the definition of a DS valuation function

To me, it's like conservation laws in Hamiltonian systems.
If someone tells you about conservation of angular momentum, you try
to prove it in your setup.

================================================================

3 July 2004:

BTW that's a good tip to look at Tarski's DS.  Where can we read this?

[Editor's note:  Tarski's semantics of first order logic is presented
in chapter 9 of Boolos and Jeffrey's undergraduate-level textbook,
which Richter had begun to quote quite often.]

================================================================

4 July 2004, quoting Marshall:

  I'm going to answer the rest of this tomorrow.
  
Take your time!  BTW I think you're the engine driving the thread.
I'm interested in settling old scores, although my blood pressure is
safely down now, as I realize that my Math guys are much worse :^0 
But it seems to me that several times folks have tried to stop the
thread, and you've always come through with a thoughtful technical
post for me to respond to, and that's what's kept the thread alive.

================================================================

11 July 2004:

But what I meant was: why not celebrate after a "known" bad play?

================================================================

12 July 2004:

Thanks.  I TA-ed for Rogers at MIT, I should look at his book.  I
imagine Kleene's book is too old for me to be able to read.

[Editor's note:  Kleene's "Introduction to Metamathematics" was
published in 1952.]

================================================================

18 July 2004:

So you've now done as much work as I did anyway.  I now declare your
semantics here to not be "meaningless" anymore, since you've re-proved
my result, and quite likely you've cleaned up the proof as well.

================================================================

22 July 2004, addressing Joe Marshall:

....Anyway, I yet again apologize for not reading your code.  You're code
can't be right until you first code up LC_v.  That is, beta_v
reduction modulo alpha equivalence.  I don't know how to do that
myself, and maybe environments come to the rescue here.
But the exercise would be to code up everything that F-F say, and to
note that define-less state-less Scheme gives the same answers as your
LC_v->Scheme interpreter.  Sounds like work.

================================================================

24 July 2004:

Joe, I said something dumb, and for penance, I explain below how the
ZFC axioms imply mathematical induction (from an article I googled)....

5) Proofs 3 & 4 take place in a context that CS folks may not be
familiar with, the ZFC-powered world of pure Math.  All DS takes place
there, certainly Scott models also require this pure Math world.  Will
knows quite a lot about this, but his troubles with 4 indicate that he
may not be as fluent here as I am.

6) I don't mean that the pure Math folks know what the ZFC axioms are!
Just that we pure Math folks are fluent in sets 'n functions stunts
which we understand to be derived from the ZFC axioms.  Will would be
in a much better position than I to give these ZFC-derivations.

7) I myself had trouble with the axiom of infinity, which is the reason
we have both the set of natural numbers and mathematical induction.  
I failed to understand Enderton's argument for this a while back when
we wrote about transfinite induction, but I googled article giving 
essentially Enderton's argument, so for penance, I went through it....

================================================================

24 July 2004, quoting Clinger:

   This is not just a matter of opinion, it is a matter of
   mathematics.  I have sketched a proof that there can be multiple
   solutions, and I am willing to expand that to a complete proof if
   need be.  

Sorry, I refuse to look at it.  That violates all my notions of how
Math is done.  I'll believe you, though.

================================================================

25 July 2004:

Aha!  So we're still in disagreement.  This is the sort of ZFC-rumble
I want to engage in.  Not actual rumbles about the ZFC axioms, but
pure-Math-world rumbles, however ZFC might justify the common stunts
that pure-Math-folks engage in....

   It seems that IZF (intuitionistic ZF) is gaining some intellectual
   share here.

Sounds like a real contradiction to me!  But I don't know what IZF
even means.  I'd prefer we didn't discuss that either.  Let's stick to
axiom schemes that are powerful enough to build the Scott model of LC
P(omega), which is as a set P(N).  So you need to construct N and you
need a power set axiom.  I don't think intuitionism will cut that.

================================================================

29 July 2004:

Thanks, Matthias!  Sorry, I misunderstood your English.  Here's the
one issue driving this thread: Nobody else here seems to agree with
you.  Will, Joe & Shriram have all posted that I did not successfully
define compositional semantic functions.  Can you help out?  You don't
have to, of course, but you might well be able to bring this thread to
an end if you did.  I'm sure that would make all of us happy!

================================================================

30 July 2004, quoting Marshall:

    You have not yet agreed that any version of my code is correct.  

Yeah, but I probably would have, if you'd kept writing.  You & Shriram
turned the job over to me, and I haven't been able to extricate myself
from the thread enough to finish coding.

================================================================

31 July 2004, addressing Clinger:

Before last night, I thought you were doing what my pure Math guys do:
more or less intentionally making mathematical errors for political
purposes.  It's what Orwell calls "crimestop."  It doesn't sound
particularly evil: my pure Math guys ignore bugs in the boom cycle of
their cutting edge fields, and in the bust cycle, they pretend the
bugs don't exist, & that keeps me from publishing bug-fixes.  Both are
arguably good things: the 2nd because it prevents vital human
resources from being diverted into "known" dead ends.

But now I think you genuinely believe what you say.  I don't think
you're merely keeping yourself ignorant of your obvious errors.  And I
think I know the problem: CS is close enough to the real world that
you have the temptation of falsely believing that real-world phenomena
have mathematical formulations.  No pure mathematician feels this
temptation :) Of course he real world is a great source of ideas too!
I'm sorry I formerly accused you between the lines of crime-stopping.

================================================================

31 July 2004, quoting Krishnamurthi:

   Instead of constantly finding fault with Joe's code, just post the
   code that correctly represents the semantics.
   
I'll do it.  You could help, if you wanted.  Instead of asking folks
not to post, you, Joe, MB & Will could carry on the mathematical
discussion without me.  It's really punishing, me going 1 on 4....

   That you wrote a parser is a kind courtesy, but it is hardly an
   accomplishment.  If you turned that in as a homework solution in my
   undergrad class, you would get a 0.  In short, you have so far
   written nothing.  Get on with it.

I didn't expect a higher grade.  I hoped for cooperation: you guys
actually thinking about my mathematical ideas & sensibly discussing it
among yourselves.   Instead of 4 of your attacking me at once.  

================================================================

1 August 2004, addressing Jim Bender:

Jim, I'm honored for such a distinguished schemer as you to respond to
me, so I'll say what I think the real-world temptation is, and why I'm
oblivious to it.  I really think that Will and the others want to
believe that compositionality means that there's some irreversible
flow of information from the f_ij functions to the semantic functions....

See the flow of information from the simple computable f_ij to the
curly-E?  I have this suspicion (I don't know it's true) that folks
here want to say that the definition of compositionality forces this
flow of information.  And I've proved that to be false.  If you
construct a set or function by induction, then we can see a flow of
information maybe, but folks (not A.N, Whitehead) often say that all
Math objects exist eternally in the Platonic world of Forms!

Thus, we don't create something new by constructing a set or function
by induction.  We're just getting at this (supposedly eternal) object
in a certain way.  But that's easy for me to say!  As a pure Math guy, I
have no temptation to think any other way.

But in the real world, one often sees an irreversible flow of
information.  Just think of evolution of living creatures, from
cyanobacteria 2.5 billion years to complex multicellular orgs like us.
Alg Topology doesn't have much to say about it, but nowadays,
there's a lot of interaction between Biology & CS.  I've much enjoyed
the MIT biologist Evelyn Fox Keller's accounts, e.g. in her latest
book, "Making Sense of Life", I think.  So folks here might feel a
temptation to try to mathematize irreversible flow of information.

I can't think of anything else that would account for the spectacular
flame-war that Will & I are engaged in.  If you want to get good at
DS, you should go "weight-lifting" at the point-set Topology gym.  In
fact, Scott models are strange animals in the point-set Topology zoo!
And I bet Will is better than I at point-set Topology, although I've
done lots of weight-lifting in related areas.  The only thing I can
think of to account for our feud is that Will, whose Math skills are
more than good enough to understand me, has this overwhelming cultural
problem to surmount, involving irreversible flow of information.

Anyway, they want to me to code up my DS, which is sorta strange, as
my DS is really just OpS plus some non-computable Math, so that means
I'm coding up the original OpS, which is Felleisen-Flatt's LC_v.  But
I like the exercise, and I'm now up to 350 lines of code, and another
100 lines of tests, and beta_v reduction seems to be working, and also
code to find the leftmost redex, and that doesn't seem to be working.

================================================================

5 August 2004, quoting Marshall:

   I want you to add the following primitive procedure to your language:
     (DISPLAY <expression>)
   
Joe, this looks like real work to this humble schemer...

But since you're here, let me answer something David asked, and you
might be interested in this too.  David asked:

   > > > That is, if E is an LC_v expr that doesn't standard-reduce to
   > > > a value in finite time, we send it to bottom,
   
   if the construction is founded on an undecidable proposition (the
   expr doesn't reduce in finite time), how can the construction be
   used to build anything else? 

An engineer cannot build my non-computable function

E: LC_vExp ---> Value_bottom

by the Halting problem.  But an engineer can't build F-F's computable
partial function either: 

|--->>_v : LC_vExp ----> Value

Possibly folks (not Will) are confused on this point.  What the
engineer can do is build one function given the other.  If you hand an
engineer the partial function |--->>_v, they can build the total
function E.  Or vice versa.  The point is:

To say that a partial function is computable doesn't mean it's a 
procedure.  A computable partial function is only defined by a 
procedure on its subset of definition.

================================================================

6 August 2004:

   > To say that a partial function is computable doesn't mean it's a
   > procedure.

   In the Appendix of Alan Turing's paper ``On computable numbers,
   with an application to the Entscheidungsproblem'' he proves that
   computable functions are exactly those for which an effective
   procedure exists.

There's no contradiction between what I posted (above & below) & what
Turing wrote.  Turing's effective procedure is not _equal_ to the
partial function.  The effective procedure _plus_ modern pure Math
determines a unique partial function.  The reason why we need the
noncomputable pure Math is:
   
   > A computable partial function is only defined by a procedure on
   > its subset of definition.

   A partial function is only defined on a subset of its domain.

Right.  But that subset is included in the definition of the partial
function.  That has to be true, even if you never read it, Joe.
Otherwise, the concept of partial function takes place outside the
framework of modern pure Math, which is all about sets (in a model of
ZFC) and functions (which as you know are sets too).

[Editor's note:  See the excerpt below for 8 August.]

================================================================

8 August 2004:

Please critique my reasoning: I define a partial
function X -> Y as the following kind of set:

R subset  X x Y

s.t. \forall x, y in X (x, y) in R & (x, y') in R => y = y'

I can't imagine any other set-based definition of partial function.
But then we read of the actual domain of R by projecting onto X.

actual-domain(R) = {x in X : \exists y in Y s.t. (x, y) in R}

That's why the actual domain of a partial function is part of the
partial function.  And that's why a computable partial function is
more than just the procedure that computes the partial function on its
actual domain.  The procedure cannot itself tell us what the actual
domain of a partial function is.  And that's why I was right in the
post Joe responded to (failing to agree with me):

   > An engineer cannot build my non-computable function
   >
   > E: LC_vExp ---> Value_bottom
   >
   > by the Halting problem.  But an engineer can't build F-F's
   > computable partial function either:
   >
   > |--->>_v : LC_vExp ----> Value

The "engineer" can only compute |--->>_v on its actual domain.
The"engineer" can't know the actual domain, because of Halting.

[Editor's note:  All of Bill's arguments concerning what an engineer
can't do or know apply equally to mathematicians, but Bill appears
to believe that pure mathematicians transcend these limitations by
working at some higher "semantic" plane of metaphysical reality.
See the excerpt for 13 August, below.]

================================================================

9 August 2004:

Joe, this post indicates you don't yet understand the definition of a
partial function.  The partial function |--->>_v is a subset

R subset LC_vExp x Value

The projection of R to LC_vExp is a noncomputable set

Halt = { x in LC_vExp : x standard-reduces to a value }  

So it's ludicrous to assert that a machine can compute R....

[Editor's note:  What Bill calls ludicrous is standard practice.
R is a partial recursive function.  That *means* there is some
Turing machine M that computes R.  The domain of R, Bill's Halt,
is then said to be the set enumerated by M.  That set is said
to be a recursively enumerable set.]

....The actual domain is often an
uncomputable set, and the machine does not "compute" that.

[Editor's note:  The domain of a partial recursive function is
often not recursive, but it is always recursively enumerable,
and the machine that computes the partial function is said to
enumerate the partial function's domain.  To avoid the confusion
that afflicts Bill, recursion theorists do not speak of sets as
computable or uncomputable.]

================================================================

13 August 2004, quoting Lauri Alanko:

   ZFC is pretty darn powerful (especially the "C" bit), so if you go
   beyond it, you had better state exactly what additional logical or
   mathematical assumptions you make.

Yeah, well said.  Please, jump into the thread, before it goes down in
flames.  Look up my old posts on Bill=c.l.s.-compositionality, and
churn out some sensible response.  Don't defer to your elders.
   
   Or if you just mean that you believe that your proofs are
   formalizable in ZFC but you do not want to have to do it, then just
   say so, there's nothing strange in that. I believe that to be the
   usual attitude of mathematicians. :)

Ah, you said it perfectly.  But there's an interesting point here,
which I learned from one of Will's posts: in syntactic ZFC proofs, we
must seriously worry about variable capture issues.  It's very
important to realize that pure Math (including DS) is entirely carried
out in the semantics of ZFC, and not the syntax.  As I keep saying,
and you cited, a functions (which is a set) doesn't have a definition....

[Editor's note:  Bill appears to be rationalizing his sloppy, even
fallacious mathematical exposition by postulating a "semantic" fantasy
world in which pure mathematicians (but not engineers!) refer directly
to sets and functions without using language, and construct particular
sets and functions without defining them.]

================================================================

14 August 2004:

It's meaningless to say that one set
"uses" or is "defined in terms of" another set.  This is the
difference between ZFC syntactic proofs, where variable capture is a
real issue, and the "semantic proofs" that pure mathematicians make,
where variable capture is a useful rule of thumb, but no more.

================================================================

15 August 2004, quoting Alanko quoting Richter:

   > But informal isn't really the right word, as formal would mean
   > axiomatic or syntactic proofs, which a computer could perform.
   > My "semantic proofs" are indeed more informal, but it's not
   > informal syntax.  It takes place in the model.
   
   This again makes very little sense. The best I can think of is to
   interpret you to claim that your mathematical assumptions are
   consistent (i.e. they have a model). This of course is just as true
   (or false) of formal as well as informal theories.

No, no.  It's largely the difference between syntax & semantics in
Math Logic.  Pure Math consists of statement, constructions, theorems
& proofs that can probably be justified by axiomatic ZFC syntactic
proofs.  But pure Math isn't done that way at all.  Pure Math that
some ZFC model exists, and then does statements & proofs in this
model.  That's quite different from syntactic statements & proofs.

[Editor's note:  If proofs were done in some model of ZFC, as Bill
here claims, they would not be valid proofs.  A valid proof cannot
depend on any one model.  It must hold for all models.]

....But I
guess there's a selection effect: folks with a lot of pure Math talent
who can't stand it (presumably you & Will) switch to Logic & CS.

================================================================

28 August 2004, quoting Aatu Koskensilta:

   If it bugs you, that's a good indication that your understanding of
   axiomatic set theory and logic is too superficial to serve any
   useful purpose.

Aatu, I don't see any purpose to your trash-talking here.  The issue
is not whether I have a good understanding of axiomatic set theory and
logic.  I've posted over & over that I don't understand it very well,
and it's Will's biggest contribution to me in this thread: explaining
how poorly I (and my pure Math pals) actually understand ZFC.

The issue is: what logical framework that DS and Point Set Topology
take place in?  The obvious answer is the set theory framework of
Halmos's book Naive Set Theory, where he assumes there exists a set
theoretic universe V, in which the ZFC axioms hold.  And you have no
business insulting my (meager) set theory skills when you posted last
time an idiotic question....

Since you include the Wittgenstein quote ("shuddup about whatcha don't
know"), I suppose you're saying I shouldn't post about ZFC since I'm
not an expert in ZFC models, or axiomatic set theory and logic.

But I reject such a point.  Folks here don't seem to understand that
all the DS we're talking about is statements, proofs and constructions
about sets, and the ZFC axioms hold for the sets we use.  Instead of
carping about my lousy understanding of ZFC, why don't you make an
actual contribution to the discussion, by helping to explain this?

[Editor's note:  ZFC is irrelevant to the discussion, but Bill has
mentioned ZFC in 65 of his 242 messages.  The reason is apparent:
He believed ZFC to be too arcane for anyone here to understand, and
hoped his references to ZFC in every fourth message might intimidate
or at least impress readers who would otherwise see right through his
flimsy arguments.  We were impressed, all right---by the foolishness
of a man who flunked two undergraduate courses in logic and has only
a superficial knowledge of set theory, yet insists upon the centrality
of those topics in this discussion of programming language semantics.
What's more, this charlatan brazenly lectured us concerning logic and
set theory, saying his experience as a pure mathematician made him
more expert than other mathematicians who have actually studied those
subjects.  See, for example, the excerpts above for 26 June, 24 July,
25 July, and 14 August.]

================================================================

3 September 2004, quoting David Rush:

   Then you need to get yourself some real credentials (Usenet is
   meaningless to the world of refereed papers) 

I've got real pure Math credential (uh, amassed in the dim past).

   and shoot these guys down in fora like ACM SIGPLAN, Lisp & FP,
   POPL, &cet.

But you guys are the only people I'm interested in arguing with!  Hey
that's good, I didn't know fora was a word :)

================================================================

3 September 2004:

I always kinda get a kick outta the crazy feuds, even though I rarely
have any clue what's being argued about.

================================================================