Can we go meta? Do we dare dream that we can find, in the ways persuasion was achieved on this topic, some general principles about the (idealized) design of scheme? We're fast and loose about how nullary and unary < makes sense based on the usual way of defining things in math -- does anyone dare try to generalize the modus of reasoning around that?
Also, and I think we are sloppy on this point: What is (< 'x) and why? -t -----Original Message----- From: "Keith Wright" <[EMAIL PROTECTED]> Sent: Tuesday, October 28, 2008 12:52am To: [email protected] Subject: Re: [r6rs-discuss] Comparison procedures' number of arguments For what it's worth, I will post exactly one comment to this amazingly long discussion. > From: "Marcin 'Qrczak' Kowalczyk" <[EMAIL PROTECTED]> > > A sequence is increasing if, for every i, j from the > range of its indices such that i<j, a[i]<a[j]. This > is true for any sequence of length 0 or 1. This > condition is equivalent to: there exist no numbers i, > j from the range of its indices such that i<j and > a[i]>=a[j]. This is obviously true. I find this argument totally convincing. I was not sure at first, because I could not see how to write a recursive definition with a null base case, (as opposed to a special case). Maybe I was slow because the algorithm based upon this general definition is O(n^2). Any sane programmer will make zero and one into special cases and then use transitivity to prove a theorem like if (length S) >= 2 then S is monotone increasing iff (car S) < (cadr S) and (cdr S) is monotone increasing to make a linear algorithm. But these special cases are for efficiency, not correctness. ;;; Definition of multi-argument monotonicity ;;; in terms of binary comparison. For any ;;; comparison <?>. Sequence S is monotone <?> ;;; iff for all i,j if i<j then S[i] <?> S[j] ;;; The base cases are naturally all true. (define ((mono <?>) . ls) (or (null? ls) (and (let ((a (car ls))) (let acmp ((others (cdr ls))) (or (null? others) (and (<?> a (car others)) (acmp (cdr others)) )))) (apply (mono <?>) (cdr ls)) ))) ((mono <) 2 3 5 7) ==> #t ((mono <) 2 7 5 3) ==> #f ((mono <)) ==> #t Q.E.Damnit -- Keith PS: This isn't really relevant, but: > From: Jed Davis <[EMAIL PROTECTED]> > > On Mon, Oct 20, 2008 at 06:14:47PM -0400, John Cowan wrote: > > > > ObDigression: This is only true on the assumption of unrestricted > > quantification, which translates "All witches are green" as (Ax)(Wx->Gx). > > > > Restricted quantification, however, is (AWx)(Gx), and is *false* if > > there are no witches, just as "Each rhinoceros in my workplace is painted > > purple" is false. There are no such rhinocerotes, and so the claim fails. > > Ah, but the corresponding item using the typed quantification of the > Calculus of Inductive Constructions, or presumably any other flavor of > intuitionistic type theory, is *true* -- to prove something of the form > "forall x : Witch, ...", one can begin with "lambda x : Witch, ...", > and then apply the "there are no witches" axiom (which has type "Witch > -> False") to this alleged witch "x" and obtain a proof of false, from > which anything (including the greenness of that witch) can be derived; > /ex falso quodlibet/ is just a special case of structural induction. I, too, find the claim that restricted quantification gives a different answer dubious without a reference (off list please). Aristotle took vacuous quantification to be false, but I don't recall any modern author that uses that conventions, except for one, whose details I forgot decades ago, who was trying to make a formal system specifically to reproduce the claims of De Interpretatione and the Prior Analytics. The result was messy, and good for nothing much except explaining to a modern logician what Aristotle thought. In particular, Lambek and Scott, Introduction to Higher Order Logic, a book on logic with possibly empty types, say (p 131): "Had we not insisted on <technical device> we would have been able to infer from the fact that all unicorns have horns that some unicorns have horns." So they take the former as true, and the latter as false. It would torque up the semantics to have it otherwise, and they are willing to somewhat complicate the syntax to avoid an invalid inference. I have an unreasonably large collection of books on this subject, and do not think any of them would deny that all unicorns have horns. PPS: I have a friend who says she is a witch. She isn't green. _______________________________________________ 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
