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.