Open rospoly opened 3 years ago
FPTaylor always assumes that errors are symmetric, i.e., if X
is real then Round(X) in [X - e, X + e]
. This estimate can be improved because errors are monotone: a <= b
implies Round(a) <= Round(b)
. So in your case it can be proved that X <= 1
implies Round(X) <= Round(1) = 1
. I have been thinking about implementing monotonicity error reasoning in FPTaylor for some time already. It should be not difficult to do in simple cases: It is enough to track interval bounds of the rounded subexpressions and intersect Taylor forms with these bounds. This simple approach may not work very well in general but it should be sufficient for simple examples. Unfortunately, it will be not enough to deal with your example. The derivatives of arcsine are not defined when X = +-1. It will be necessary to replace the standard Taylor approximation with a special function which has different branches for cases when X is close to -1 or 1.
I am leaving this issue open until I try some experiments with monotonicity in FPTaylor.
I have been playing with the arcsine operator in FPTaylor. FPTaylor does not like when the argument of arcsine is a fresh variable bounded in [-1, 1].
Program causing the error:
I suspect the reason is X=[-1, 1] implies Round(X)=[-1-err, +1+err] thus the domain of the arcsine is violated thus the error message: Potential exception detected: Arcsine of an invalid argument at: asin(rnd64(angle)). On the other hand, this is a very specific scenario where also Round(X) is bounded between [-1 ,1]. So the error might be because of the over-approx. introduced by FPTaylor.
--Rocco