Alan Bawden wrote:
> That `null?' check in the preamble looks pretty arbitrary now. It doesn't
> have anything to do with the base case of the recursion. The base case
> occurs when the list has length one, not zero. The decision to return #T
> for zero arguments, if it is the correct one, must be driven by some other
> concern. (Like some nice mathematical identity.)
>
It's not an "identity". It's that in your induction rules if you
allow the 0 and 1 cases it's very simple. If you disallow either
or both your inductions will ultimately be much the same but
you'll needlessly carry around a lot of baggage that restrict
you to cases where sequence predicates constructed from binary
relations are never applied to 0 or 1 arguments. You'll have a
lot more tedious, trivial proof burden and exceptional case stating
and exceptional case resolving to do for no gain at all beyond it
being hard to explain to a teen armed with typical HS math why
the 0 and 1 cases ought to be defined. ("Induction? What's that?"
is what I'm imagining.)
> Now there might be some other way to write this code so that having the
> zero argument case return #T really is the base case, but I don't see how
> to do it.
>
> I think I've said the same thing in three different ways now...
>
Yes, you seem to me to be talking about one of the many artifacts that
English syntax casts as a confusing shadow on logic but then arguing
that because the shadow is confusing we should take the side of English
syntax. And this in spite of overwhelming evidence that just about anyone
who studies math doesn't have any troubles from that shadow once they
recognize it for the arbitrary nothing it is. The ordinary english senses
of some words is confusing you vis a vis the ordinary math english senses.
(It seems to me, IMHO, I doff my cap, I mean no disrespect -- really.)
-t
> _______________________________________________
> r6rs-discuss mailing list
> [email protected]
> http://lists.r6rs.org/cgi-bin/mailman/listinfo/r6rs-discuss
>
>
_______________________________________________
r6rs-discuss mailing list
[email protected]
http://lists.r6rs.org/cgi-bin/mailman/listinfo/r6rs-discuss
