Ken Dickey wrote:
> I accept that there is a well defined base case (identity) for * and + .
>
> I find it wacky but perhaps useful that (gcd) ==> 0 .
>
> I accept that returning #t for relational tests on zero and one argument
> cases
> operationally may make some code more compact.
>
> I don't see how it helps me reason.
>
> I fail to see a model or proof that would sensible be helped by having the
> unrelated empty sequence or sequence of one element compare <, >, and = .
>
Is this a valid program transformation? Should it not be?:
(apply = (append x y z))
<==>
(let ((x0 x)
(y0 y)
(z0 z))
(let* ((xy (append x0 y0))
(yz (append y0 z0)))
(and (apply = xy)
(apply = yz))))
All of the math texts I've seen define a relation either as
a class or set of ordered pairs or as a class or set of
k-tuples, k >= 0, with k fixed for the relation.
When we start talking about partial orders it's common
to define sequences (aka families or lists) and a generic,
inductive way to convert any binary relation to a pair-wise
relation on a sequence. These definitions always handle
the empty and singleton sequence cases because otherwise
the inductions are far more awkward (as the above proposed
transformation rule illustrates). I've never heard
of any suggestion that the empty-sequence or singleton-sequence
cases be otherwise defined.
> It seems somehow too close to "assume black is white, not prove you are the
> pope" kind of logic.
>
It doesn't take any new axioms so there is no danger of
creating an inconsistent system. It just simplifies induction
rules.
> Is (and (< -inf.0) (> +inf.0)) => t#
> really helpful to clarity of thought?
>
Let's talk about those separately because that's a different
issue entirely. Scheme has the handling of +/- inf/nan .0
wrong, in my opinion, but it's a different case -- not really analogous.
(I'll express my opinion about those things in a separate message.)
> I am happy to be educated here. I am still looking for a model which makes
> sense to me [and which I can explain to a student who's background is high
> school mathematics].
>
Ugh. High school math tends to be not so very good, afaict.
If they're going to really get into the whys and wherefores of
Scheme a good place to start, probably absent or poorly done, from their
high school curriculum is a review of logic, introduction to set
theory, the concept of a class vs. a set, standard definitions for
relation, partial order, equivalence, mapping, family, list, and lattice.
Ideally by the time you're talking about lists and lattices they should
be doing
inductive proofs that will make it easier to "see and feel" why
when you lift a binary relation to make a pairwise predicate that
applies to sequences it is handy to define the 0-length and singleton
sequence cases in the obvious way.
-t
> Cheers,
> -KenD
>
>
_______________________________________________
r6rs-discuss mailing list
[email protected]
http://lists.r6rs.org/cgi-bin/mailman/listinfo/r6rs-discuss
