From mboxrd@z Thu Jan 1 00:00:00 1970 Received: (from majordomo@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id TAA03874; Thu, 16 Oct 2003 19:29:55 +0200 (MET DST) X-Authentication-Warning: pauillac.inria.fr: majordomo set sender to owner-caml-list@pauillac.inria.fr using -f Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id TAA19443 for ; Thu, 16 Oct 2003 19:29:54 +0200 (MET DST) Received: from tcs.inf.tu-dresden.de (orchid.inf.tu-dresden.de [141.76.75.101]) by nez-perce.inria.fr (8.11.1/8.11.1) with ESMTP id h9GHTr127321 for ; Thu, 16 Oct 2003 19:29:54 +0200 (MET DST) Received: from ithif51 (ithif51 [141.76.75.51]) by tcs.inf.tu-dresden.de (8.12.9/8.12.9) with ESMTP id h9GHTnAT026928 for ; Thu, 16 Oct 2003 19:29:49 +0200 (MET DST) Received: from tews by ithif51 with local (Exim 3.36 #1 (Debian)) id 1AABwb-00075W-00 for ; Thu, 16 Oct 2003 19:29:49 +0200 MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Message-ID: <16270.54668.942746.619730@ithif51.inf.tu-dresden.de> Date: Thu, 16 Oct 2003 19:29:48 +0200 To: caml-list@inria.fr Subject: Re: [Caml-list] Weird behavior with nan's and min/max In-Reply-To: <1066175022.17727.9.camel@pelican> References: <51792.141.155.88.179.1066142234.squirrel@minsky-primus.homeip.net> <54490.141.155.88.179.1066143413.squirrel@minsky-primus.homeip.net> <63219.141.155.88.179.1066164734.squirrel@minsky-primus.homeip.net> <1066175022.17727.9.camel@pelican> X-Mailer: VM 7.16 under Emacs 21.2.1 From: Hendrik Tews X-Scanned-By: MIMEDefang 2.33 (www . roaringpenguin . com / mimedefang) at tcs.inf.tu-dresden.de X-Loop: caml-list@inria.fr X-Spam: no; 0.00; caml-list:01 hendrik:01 tews:01 tews:01 caml-list:01 mathematic:01 logics:01 logics:01 existential:01 definedness:01 predicate:01 recursively:01 higher-order:01 hendrik:01 tu-dresden:01 Sender: owner-caml-list@pauillac.inria.fr Precedence: bulk skaller writes: Subject: Re: [Caml-list] Weird behavior with nan's and min/max The idea that x = x isn't universally true is mathemtically absurd. I don't think it has to do with mathematics. It has to do with logic. While there is only one mathematic, there lots of logics around. Some of those are totally sensible, still they do not let you deduce x = x for all x. The prominent examples are logics that deal with undefined terms and partial functions. In this field a popular approach is to use existential equality: x = y is true iff both are defined and equal. The advantage of this approach is that you don't need an additional definedness predicate and (more importantly) the equality relation is recursively enumerable (if you don't mess things up in the rest of the logic). In this light, I think it might be absurd to have x = x universally true, because sometimes you can't even tell if x = x (because there is no algorithm that can decide it). ;-) (However, most of the time I use higher-order logics in which x = x is always true.) Bye, Hendrik Tews ------------------- To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/ Beginner's list: http://groups.yahoo.com/group/ocaml_beginners