Re: ISSUE-126 (Revisit Datatypes): A new proposal for the real <-> float <-> double conundrum

On 4 Jul 2008, at 15:18, Boris Motik wrote:
[snip]
> This ontology is unsatisfiable: the range of a:prop contains only  
> one object, but (4) requires existence of two different objects.
> The difficulty in detecting this is that you need to count how many  
> numbers are there between n1 and n2. How are you going to do
> that? The binary representation of floats is really cumbersome to  
> deal with.
[snip]

I finally found a reasonable reference:

	http://www.cygnus-software.com/papers/comparingfloats/ 
comparingfloats.htm

"""The IEEE float and double formats were designed so that the  
numbers are “lexicographically ordered”, which – in the words of IEEE  
architect William Kahan means “if two floating-point numbers in the  
same format are ordered ( say x < y ), then they are ordered the same  
way when their bits are reinterpreted as Sign-Magnitude integers.”

This means that if we take two floats in memory, interpret their bit  
pattern as integers, and compare them, we can tell which is larger,  
without doing a floating point comparison....

Because the floats are lexicographically ordered that means that if  
we increment the representation of a float as an integer then we move  
to the next float....

We can apply this logic in reverse also. If we subtract the integer  
representations of two floats then that will tell us how close they  
are. If the difference is zero, they are identical. If the difference  
is one, they are adjacent floats. In general, if the difference is n  
then there are n-1 floats between them. """

So you can map them to integers for counting purposes pretty easily.

Cheers,
Bijan.

Received on Friday, 4 July 2008 15:05:40 UTC