Open AKEOPLUS-boris-bocquet opened 12 months ago
Even trying without the implementation of my norms, I got similar weird results :
8 ?- {N1 == 0.6065, A == 0.5, N2== 0.3678, AN2 == A * N2}.
N1:: 0.606500000000000...,
A:: 0.500000000000000...,
N2:: 0.367800000000000...,
AN2:: 0.183900000000000... .
9 ?- {N1 == 0.6065, A == 0.5, N2== 0.3678, AN2 == A * N2}, {N1 <> AN2}.
false.
10 ?- {N1 == 0.6065, A == 0.5, N2== 0.3678, AN2 == A * N2}, {N1 =\= AN2}.
false.
11 ?- {N1 == 0.6065, A == 0.5, N2== 0.3678, AN2 == A * N2}, {N1 == AN2}.
false.
Queries 9 and 10 are wrong.
<>
and =\=
are only supported for integers, the reason being that these operations are unsound over reals. The set of reals is continuous so X <> Y
can't be finitely expressed. Of course you can express <>
over finite domains like integers and floats. In clpBNR using <>
automatically constrains the values to be integers:
?- {N1 <> N2}.
N1::integer(-1.0Inf, 1.0Inf),
N2::integer(-1.0Inf, 1.0Inf).
<
and >
have a similar issue (unsound over reals), but the restriction is relaxed in clpBNR. In these cases X<Y
means the upper bound of X is less than the lower bound of Y by 1 floating point value which can be useful for some branch-and-bound search algorithms
In these cases X<Y means the upper bound of X is less than the lower bound of Y by 1 floating point value which can be useful for some branch-and-bound search algorithms
Sorry, I meant "at least 1 floating point value".
SWI-Prolog (threaded, 64 bits, version 9.1.10) % *** clpBNR v0.11.1 ***.
Dear Rick, a friend told gave me this small problem to implement : can prolog check if a given function is a "norm" or not. To be a norm, the function has to respect a couple of properties. The only one I started to implement is
norm(a*X) = a * norm(X)
. I know that Prolog is not the best language for theorem / math proving. Still, I though this could help him to find quickly counter-examples.Saddly, I could not succeed. It looks like the not equal always fail.
Here is the code :
norm1
is a function that respect the property. WhereasnormNok
does not. I can switch the norm to be tested by commenting / uncommenting the lines withmy_norm_under_test
.When I test
norm1
, I have these outputs for these queries :It looks OK for me.
Now I switch to
normNok
and here are the results I got from the queries :Query number 5 fails. Which is fine because
N1 <> A*N2
, so I cannot meet the constrainN1 == A*N2
.So if query 5 fails, why query 6 also fails ?? Even in the console output, the intervals of N1 and A*N2 are really far away, so I cannot see why not equal fails.
I tried other NOK norms (e.g. log and cos). Similar behaviour. I tried to restrains reals to be within -1e3, 1e3 : same behaviour.
Can you help ? This is not an urgent matter at all. Thanks in advance