🚀 go-pugleaf

In article <19080@brunix.UUCP>, mj@brunix (Mark Johnson) writes:
> At least one Prolog I know of (BNR Prolog) uses interval arithmetic.
> Couldn't this be used to provide a sound floating-point unification?

First tell us what you _mean_ by "sound floating-point unification".
Then maybe the question can be answered.  I can see one way of integrating
interval arithmetic with unification which makes logical sense:  to
interpret a binding X:[L,U] as a constraint L =< X =< U.  In that case,
unifying X:[Lx,Ux] with Y:[Ly,Uy] should yield X,Y:[max(Lx,Ly),min(Ux,Uy)].
Intervals of floats have all the nice lattice properties that we need to
make unification work.  

There is no difficulty with making floating-point unification sound.
Have two floating-point numbers unify if and only if they are the exact
same bit pattern.  That way you preserve all the properties of equality
which unification otherwise possesses, one of which is that substitution
of equals for equals should result in no detectable change whatsoever.
"Fuzzy" unification torpedoes that completely.