I just read up on interval arithmetic. I understand its desirable properties. Where in practice have you applied it? What’s a real world application for interval arithmetic?

▲ ngruhn 6 hours ago | parent | next [-]

It can be used in static analysis or type checking. E.g.

    if (x >= 0) {
      x += 10
      if (x =< 9) {
        // unreachable 
      }
    }

By maintaining an interval of possible values of x, you can detect the unreachable branch, because the interval becomes empty:

    initial: [-oo, oo]
    x >= 0 : [0, oo]
    x += 10: [10, oo]
    x =< 9 : [10, 9] (empty)

	▲	Oberdiah 4 hours ago \| parent \| next [-]
		I’m working on a static analyser at the moment that does this, and the inferences that can be made just from the information of intervals is quite impressive. One thing you run into pretty quickly though in a lot of languages is integer overflow ruining your day - in your example above the commented section is reachable for signed ints that support overflow and that adds a whole other layer of complexity to things.
	▲	thekoma 4 hours ago \| parent \| prev [-]
		We recently implemented this idea in an LLVM optimisation pass based on value-range information from sensor datasheets [1]. [1]: https://dl.acm.org/doi/pdf/10.1145/3640537.3641576

▲ nickcw 5 hours ago | parent | prev | next [-]

In physics, whenever you make a measurement it has a precision. Usually you represent this as a normal distribution, but for calculations it can be easier to represent this as an interval.

The police measure the distance my car travelled [ 99.9, 100.1 ] m and the time it took [ 3.3, 3.4 ] s - how fast was my car going? [29.38, 30.33] m/s according to the interval calculator.

Physics students learn exactly this method before they move on to more sophisticated analysis with error distributions.

	▲	ttoinou 4 hours ago \| parent [-]
		And one might want to approximate error distribution calculus with a method that will look like the one here

▲ nicolodev 6 hours ago | parent | prev [-]

It’s astonishing how nobody hasn’t mentioned abstract interpretation yet. Under classical static analysis, if you can “prove” that a variable does not have values in some unsound zones, you can e.g. “prove” soundness or apply further optimizations.

The interval abstract domain works under interval analysis with an algebra that’s the same of this calculator. It’s funny to implement something like that on source/binary level :)