Re: [Caml-list] Weird behavior with nan's and min/max

[Hendrik Tews <tews@tcs.inf.tu-dresden.de>]

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