5 ms·

Couldn't the overdetermination problem be solved by tagging intervals with their ids? E.g., "xx" should be resolved as "(x, i[-3, 3])(x, i[-3, 3])" and "i[-3,

Couldn't the overdetermination problem be solved by tagging intervals with their ids? E.g., "x*x" should be resolved as "(x, i[-3, 3])*(x, i[-3, 3])" and "i[-3, 3]*i[-3, 3]" as "(nil, i[-3, 3])*(nil, i[-3, 3])". Since the tag matches in the first expression and not in the second (nil != nil) different rules could be used. Btw this comes up a lot in compiler design for dynamic languages since constraining the value ranges of variables means that you can implement them more efficiently. In static languages it is not as important since the domains of most variables are either given to you or inferred by the type system. Also an interesting head scratcher is how to implement interval arithmetic for modulus: i[3,6] % i[3, 6] = ???*

kragen 2y ago
this is basically how affine arithmetic works. but in interval arithmetic or modal interval arithmetic the representation of a float is two floats, and in affine arithmetic the representation of a float is a potentially unboundedly large set of float coefficients, none of which can be safely ignored, so there are some drawbacks to this approach i'm not sure why wayne doesn't mention affine arithmetic and modal interval arithmetic in this post; i'd think they were relevant
- lifthrasiir 2y ago
  > none of which can be safely ignored Or more accurately speaking, they can be ignored but at some expense of accuracy. (You can always approximate every variable with a (-inf, +inf) interval!) There are several working ways to "compress" affine variables when they get too many. Probably a worse problem with AA is that every multiplication introduces a new variable, so it can be very frequent to head into the maximum number of variables set for the reasonable performance...
  - kragen 2y ago
    agreed. i find reduced affine arithmetic the most appealing, but haven't tried it
moonchild 2y ago
this requires all terms to be represented symbolically, which 'works', but now you need a full-blown symbolic rewrite engine to try to simplify things. very reasonable for an optimiser but not so much for numerics. for numerics a more common approach is interval mincing. we have a function f(x) = x*x, and try to apply f([-3 3]). we can 'mince' the inner interval and say that (e.g.) [-3 3] = [-3 -1] U [-1 1] U [1 3]. so we have f([-3 -1] U [-1 1] U [1 3]); distribute function application over U (which is sound) to get f([-3 -1]) U f([-1 1]) U f([1 3]), which is obviously tighter than f([-3 3]). we picked a subinterval size of 2, but can shrink it arbitrarily until we're satisfied with the result. this technique is essentially a form of case analysis, and can also be applied to optimisers/static analysers (complementarily to simplifying rewrites)
- kragen 2y ago
  affine arithmetic does not need a full-blown symbolic rewrite engine, though it too sometimes produces overbroad intervals
  - moonchild 2y ago
    so a middle ground (as many pseudo-symbolic approaches). glanced at wikipedia—this seems not dissimilar conceptually to the abstract domain of polyhedra, in that it's symbolic but has a flat structure and expresses only linear relationships. of course, polyhedra are exponential where affine arithmetic is quadratic (overall space in number of terms), and polyhedra are global where affine is local (therefore easier to implement as a library, but no sharing). more missed connections between numerical analysis and program analysis? (meh but no sharing probably means affine generally loses for a given resource budget. would still be interesting to try though)
    - kragen 2y ago
      this sounds interesting! i think aa is linear in the number of terms, and reduced aa is linear in the number of independent variables, but possibly i don't understand your meaning

Couldn't the overdetermination problem be solved by tagging intervals with their ids? E.g., "x*x" should be resolved as "(x, i[-3, 3])*(x, i[-3, 3])" and "i[-3,

kragen 2y ago

this is basically how affine arithmetic works. but in interval arithmetic or modal interval arithmetic the representation of a float is two floats, and in affine arithmetic the representation of a float is a potentially unboundedly large set of float coefficients, none of which can be safely ignored, so there are some drawbacks to this approach i'm not sure why wayne doesn't mention affine arithmetic and modal interval arithmetic in this post; i'd think they were relevant

lifthrasiir 2y ago
> none of which can be safely ignored Or more accurately speaking, they can be ignored but at some expense of accuracy. (You can always approximate every variable with a (-inf, +inf) interval!) There are several working ways to "compress" affine variables when they get too many. Probably a worse problem with AA is that every multiplication introduces a new variable, so it can be very frequent to head into the maximum number of variables set for the reasonable performance...
- kragen 2y ago
  agreed. i find reduced affine arithmetic the most appealing, but haven't tried it

moonchild 2y ago

this requires all terms to be represented symbolically, which 'works', but now you need a full-blown symbolic rewrite engine to try to simplify things. very reasonable for an optimiser but not so much for numerics. for numerics a more common approach is interval mincing. we have a function f(x) = x*x, and try to apply f([-3 3]). we can 'mince' the inner interval and say that (e.g.) [-3 3] = [-3 -1] U [-1 1] U [1 3]. so we have f([-3 -1] U [-1 1] U [1 3]); distribute function application over U (which is sound) to get f([-3 -1]) U f([-1 1]) U f([1 3]), which is obviously tighter than f([-3 3]). we picked a subinterval size of 2, but can shrink it arbitrarily until we're satisfied with the result. this technique is essentially a form of case analysis, and can also be applied to optimisers/static analysers (complementarily to simplifying rewrites)

kragen 2y ago
affine arithmetic does not need a full-blown symbolic rewrite engine, though it too sometimes produces overbroad intervals
- moonchild 2y ago
  so a middle ground (as many pseudo-symbolic approaches). glanced at wikipedia—this seems not dissimilar conceptually to the abstract domain of polyhedra, in that it's symbolic but has a flat structure and expresses only linear relationships. of course, polyhedra are exponential where affine arithmetic is quadratic (overall space in number of terms), and polyhedra are global where affine is local (therefore easier to implement as a library, but no sharing). more missed connections between numerical analysis and program analysis? (meh but no sharing probably means affine generally loses for a given resource budget. would still be interesting to try though)
  - kragen 2y ago
    this sounds interesting! i think aa is linear in the number of terms, and reduced aa is linear in the number of independent variables, but possibly i don't understand your meaning