I use interval arithmetic for reliable computing. Now, a procedure coded in a good implementation of interval arithmetic takes perhaps about eight times as much as the same procedure carried out without interval arithmetic (if the lion's share of runtime is taken by floating-point computations). I have sometimes been asked why I don't do rounding-error analysis by hand instead. To me, that does not look like a good option: it amounts to saving computer time at the expense of human time, and creates one more occasion for human error.

Now, what would make sense for me would be for there to be a system for bounding rounding errors with the help of a computer. It might not be realistic to expect a computer to analyse the total error in fairly complex procedures, but a human and a computer might be able to do a quicker and more reliable job than a human working alone, and produce a certificate of correctness to boot. Cf. how it is much easier to produce a formal proof with computer assistance.

(In particular: I would be interested in how error analysis in the sense of e.g. Wilkinson could be used in the context of a rigorous proof. I could see how it might be possible to implement it by means of a system for the computer-aided production of formal proofs. Has such a thing been done in practice?)

Note: perhaps it shows, but -- I am a pure mathematician; feel free to tell me if what I say seems a little naïve.

  • 3
    $\begingroup$ Interval arithmetic is a method for bounding rounding errors with the help of a computer. Are you asking for something different? $\endgroup$ – Federico Poloni Aug 26 '18 at 17:02
  • 1
    $\begingroup$ There are plenty of automated systems that ensure that certain computations and their floating point errors are bounded and safe. Many of them these days use semidefinite optimization to write down an optimization problem for the worst case. Search the literature for some papers on this! $\endgroup$ – Wolfgang Bangerth Aug 26 '18 at 21:23
  • 1
    $\begingroup$ Federico Poloni: yes, but it is a posteriori method; each time a computation is carried out, the maximal error is, if you wish, computed afresh, with a substantial overhead. The alternative is to estimate what the maximal error in the output of an operation can be, given a relative error size in the input. Say we have a loop running 10^9 times. We should be able to bound the maximal error in the final output of the loop without having to compute intervals or error bounds 10^9 times. $\endgroup$ – H A Helfgott Aug 27 '18 at 3:40
  • $\begingroup$ Wolfgang Bangerth: any references to the literature would be very welcome; as I should have said, I work in number theory, and this area is relatively unfamiliar to me. Just to be clear - I know (or think I know) that what e.g. matrix multiplication does to errors is well-understood. Are there systems that - presumably with some human help - can bound the error the result from iterating a loop 10^9 times, say, without having to go through the loop 10^9 times and seeing how the error changes with every operation? $\endgroup$ – H A Helfgott Aug 27 '18 at 4:16
  • 1
    $\begingroup$ I suggest that you use a @ before name when replying, that way the person will receive a notification. $\endgroup$ – nicoguaro Aug 27 '18 at 13:20

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.