Scheme - Usenet category theory

Author

Usenet category theory

William D Clinger

2004-08-05, 3:59 pm

Pure mathematicians like to classify mathematical things: finite
simple groups, systems of differential equations, topological spaces,
and so on.

A classification of non-mathematical things would streamline our
posts and make our newsgroup discussions more efficient. While
reviewing recent threads, I observed that the points being made
generally fell into one of the following broad categories:

Category 0: Correct and germane.
Category 1: So-and-so is competent.
Category 2: So-and-so is not.
Category 3: So-and-so doesn't understand what so-and-so meant.
Category 4: Incorrect statements and fallacious arguments.
Category 5: Irrelevancy.
Category 6: Lunacy.

These categories are not mutually exclusive, and there are arrows
that relate one category to another, but let's not chase them.

There are seven other categories dual to those above, consisting
of statements that attempt to refute, to challenge, or to mock a
statement that falls into one of the above seven categories. I
propose we overload our nomenclature to refer to both the seven
categories above and to their duals, relying on the "From:" field
and other context to distinguish each category from its dual.

Here, for example, is the category-theoretic content of a 40-line
message posted to comp.lang.scheme on 4 August 2004:

Category 1. Category 5. Category 3. Category 2.
Category 0.
Category 0. Category 4. Category 2. Category 2. Category 6.
Category 0.
Category 0. Category 4. Category 6.

Mnemonically:

Competent. Irrelevant. Incomprehending. Incompetent.
Germane.
Germane. Incorrect. Incompetent. Incompetent. Surreal.
Germane.
Germane. Incorrect. Surreal.

Another example: Instead of writing the post I am writing now,
I could simply have written "Category 6".

See how much easier this is to write, to read, to understand?

Will

Matthias Blume

2004-08-05, 3:59 pm

cesuraSPAM@verizon.net (William D Clinger) writes:

....
> Category 4: Incorrect statements and fallacious arguments.
....
> Category 6: Lunacy.

The problem with these two is that those who post in one of them would
not know -- unless they do it on purpose. But in that case they
should rather go under:

Category 7: flame bait (aka. troll)

Matthias

PS: I admit that the article you are reading straddles the boundaries
between categories 2, 5, and 7.

Shriram Krishnamurthi

2004-08-05, 3:59 pm

Category 5. Category 6. Category 5.

Shriram

Ron Garret

2004-08-05, 3:59 pm

In article <fb74251e.0408050523.5b027405@posting.google.com>,
cesuraSPAM@verizon.net (William D Clinger) wrote:

> Another example: Instead of writing the post I am writing now,
> I could simply have written "Category 6".
>
> See how much easier this is to write, to read, to understand?

http://underground.musenet.org:8080/utnebury/puzzle.txt

RG

Joe Marshall

2004-08-05, 3:59 pm

cesuraSPAM@verizon.net (William D Clinger) writes:

> Pure mathematicians like to classify mathematical things: finite
> simple groups, systems of differential equations, topological spaces,
> and so on.
>
> A classification of non-mathematical things would streamline our
> posts and make our newsgroup discussions more efficient. While
> reviewing recent threads, I observed that the points being made
> generally fell into one of the following broad categories:
>
> Category 0: Correct and germane.
> Category 1: So-and-so is competent.
> Category 2: So-and-so is not.
> Category 3: So-and-so doesn't understand what so-and-so meant.
> Category 4: Incorrect statements and fallacious arguments.
> Category 5: Irrelevancy.
> Category 6: Lunacy.
>
> These categories are not mutually exclusive, and there are arrows
> that relate one category to another, but let's not chase them.

Some of these posts are epic, so you need a lemma --- in fact, the
Yoneda lemma. This would naturally transform the category. I'd
suggest one in which we can do lambda calculus, but I hear that it's
closed. However, I understand there may be a free topos available.

I just don't want to end up Heyting algebra.

Jens Axel Søgaard

2004-08-05, 8:57 pm

Shriram Krishnamurthi wrote:

> Category 5. Category 6. Category 5.

Category 0.

Jens Axel

William D Clinger

2004-08-05, 8:57 pm

Category theoretic abstract:
Category 6. Category 1. Category 1. Category 4. Category 0.

Category theoretic abstract of category theoretic abstract:
Category 7.

Open problem: Characterize all fixed points of the category
theoretic abstraction function.

> ...
>
> The problem with these two is that those who post in one of them would
> not know -- unless they do it on purpose. But in that case they
> should rather go under:
>
> Category 7: flame bait (aka. troll)
>
> Matthias

You're completely right, Matthias, but so am I. As a pure Usenet
category theorist, I don't care about categorizability.

Will

Anton van Straaten

2004-08-06, 3:56 am

William D Clinger wrote:
> Pure mathematicians like to classify mathematical things: finite
> simple groups, systems of differential equations, topological spaces,
> and so on.
>
> A classification of non-mathematical things would streamline our
> posts and make our newsgroup discussions more efficient. While
> reviewing recent threads, [...]

Speaking of mathematicians, I will take the liberty of adding both another
category, Category 7 - Tangential but (Possibly) Relevant - along with a
post in that category:

My own review of recent threads brought to mind a quote which I noticed in
the book "Dr. Riemann's Zero's", by Karl Sabbagh. The quote is by the
"brilliant French mathematician" Alain Connes, who "devised his own system
of mathematics for solving the problems he was presented with in class."
Connes described this as follows:

"What happened was that I first began to work in a very small place in
the mathematical geography. This meant that I had a strange and polarized
view of things which was peculiar to me, and somehow from then on I
travelled through many other places, but without ever breaking this thread
which I had created from the beginning and which was giving me a particular
point of view, quite different from the standard point of view. So I had my
own system, which was very strange because when the problems that the
teacher was asking fell into my system then of course I would have an
instant answer, but when they didn't - and many problems, of course, didn't
fall into my system - then I would be like an idiot, and I wouldn't care."

Anton

Bill Richter

2004-08-06, 4:00 pm

"Anton van Straaten" <antonvs@acm.org> responded to Will Clinger:

I was wondering when you'd join the thread, Anton :) Welcome aboard.
That's a great quote of Connes, who is indeed a brilliant French
mathematician, he's got a Fields medal. Dunno who you thought this
applied to, me or Will :)

"So I had my own system, which was very strange because when the
problems that the teacher was asking fell into my system then of
course I would have an instant answer, but when they didn't - and
many problems, of course, didn't fall into my system - then I would
be like an idiot, and I wouldn't care."

BTW I was amazed that Joe knew about the Yoneda lemma, which is how we
construct products in Ext in Algebraic Topology. I knew there was
some Category Theory being used in CS these days, but Ext groups?

BTW again for Joe, on the other thread: Joe wanted to add in display,
and I said it would be hard and destroy the BNF/struct biz, but I
think that was nonsense. I think all you have to do is change in
addition this function:

(define (1ary-prim-function op)
;; 1aryPrimOp ---> (Integer -> LC_vValue)
(cond
[(symbol=? 'zero? op)
(lambda (n)
(if (= 0 n)
LC_v-true
LC_v-false))]
[(symbol=? '- op) -]
[(symbol=? 'add1 op) add1]
[(symbol=? 'sub1 op) sub1]))

I assume that you only need to insert one extra cond clause:

[(symbol=? 'display op)
(lambda (arg)
(begin
(display arg)
arg))]

if that's what he wanted, on top of what I already posted to Joe:

(define 1aryPrimOp
(list 'zero? '- 'add1 'sub1 'display))

Anyway, code isn't just to read, it's to modify & run. If you just want
to read it, you could read my crystal clear math posts.

My position is solidifying anyway. Here's what I say happened:

1) I posted crystal clear proofs that I had defined some semantic
functions that satisfied compositionality.

2) Will maybe was the only person who cared, and he flamed me to heck
& gone about errors that I absolutely did not make.

3) I don't know if Will made any actual mathematical errors of his
own. Seems to me the problem was that he couldn't understand what I
wrote, and mistranslated it. What Category is that?

I'm not at all sure I can detect any actual errors in Will's
work, other than maybe his claim that compositionality was a property of
the _definitions_ of the semantic functions, rather than the
semantic functions themselves. But I hesitate to call that an error,
because Will merely didn't respond to my post correcting him.
Possibly he silently agreed I was right, or he's working up a response.

4) But I think I can say this with confidence: Will's failure to
understand me shows Will's lack of fluency in the lingo of pure Math.
None of the pure mathematicians I know would have had any trouble
understanding what I wrote. Now that's just a cultural remark, but

5) Arguably, pure Math fluency is a good thing for CS, since, as I
claim, DS takes place in the world of modern pure Math. For instance,
Scott's model P(omega) of LC is an object in point-set Topology.

Joe Marshall

2004-08-06, 8:56 pm

richter@math.northwestern.edu (Bill Richter) writes:

> BTW I was amazed that Joe knew about the Yoneda lemma, which is how we
> construct products in Ext in Algebraic Topology. I knew there was
> some Category Theory being used in CS these days, but Ext groups?

You never know what I might know.

> BTW again for Joe, on the other thread: Joe wanted to add in display,
> and I said it would be hard and destroy the BNF/struct biz, but I
> think that was nonsense. I think all you have to do is change in
> addition this function:
>
> (define (1ary-prim-function op)
> ;; 1aryPrimOp ---> (Integer -> LC_vValue)
> (cond
> [(symbol=? 'zero? op)
> (lambda (n)
> (if (= 0 n)
> LC_v-true
> LC_v-false))]
> [(symbol=? '- op) -]
> [(symbol=? 'add1 op) add1]
> [(symbol=? 'sub1 op) sub1]))
>
> I assume that you only need to insert one extra cond clause:
>
> [(symbol=? 'display op)
> (lambda (arg)
> (begin
> (display arg)
> arg))]
>
> if that's what he wanted, on top of what I already posted to Joe:
>
> (define 1aryPrimOp
> (list 'zero? '- 'add1 'sub1 'display))
>
> Anyway, code isn't just to read, it's to modify & run.

Yes, and this precisely illustrates the problem. Define expa, expa1,
and expa2 as these:

(define expa '(((lambda (f)
((lambda (x) (x x))
(lambda (x)
(f (lambda (p) ((x x) p))))))
(lambda (f)
(lambda (n)
(if0 n
(display 1)
(* n (f (sub1 n))))))) 2))

(define exp1a (Exp-parser expa))
(define exp2a (Exp->LC_v exp1a))

(E exp2) is the `Bill semantics' of exp2.
(E exp2a) is the `Bill semantics' of exp2a.
Both are `2', which would indicate that these two programs have the
same `meaning'. But the two programs do not in fact have the same
meaning. The second program has some output that the first does not.

We notice something else: when computing the semantics of exp2a, the
number 1 is printed. The act of printing numbers is not properly part
of the semantics, it is part of the program. When we run a program,
we expect it to print 1, but we hardly expect to see output when we
*analyze* the program (I don't feel an overwhelming desire to write
the number 1 when reading Bill's code).

A denotational semantic function (such as the one Matthias Blume wrote
in ML) would not print 1 and it would produce different denotations
for exp2 and exp2a.

The simple conclusion is this:

E is an evaluator, not a semantic function.

The fact that (E exp2) produces a value equivalent to what we would
expect from a semantic analysis shows that E is correctly implemented.
This makes it difficult to show that E is *not* a semantic function
because a correctly implemented E ought to produce the answer that the
semantics dictate. But a semantic function is a mapping, not a
process. (A program has the same meaning even if you don't run it!)
With the addition of an output function, we can easily see that E
executes the program rather than analyzing it.

> If you just want to read it, you could read my crystal clear math
> posts.

Iron pyrite forms wonderful crystals.

--
~jrm

Anton van Straaten

2004-08-07, 3:56 am

Bill Richter wrote:
> I was wondering when you'd join the thread, Anton :) Welcome aboard.

I'd have to work too hard to make even Category 4 posts in these threads,
and I have neither tenure nor a trust fund. I'm pretty good at Category 5
(e.g. this post).

> That's a great quote of Connes, who is indeed a brilliant French
> mathematician, he's got a Fields medal. Dunno who you thought
> this applied to, me or Will :)

The brilliance in this case is a red herring: Connes' brilliance would be
unknown unless he eventually succeeded either in escaping his own unique
system, or in using it to unusually good effect. I haven't noticed evidence
of either of those outcomes here.

But perhaps I'm merely impatient, and you have a plan, such as the Parker &
Stone three-step plan:

1. Torture-test Bill-semantics on c.l.scheme
2. ???
3. Fields medal!

Anton

Bill Richter

2004-08-09, 3:56 am

Joe Marshall <prunesquallor@comcast.net> responds to me:

[Sorry if this is a repeat: my post did not seem to go through.]
> BTW I was amazed that Joe knew about the Yoneda lemma, which is
> how we construct products in Ext in Algebraic Topology.

You never know what I might know.

You're right, Joe, I don't. Please post something explaining your
Math level. It was helpful to me when Will explained his Bing college
point-set Topology background.

Define expa, expa1, and expa2 as these:

(define expa '(((lambda (f)
((lambda (x) (x x))
(lambda (x)
(f (lambda (p) ((x x) p))))))
(lambda (f)
(lambda (n)
(if0 n
(display 1)
(* n (f (sub1 n))))))) 2))

OK, that's your Scheme code for 2!, with a display.

(define exp1a (Exp-parser expa))

exp1a belongs to the syntactic domain Exp

(define exp2a (Exp->LC_v exp1a))

exp2a belongs to the "hybrid" set LC_vExp.

(E exp2) is the `Bill semantics' of exp2.

I think by exp2, you mean a version of this from my web page
<http://www.math.northwestern.edu/~richter/lc_v.scm> that does not
have the display in it.

(E exp2a) is the `Bill semantics' of exp2a.

Well, no, because of the display, as you explain:

Both are `2', which would indicate that these two programs have the
same `meaning'. But the two programs do not in fact have the same
meaning. The second program has some output that the first does
not.

Very clever! So I can't at this stage put display in my simple ISWIM
language. Well, it was your idea! I think the upshot is that that
you need continuations for things like display and error messages. I
imagine you know this quite well. You might note that my code
contains lots of error messages, like in the definition of \|--->_v:

(if (LC_vValue? proc)
(if (abstraction? proc)
(if (LC_vValue? arg)
(beta_v-reduce exp)
(make-comb proc (\|--->_v arg)))
(begin
(printf "proc ~vis not an abstraction~n"
(LC_vExp-print proc))
false))

But the printf is just taking advantage of Scheme capability. It's
not really part of my LC_v->Scheme interpreter.

We notice something else: when computing the semantics of exp2a,
the number 1 is printed. The act of printing numbers is not
properly part of the semantics, it is part of the program. When we
run a program, we expect it to print 1, but we hardly expect to see
output when we *analyze* the program (I don't feel an overwhelming
desire to write the number 1 when reading Bill's code).

Let me restate: with the display, E[5!] = 120, but the program
first displays
5 4 3 2 1
That's not part of my semantics. It's something you asked me to add
to the code, and to my surprise, it was easy.

A denotational semantic function (such as the one Matthias Blume
wrote in ML) would not print 1 and it would produce different
denotations for exp2 and exp2a.

Right, assuming that display is part of the language. It wasn't part
of mine.
The simple conclusion is this:

E is an evaluator, not a semantic function.

No, and this display biz proves nothing. I defined E as a total
function between 2 sets

E: Exp ---> Value_bottom

and nobody so far said I can't call E a "semantic function". It's
certainly a function. The purpose of me coding was for you to
understand how E was defined, and whether it was well-defined, or
fulla bogus mutual recursion. How are you coming with this?

But a semantic function is a mapping, not a process. (A program has
the same meaning even if you don't run it!) With the addition of
an output function, we can easily see that E executes the program
rather than analyzing it.

That's meaningless, at least for the map = math-function

E: Exp ---> Value_bottom

Analyze & execute aren't adjectives of a map = math-function. If you
want to haggle about whether I can call E a "semantic" map, OK.

And then there's the Scheme procedure E I coded up. The procedure E
seems to execute the program, I don't dispute that. But I only coded
up the Scheme procedure E to help folks understand the map E.

> If you just want to read it, you could read my crystal clear math
> posts.

Iron pyrite forms wonderful crystals.

Isn't that fools gold? A funny joke, even at my expense! Thanks,
Joe. It's my adviser's phrase, crystal clear, so I'll use your joke
on him the next time he says something he wrote was crystal clear.

Joe Marshall

2004-08-10, 3:57 am

richter@math.northwestern.edu (Bill Richter) writes:

> The simple conclusion is this:
>
> E is an evaluator, not a semantic function.
>
> No, and this display biz proves nothing.

Another math question: If E is not an evaluator, then there is some
behavior of E that differs from that of an evaluator. Show me one.

The display biz shows that E is evaluating the program.

> I defined E as a total function between 2 sets
>
> E: Exp ---> Value_bottom
>
> and nobody so far said I can't call E a "semantic function".

You really should read our responses. Time after time I have said
that E is not a semantic function by any usual definition.

> It's certainly a function.

I don't think so.

> The purpose of me coding was for you to
> understand how E was defined, and whether it was well-defined, or
> fulla bogus mutual recursion. How are you coming with this?

I'm attempting to put together a proof that E is not a well-defined
function. It is a complicated proof and it may take some time.

> But a semantic function is a mapping, not a process. (A program has
> the same meaning even if you don't run it!) With the addition of
> an output function, we can easily see that E executes the program
> rather than analyzing it.
>
> That's meaningless, at least for the map = math-function
>
> E: Exp ---> Value_bottom
>
> Analyze & execute aren't adjectives of a map = math-function.

Exactly my point. Why is something being printed?

--
~jrm

Bill Richter

2004-08-10, 3:57 am

Joe Marshall <prunesquallor@comcast.net> responded to me:

> The simple conclusion is this:
>
> E is an evaluator, not a semantic function.
>
> No, and this display biz proves nothing.

Another math question: If E is not an evaluator, then there is some
behavior of E that differs from that of an evaluator. Show me one.

Joe, this is apples vs oranges. My total maps = math-functions

EE_1: Exp ---> Value_bottom
E: LC_vExp ---> Value_bottom

are not an evaluators, because evaluator is not a word that's used to
describe a map = math-function. The code I wrote for E looks like an
evaluator, sure. That's obvious to all, and of no interest here.

If you think it's impossible to turn OpS into total functions such as

Exp ----> M

then you haven't understood Will's ISWIM posts.

> I defined E as a total function between 2 sets
>
> E: Exp ---> Value_bottom
>
> and nobody so far said I can't call E a "semantic function".

You really should read our responses. Time after time I have said
that E is not a semantic function by any usual definition.

Sorry, I meant "nobody else". You made this objection, but Will & MB
did not. Will & MB in their posts used the term "semantic function"
to refer to their OpS-ized maps = math-functions. If you won't defer
to Will & MB, then by all means, let's stop calling my map EE_1 a
semantic function. They're certainly maps = math-functions.

Actually there's a possibly serious typo above: my E above should be
EE_1. Certainly my map

E: LC_vExp ---> Value_bottom

is not a semantic function.

> It's certainly a function.

I don't think so.

Of course it is, but you don't yet understand my mathematical
description of my total maps = math-functions

EE_1: Exp ---> Value_bottom

E: LC_vExp ---> Value_bottom

I guess you're in good company.

> The purpose of me coding was for you to understand how E was
> defined, and whether it was well-defined, or fulla bogus mutual
> recursion. How are you coming with this?

I'm attempting to put together a proof that E is not a well-defined
function. It is a complicated proof and it may take some time.

It sounds like nonsense, and I advise you to quit now. My guess is
that you're just looking at my code & thinking of ways it's not DS.
That's won't prove anything IMO, because it won't have anything to do
with my actual map = math-function E. The only way you can prove
anything about my E is to work with it directly. The only purpose of
my code was to help was to help you understand my maps E & EE_1.

> But a semantic function is a mapping, not a process. (A
> program has the same meaning even if you don't run it!) With
> the addition of an output function, we can easily see that E
> executes the program rather than analyzing it.
>
> That's meaningless, at least for the map = math-function
>
> E: Exp ---> Value_bottom
>
> Analyze & execute aren't adjectives of a map = math-function.

Exactly my point. Why is something being printed?

Only because you asked me to do it!!! My semantic function can't
handle printing. That is, my map = math-function

E: Exp ---> Value_bottom

cannot have display as a primitive 1-ary function. I think I'd need
continuations to handle display. But you asked me to make the change,
and I did, because it was a good programming exercise.

It's like if you got me to add the print statement

(print "1 = 0")

And you said, "That's a contradiction! You proved that 1 = 0!"

Shriram Krishnamurthi

2004-08-10, 9:02 pm

Bill,

In cls today I find two posts from you. The first is mad at the rest
of the world for treating you like a blithering idiot. Now you go on
to say,

> Joe, this is apples vs oranges. My total maps = math-functions
>
> EE_1: Exp ---> Value_bottom
> E: LC_vExp ---> Value_bottom
>
> are not an evaluators, because evaluator is not a word that's used to
> describe a map = math-function. The code I wrote for E looks like an
> evaluator, sure. That's obvious to all, and of no interest here.

and about 30 lines later,

> Actually there's a possibly serious typo above: my E above should be
> EE_1. Certainly my map
>
> E: LC_vExp ---> Value_bottom
>
> is not a semantic function.

Do you see why people might treat you this way? (That's a rhetorical
question -- ponder it for a moment, don't follow-up to it.)

1. You don't evince ability to use a text editor. Apparently you
think a stream-of-consciousness drool is worth everybody else's time
to have to follow.

2. You get

even over your own fundamental claims.

3. On top of all that, you use the weasel word "possibly", which
suggests you don't even understand your fundamental claims, and make
them up as you go along.

>
> Exactly my point. Why is something being printed?
>
> Only because you asked me to do it!!! My semantic function can't
> handle printing.

Rubbish. For a w

you went on about how simple it would be to
handle printing. Your complaint was *never* about the fact that it
was inconsistent with the semantics or other argument at that level:
it was about your lack of experience as a Schemer. It was evident all
along that you didn't see where Joe was leading you, as witnessed by
your confusion suggesting Joe add printing statements to monitor the
interpreter itself. When you figured out the code, you happily posted
it. Now you cannot retract it.

> cannot have display as a primitive 1-ary function. I think I'd need
> continuations to handle display. But you asked me to make the change,
> and I did, because it was a good programming exercise.

1. So what's on the Web no longer captures your semantics? This
violates your own promise. You should have refused to add it. You
knew darn well that you were implementing your semantics, not writing
random code.

2. The "continuations" (whatever magical properties they posess to
help you out here) wouldn't address Joe's core concern, at least not
in any way that I can see.

> It's like if you got me to add the print statement
>
> (print "1 = 0")
>
> And you said, "That's a contradiction! You proved that 1 = 0!"

This analogy is nonsensical at so many levels I won't even begin to
address them, for fear you will use that as a distraction from the
knot Joe very elegantly tied.

Shriram

Joe Marshall

2004-08-10, 9:02 pm

richter@math.northwestern.edu (Bill Richter) writes:

> Joe Marshall <prunesquallor@comcast.net> responded to me:
>
>
> Another math question: If E is not an evaluator, then there is some
> behavior of E that differs from that of an evaluator. Show me one.
>
> Joe, this is apples vs oranges. My total maps = math-functions
>
> EE_1: Exp ---> Value_bottom
> E: LC_vExp ---> Value_bottom
>
> are not an evaluators, because evaluator is not a word that's used to
> describe a map = math-function. The code I wrote for E looks like an
> evaluator, sure. That's obvious to all, and of no interest here.

I refer you to my post of Jul 30:

Your definition of semantics is this:

``The meaning of an expression is what you would get if you
evaluate it.''

I will certainly retract this.

I go on to say:

It's silly enough to define EE_1 [[EXP]] as (lambda () (e 'EXP)),
which says

``The meaning is what you *would* get *if* you ran the
program.''

but it is ludicrous to say EE_1 [[EXP]] = (e 'EXP), which says

``The meaning is defined only by running the program and is not
defined otherwise.''

You are clearly asserting this latter.

> If you think it's impossible to turn OpS into total functions such as
>
> Exp ----> M
>
> then you haven't understood Will's ISWIM posts.

I certainly do think that OpS is isomorphic to DS, (see Chapter 24 of
Open Problems in Topology, J. van Mill and G.M. Reed (Editors),
Elsevier Science Publishers B.V. (North-Holland), 1990,
<http://www1.elsevier.com/homepage/s.../24/article.pdf>
).

> I'm attempting to put together a proof that E is not a well-defined
> function. It is a complicated proof and it may take some time.
>
> It sounds like nonsense, and I advise you to quit now. My guess is
> that you're just looking at my code & thinking of ways it's not DS.

No, actually, I'm constructing an expression for which E cannot
logically assign a value (thus E will either be non-total,
non-well-defined, or a non-function). That's not particularly
difficult, but the construction involves creating an isomorphism for E
in the domain of ISWIM. As ISWIM is rather primitive, a
straightforward construction would be huge. It is unlikely that you
would be willing to follow it.

My effort has been in seeing if I can reduce the proof to something
much smaller.

>
> Exactly my point. Why is something being printed?
>
> Only because you asked me to do it!!! My semantic function can't
> handle printing. That is, my map = math-function
>
> E: Exp ---> Value_bottom
>
> cannot have display as a primitive 1-ary function.

This casts doubt on all the other primitive functions as well. I
assert that when presented with a primitive application, you are not
determining the `semantics', but rather just executing the primitive.

> I think I'd need continuations to handle display. But you asked me
> to make the change, and I did, because it was a good programming
> exercise.

Feel free to add what you think you need.

Bill Richter

2004-08-11, 4:01 am

Joe Marshall <jrm@ccs.neu.edu> responds to me:

Joe, let's just forget the word "semantic", OK? So we don't have to
talk about stuff like this anymore:

``The meaning is defined only by running the program and is not
defined otherwise.''

You are clearly asserting this latter.

I only claim I defined some total maps = math-functions

EE_1: Exp ---> Value_bottom
E: LC_vExp ---> Value_bottom

(There's compositionality claims too, but they have to wait on
well-definedness.) If you say these maps E & EE_1 are not
well-defined, you're going to find an error in my mathematical
definitions, so you'll probably have to read my 2 ISWIM posts. You
don't seem to have done so yet. The code I wrote is only something
that might help you understand my math. The code certainly can't
explain all the math, since E & EE_1 are noncomputable functions.

It's completely blitheringly obvious that my map E is well defined.
F-F claim that their |--->>_v is a well-defined partial function, and
you seem to believe this. As I posted to Shriram, this immediately
implies that my total map

E: LC_vExp ---> Value_bottom

E[ M ] = V in Value, if M |--->>_v V
bottom, otherwise

is a well defined math-function = map. If you don't understand this,
that's what we need to talk about. But all you only need to know is
what a partial function is. You can't replace the partial function by
the procedure which computes it on the set

{x in LC_vExp : (|--->>_v x) is defined }

> If you think it's impossible to turn OpS into total functions such as
>
> Exp ----> M
>
> then you haven't understood Will's ISWIM posts.

I certainly do think that OpS is isomorphic to DS, (see Chapter 24
of Open Problems in Topology, J. van Mill and G.M. Reed (Editors),
Elsevier Science Publishers B.V. (North-Holland), 1990,
<http://www1.elsevier.com/homepage/s.../24/article.pdf> ).

Thanks for the reference, I printed it out, but it looks like tough
sledding (to quote Marathon Man). Will's ISWIM posts were a lot
simpler.

> I'm attempting to put together a proof that E is not a
> well-defined function. It is a complicated proof and it may
> take some time.
>
> It sounds like nonsense, and I advise you to quit now. My guess
> is that you're just looking at my code & thinking of ways it's
> not DS.

No, actually, I'm constructing an expression for which E cannot
logically assign a value (thus E will either be non-total,
non-well-defined, or a non-function).

If you mean you're going to find an expression that puts my code into
an infinite loop, that's nonsense. It says nothing about my
mathematically defined map E.

That's not particularly difficult, but the construction involves
creating an isomorphism for E in the domain of ISWIM.

I don't even know what that means.

As ISWIM is rather primitive, a straightforward construction would
be huge. It is unlikely that you would be willing to follow it.

I have to think you're going to do something that has nothing to do
with my mathematical definition of E at all, like before when you
"proved" that I needed Scott models.

My effort has been in seeing if I can reduce the proof to something
much smaller.

>
> Exactly my point. Why is something being printed?
>
> Only because you asked me to do it!!! My semantic function can't
> handle printing. That is, my map = math-function
>
> E: Exp ---> Value_bottom
>
> cannot have display as a primitive 1-ary function.

This casts doubt on all the other primitive functions as well. I
assert that when presented with a primitive application, you are
not determining the `semantics', but rather just executing the
primitive.

But we're not using the word `semantics' anymore. We're just talking
about well defined maps, and that's a matter of set theory. Execute
is not a word in set theory, so we won't use it.

> I think I'd need continuations to handle display. But you asked
> me to make the change, and I did, because it was a good
> programming exercise.

Feel free to add what you think you need.

No! We started with the most primitive Scheme-like language we could
find! You were the one who found it! I'm still grateful to you for
it! I'm not throwing in continuations yet! That's why I'm staying
away from primitives like display, which in fact are not in ISWIM!

Bill Richter

2004-08-11, 4:01 am

Shriram Krishnamurthi <sk@cs.brown.edu> responded to me:

> It's like if you got me to add the print statement
>
> (print "1 = 0")
>
> And you said, "That's a contradiction! You proved that 1 = 0!"

This analogy is nonsensical at so many levels I won't even begin to
address them, for fear you will use that as a distraction from the
knot Joe very elegantly tied.

You're just wrong, Shriram. You shouldn't expect to be able to
"referee" a discussion without actually understanding what folks are
saying. If Joe wanted to know if I could add display to F-F's ISWIM
language, then the answer is no. There's no elegant knot.

BTW I'm a little sore at you for not responding to my correction of
your earlier post, which showed you weren't following the discussion:

> It makes no sense to ask: "What's *the* definition of this
> function?". You can only ask, "What's *a* definition of this
> function?" One Function may have a variety of definitions.

Welcome to computer science. You keep insisting that functions
are maps. That's what a function is in math. That's not what
it is in computer science. If you prefer, we can use the term
"procedure" instead for the CS version, to keep this distinction
straight.

Perhaps my reply was too obscure. I'll try again: We're having a DS
discussion, as compositionality is a DS word. In DS, function = map.
Schmidt's book uses the convention function = map exclusively.

> Exactly my point. Why is something being printed?
>
> Only because you asked me to do it!!! My semantic function can't
> handle printing.

Rubbish. For a w

you went on about how simple it would be to
handle printing.

I'm sure you're confusing this with something else. The display
discussion took 2 days, and it started with Joe posting

I want you to add the following primitive procedure to your
language: (DISPLAY <expression> )

At first I said I couldn't do it, because it was too hard, and then I
realized it would be trivial, and I did it the next day. So it was a
nice coding exercise that Joe gave me. I'm grateful, because I hadn't
realized how abstract my code was.

Your complaint was *never* about the fact that it was inconsistent
with the semantics or other argument at that level: it was about
your lack of experience as a Schemer.

See, you're confusing 2 arguments. It took me a long time to write my
550 line ISWIM->Scheme interpreter. As you say, I lack experience as
a Schemer, and I'd never written an interpreter of any sort. I'm
grateful to you & Joe for insisting I do the exercise. I feel I
learned a lot about it, e.g. something about the power of HtDP structs.

But what I posted was an interpreter for F-F's ISWIM language, which
does not contain display. Partly because you'd need continuations.

It was evident all along that you didn't see where Joe was leading
you,

Right, I I had no idea Joe thought I was changing the ISWIM language.

as witnessed by your confusion suggesting Joe add printing
statements to monitor the interpreter itself. When you figured out
the code, you happily posted it. Now you cannot retract it.

It's nice code! Joe's a better schemer than I. What's to retract? I
didn't change the ISWIM language to include display, I hacked my code.

> cannot have display as a primitive 1-ary function. I think I'd
> need continuations to handle display. But you asked me to make
> the change, and I did, because it was a good programming
> exercise.

1. So what's on the Web no longer captures your semantics?

Right.

This violates your own promise.

No, I promised to write the code, for Joe, and he asked me to change
it, so I did.

You should have refused to add it.

Perhaps, but you maybe you overestimate my programming skill. For
me, that was a very valuable exercise. Thanks again, Joe. I'll
take it out now if you like.

You knew darn well that you were implementing your semantics,

I did not!!! I would've refused, had Joe asked me to change the ISWIM
language.

not writing random code.

It's not random if Joe asks, it's for him! I thought he was honestly
having trouble seeing how my code worked, and wanted some print
statements. So I told him to do it himself, but then I realized how
easy it would be, and leaped at the chance.

2. The "continuations" (whatever magical properties they possess to
help you out here)

I think you need continuations to handle error messages & display.
You'd know better than I would. But it's a non-issue, because display
is definitely not part of my ISWIM language.

wouldn't address Joe's core concern, at least not in any way that I
can see.

Do you have any idea what Joe's core concern is? Every objection he's
made so far sounds like rubbish to me, especially his last "proof"
that my sem function E_1 isn't well-defined:

Since we intend the domain to include higher order functions, we
need D: D->D.

That was just nonsense. I clearly well-defined my map = math-function

E: LC_vExp ---> Value_bottom

E is just a minor modification of F-F's partial function |--->>_v, and
then I clearly have well-defined my
what-everyone-except-Joe-lets-me-call-a semantic function

E_1: Exp ---> Value_bottom

by modding out by alpha, and composing with E. It's completely
blitheringly obvious that E & E_1 are well defined maps =
math-functions, and instead of looking at my Math, Joe decides what I
ought to be doing instead with Scott models.

I don't just mean to pick on Joe, he's just the calmest & sanest of
you guys, and he's stuck with the thread the longest. He blew up at
me for the first time yesterday, and we've already made up. He's just
holding the bag. Nobody else, including you, seems to be able to
understand my obvious proof that E & E_1 are well-defined maps.

Sponsored Links