Version française
Home     About     Download     Resources     Contact us    

This site is updated infrequently. For up-to-date information, please visit the new OCaml website at

Browse thread
[Caml-list] Weird behavior with nan's and min/max
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: 2003-10-16 (17:29)
From: Hendrik Tews <tews@t...>
Subject: Re: [Caml-list] Weird behavior with nan's and min/max
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.)


Hendrik Tews

To unsubscribe, mail Archives:
Bug reports: FAQ:
Beginner's list: