[racket] arity of + versus <=

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