Ken Dickey wrote:
Comparison is taught in kindergarden. Comparison is fundamental.
And in algebra. Things I didn't see taught in high school
were definitions for relation, transitive relation, reflexive
relation, symmetric relation, partial order, total order,
and equivalence along with proof techniques that use those
definitions.
In 40 years of software development I have never seen a sequence outside the
classroom. I write code which compares quantities all the time.
Surely you do see and use sequences (and their properties)
all the time. It's probably just automatic and stays in the
back of your mind rather than something you explicitly
think about. For example, you know that if you raise a total
ordering of characters to a lexical ordering of strings that the
resulting lexical order is a total order.
Given multiple models, isn't it more natural to define something more abstract
(e.g. num-seq, see below) which models the properties you want rather than
trying to overgeneralize comparison predicates?
Well, remember, you earlier convinced me that (it is at least
one reasonable approach) to have all of the numeric relation
predicates be binary -- arity 2. So, (< 1) is an error
and so is (< 1 2 3).
I think that does raise the question of how one can
write a generic "sequence-pairwise?" rather than
having to use "numeric-sequence-pairwise?" but that's
a whole separate question.
If, though, you want (< 1 2 3 4 5) to not be an error
I have trouble with your disallowing (<) and (< 1).
On Monday 20 October 2008 13:24:35 Bradley Lucier wrote:
In mathematics, statements about the (nonexistent) elements of the
empty set are taken to be true; such statements are called "vacuously
true".
[I guess you could label proofs which use such properties "vacuous". ;^]
I find it natural that
0 + x = x
1 * x = 1
(and) => #t
(or) => #f
I find it easy to explain that
(<= low x high)
is a more elegant way to write
((low <= x) && (x <= high))
But
(and (char<? #\z) (=) (string>?)) => #t
(and (< 2) (= 2) (> 2)) => #t
(and (<) (=) (>)) => #t
???
Because
() is monotonically decreasing and
() is monotonically increasing and
() is a desert topping and a floor wax
() is the pope
(2) is monotonically decreasing and
(2) is monotonically increasing
???
Doesn't it make more sense to require existence for comparison?
If I were a good teacher (I don't claim to be) trying
to talk to the guy with high school math who asked
that question I think I would have to honestly answer
that "nobody knows and don't let me stifle your
creativity but..."
And then we could look at how relations are normally
defined: as ordered pairs. For example, in this way of
talking about it, "<" is a name for the class of all pairs
of numbers where the first number is less than the second.
With that definition, I can then easily define a class
like "all numbers < X for a given X".
Suppose we have a list of numbers, (A B C ...)
Using the definition of "<" as ordered pairs I can
easily define the class of "ascending lists of numbers".
We can then ask: "Is the list (A) an ascending list of
numbers?" And that gets to the heart of your question
because the answer depends on how we've defined
"ascending list" in terms of "<". A typical definition
that people normally use might be:
a list X is defined to be an ascending list iff
for all adjacent numbers in the list X_n and X_n+1
X_n < X_n+1
Your definition would be something like:
a list X is defined to be an ascending list iff
for all adjacent numbers in the list X_n and X_n+1
X_n < X_n+1
AND
X contains at least two numbers
Interestingly, your definition leads to some "intuitive
sounding" results. For example:
Ken's definition => "all finite ascending lists contain a maximum
element"
Std definition => "ascending lists are either empty or contain a maximum"
On the other hand, the std definition leads to some "intuitive
sounding" results. For example:
Std definition => "a singleton or empty list is well ordered"
Ken's definition => "a singleton or empty list is neither well
ordered or not ordered"
You'll probably wind up, for convenience during proofs,
creating a definition for (in effect) "empty-singleton-or-ascending?"
(which definition will be the standard definition of ascending in the
first place). Indeed, you did at the end of your message.
I (using the std definition) will wind up, for convenience during
proofs, create a definition for (in effect) "non-empty lists".
So the two definitions are part of a larger cluster of definitions
that are duals. All the interesting proofs in your system correspond
exactly to
proofs in mine (but using definitions like "non-empty lists" in
mine). And vice versa (but using definitions like
"empty-singleton-or-ascending?" in yours).
In Scheme, making the relation operators strictly binary
would be the agnostic point of view that went the farthest
in two directions:
1st: It would be the Scheme definition that most closely
paralleled the standard definitions of these relations as used
in math -- Scheme's < and the < in your favorite formalization
of numbers would be closely related. Look up some math
on the web and you'll happily discover stuff that directly
applies to Scheme's strictly binary <.
2nd: It would require programs to explicitly state what they
mean when asking "is this list well ordered?" while making
it easy to answer with Ken's definition or a more "standard"
definition, etc.
(define (monotonic? ordered? sequence)
(let ( [list-of-pairs (pairs-in sequence)] )
(if (null? list-of-pairs)
#f
(for-all
(lambda (pair) (ordered? (car pair) (cdr pair)))
list-of-pairs))
) )
Can't we just use comparison predicates to compare quantities?
A set of binary predicates makes sense to me.
The way the word is usually used, the consequent of the conditional
should return #t. (You're defining "monotic-and-two-or-more?")
E.g., look for math definitions of "monotonic" on the web.
However, return #t would be incorrect in the case of a singleton
sequence whose sole element is of the wrong type for the
ordered? predicate. Again, that seems to me to be the hard and interesting
problem to fix.
Is there really a natural, universal, fundamental extension here that needs to
be in the language?
I'd prefer a type check in the single-elt case of your library
code and would prefer definition in terms of a primitive binary <
but, yes:
Having an arbitrary arity predicate that returns #t iff
it's arguments (if any) are in order seems like a basic
thing.
As it stands now the primitive < tests if a sequence
of length 2 or greater is well ordered which is a bit
exotic and tends to not come up often in math.
Scheme's current < is not quite a relation and is
a defective raising of < to a pairwise sequence operator.
While I have been arguing for strictly binary <,
I could also see one where (<), (< 1), and (< 1 2 3)
are all #t. It is easy enough to then define, say,
"<R" ("less-than-relation") which is exactly arity two.
-t
Cheers,
-KenD
;;====================
#!r6rs
(library (theory A num-seq)
(export num-seq? num-seq<) ;;; ...
(import (rnrs))
(define (num-seq? list-of-numbers)
(for-all number? list-of-numbers))
(define num-seq<
(case-lambda
[() #t]
[(single-elt) #t]
[(elt1 elt2) (< elt1 elt2)]
[list-of-numbers
(apply < list-of-numbers)]
) )
_______________________________________________
r6rs-discuss mailing list
[email protected]
http://lists.r6rs.org/cgi-bin/mailman/listinfo/r6rs-discuss
