On 10/28/2011 12:00 PM, Stephen Bloch wrote:
On Oct 28, 2011, at 1:57 PM, Jay McCarthy wrote:
I would expect
(not (and (apply< x) (apply> x)))
to be true for all x
That's not at all obvious to me. That's like saying you expect
(not (and (all-even? x) (all-odd? x)))
to be true for all sets x. It breaks down in the empty case.
Exactly.
The only thing we haven't done in this discussion (and I haven't seen it
in the discussion Eli linked to, either) is define the various proposals
in symbolic logic. We keep appealing to it already, but mostly informally.
Proposal 1. No restrictions. Because '<' checks monotonicity for two or
more arguments, it's already equivalent to the more general
(< xs ...) <->
forall x_i in xs, forall x_j in xs, j > i -> (less? x_i x_j)
where 'less?' is the primitive less-than relation. This is vacuously
true in the empty case and trivially true in the singleton case. It's
mathematically elegant. It's easy to reason about because there's only
one rule, which has no alternating quantifiers and no special cases for
any length. (It's well-defined for empty, singleton, and all finite
lists - and even countably and *uncountably* infinite lists! Woo!)
Stephen's recursive function gives an equivalent inductive definition:
(<) <-> #t
(< x) <-> #t
(< x_1 x_2 xs ...) <-> (less? x_1 x_2) and (< x_2 xs ...)
Given the third rule, the second has to be "(< x) <-> #t". (Otherwise,
(< 1 2) could be false.) The first rule seems arbitrary because "(<)"
isn't really a base case. It could arguably be "(<) <-> #f".
Proposal 2. Different zero-argument case:
(<) <-> #f
(< x) <-> #t
(< x_1 x_2 xs ...) <-> (less? x_1 x_2) and (< x_2 xs ...)
Putting it a different way makes it obvious that "(<) <-> #f" is an ugly
special case in a pretty inductive disguise:
(< xs ...) <->
not (empty? xs) and
forall x_i in xs, forall x_j in xs, j > i -> (less? x_i x_j)
I don't think anybody is arguing for this. I'm heading off arguments
against Proposal 1, which use Proposal 2 to try to show that allowing
zero arguments is inherently ambiguous. It's not.
Proposal 3. Manage the apparent ambiguity by not allowing it:
(< x) <-> #t
(< x_1 x_2 xs ...) <-> (less? x_1 x_2) and (< x_2 xs ...)
Because this would be motivated by seriously considering Proposal 2, I
see it as invalid. IOW, the decision should be between Proposal 1 and
Proposal 4 only.
Proposal 4. The current behavior:
(< x_1 x_2) <-> (less? x_1 x_2)
(< x_1 x_2 x_3 xs ...) <-> (< x_1 x_2) and (< x_2 x_3 xs ...)
Yes, that's right: allowing one or more arguments makes no sense. It
should be either zero or more, or two or more. But two or more only
because that's the status quo. Check out the quantifier version:
(< xs ...) <->
not (empty? xs) and
not (empty? (rest? xs)) and
forall x_i in xs, forall x_j in xs, j > i -> (less? x_i x_j)
There are worse ones with existential quantifiers, or left-hand sides
like (< x_1 x_2 xs ...) that require consing on the right-hand side.
So I would like to see '<' (and friends) defined using the elegant
quantifier rule in Proposal 1, but (of course) implemented recursively.
Neil T
_________________________________________________
For list-related administrative tasks:
http://lists.racket-lang.org/listinfo/users
