How would I use Supposition.jl on computer arithmetic corner cases?

This is an interesting question, thank you for bringing it up! I think the most relevant section of the docs here is Alignment of Documentation · Supposition.jl Documentation, since it talks about these kinds of issues a bit in the context of floating point values in particular. Documenting these kinds of behaviors is IMO the best course of action.

Unlike with the precision of sincosd, I don’t think there’s any guarantee about the precision of the basic sincosd relative to cosd and how it should behave when shifting the phase of the input by 90°. So whether this inexactness is considered “broken” or not is really not that easy to answer! What I would do is basically the same as what @jar1 suggested - use isapprox with an absolute tolerance and check that the output is always within that tolerance. For a single operation like sind on a Float64, this is typically 1 ULP, and the result is compared to sind on a BigFloat. For your example though, you’d still have to compare the Float64 results of sind & cosd with isapprox.

Note also that it’s going to be extremely difficult to guarantee a large number of trigonometric identities to hold, even within some chosen precision. See e.g. this floating point favorite of mine for an example where it’s hard.


All that being said - your intuition of using error plots as a guiding principle is spot on! In this example, I’d try to plot the error over the range you’re interested in and just take a look at how bad it really is. Since this is about trigonometry, I’d forego the *d versions and use sin/cos directly, producing a plot of all Float16 numbers in [0, 1].

Maybe the overall error is already acceptable, maybe the worst case is MUCH worse than the example Supposition.jl found. Remember, it tries to find the minimal input that produces the same test result, which may not necessarily be the minimal error that you’re actually interested in! You could try to find that with target!(abs(sind(x+90) - cosd(x))) (see this doc section), which looks like it could be simple enough to work out.

2 Likes