The bounded real (breal) data type

Involved: Joachim, Warwick

What is it?

A new type of number in Eclipse: a representation of a real as a pair of floating point bounds. While a float conceptually stands for a real that is somewhere in the vicinity of the float, a breal stands for a real that is somewhere between the given bounds. To keep terminology precise, we decided on the name bounded real rather than interval or ground interval - the latter would have invited confusion with interval variables.

Features

Predicates

breal/1 type test
breal/2 conversion to breal
breal_min/2, breal_max/2, breal_bounds/3 get the bounds as a float

Syntax

two floats separated by two underscores, e.g. 3.0999999999999996__3.1000000000000005

Trick to convert all float constants into breals:

?- local macro(type(float),breal/2,[]).
Yes (0.00s cpu)

?- X = 3.4.
X = 3.3999999999999995__3.4000000000000004
Yes (0.00s cpu)

Problems

There are a number of rather fundamental problems associated to the idea of having reals in a programming language. No programming language can have exact representations for all reals - they are uncountable. Any one program can only deal with a countable subset of them.

Since there are uncountably many reals but only countably many names/representations, an infinite number of reals share the same representation.

Some of the usual generic Prolog properties are violated:

equality (and unifiability) is not decidable even if the breals look the same:

?- breal(3.1,X), breal(3.1,Y), X==Y.
exiting to an undefined tag in exit_block('undecidable comparison of bounded reals')

?- breal(3.1,X), Y is sin(X), Z is sin(X), Y==Z.  
exiting to an undefined tag in exit_block('undecidable comparison of bounded reals')

except in special cases:

[eclipse 2]: breal(3.1,X), X==X.
X = 3.0999999999999996__3.1000000000000005
Yes (0.00s cpu)

the rule that you can writeq a term, read it back, and it will be identical to the written one does not hold (because there is no unique finite representation for every individual real - we would need a universal dictionary of all reals ever written)
same holds for storing breals elsewhere:

?- breal(3.1,X), findall(Y, Y=X, [X]).
exiting to an undefined tag in exit_block('undecidable comparison of bounded reals')

the arithmetic comparisons leave a delayed goal:

?-  breal(3.1,X), breal(3.1,Y), X=:=Y.

X = 3.0999999999999996__3.1000000000000005
Y = 3.0999999999999996__3.1000000000000005


Delayed goals:
        3.0999999999999996__3.1000000000000005 =:= 3.0999999999999996__3.1000000000000005

So why do all these problems not occur with floats? They do, of course, they are just fudged.