assumptions_handlers

Aaron Meurer edited this page Oct 6, 2013 · 3 revisions
Clone this wiki locally

Types of assumptions handlers

The following table goes through the handler code, but is not entirely exhaustive, because some of the code is confusing, redundant, or tautological.

Assumption Free Subexpression Computational
Infinitesimal any(Q.infinitesimal(arg) for arg in Mul.args) expr.evalf() == 0 if expr.is_number
(only works if each arg is infinitesimal or bounded)
Bounded See truth table in AskBoundedHandler.Add
See truth table in AskBoundedHandler.Mul Abs()<=1**Positive -> Bounded
Unbounded**NonZero -> Unbounded Abs()>=1**Positive -> Bounded
Bounded**Bounded -> Bounded
Q.bounded(x) >> Q.bounded(log(x))
Q.bounded(x) >> Q.bounded(exp(x))
(these last two may be iff)
Commutative Not commutative if any subexpression is not commutative
(it actually just checks the .args, but I think forward
chaining would give this)
Square expr.shape[0] == expr.shape[1]
Symmetric all(symmetric(arg) for arg in MatMul.args)
A*…*A.T is symmetric iff the … is symmetric
all(symmetric(arg) for arg in MatAdd.args)
~Q.square >> ~Q.symmetric symmetric iff square for ZeroMatrix
(this is only specified for Q.symmetric(A) iff Q.symmetric(A.T)
MatrixSymbol, but it should slice is symmetric if it’s on_diag and the parent is
be true for any expression) symmetric
Invertible Q.invertible >> Q.square Mul is invertible iff each arg is (this is not in there, but for an
Identity and Inverse are always invertible explicit matrix, the invertibility
ZeroMatrix is always not invertible can be computed)
(not in there, but Q.invertible(A) iff Q.zero(det(A)))
A is invertible iff A.T is invertible
slice is invertible if it’s on_diag and the parent is
invertible
Orthogonal Q.orthogonal >> Q.invertible MatMul is orthogonal iff each factor is and the scalar
Q.orthogonal >> Q.square factor is 1
(this can be deduced) MatMul is not orthogonal if any factor is not invertible
(this one can probably be deduced from other facts)
Identity is always orthogonal
ZeroMatrix is never orthogonal
A is orthogonal iff A.T is orthogonal
A is orthogonal iff A**-1 is orthogonal
(I skipped a
lot of the
matrix
expression
stuff because
it was
getting
repetitive)
Prime Mul of integers is not prime (note, this is not entirely For explicit integers, uses isprime
true, as Q.integer does not mean it’s not 1)
integer**integer is not prime (again, not true because
of some corner cases)
Composite composite iff nonprime
positive integer
Even even >> integer Various combinations of even and odd in Mul For explicit integers i % 2 == 0
various things that can be Integer*Integer is even if Integer + Integer is odd
deduced from this If exactly one element of a Mul is irrational, it isn’t
even (actually isn’t an integer, so it probably should
go there).
The obvious ones for even and odd in Add
Various rules for integer**integer
if x is even, then abs(x), re(x), im(x) are even
Odd odd iff integer and not even
Negative positive + positive = positive If is_number, evalf < 0
negative + negative = negative
(this is actually done more generally for and Add of n
args)
For Mul, parity of positive and negative elements
real**even = nonnegative
real**odd = same as base
nonnegative**positive = nonnegative
exp(x) is positive if x is real (should follow from Pow
but exp is not a Pow)
NonZero Add is nonzero if all terms are positive or if all terms expr.evalf() != 0
are negative
Mul is nonzero iff each term is nonzero
Pow is nonzero if base is nonzero (reverse implication
is true only for positive exponent)
Abs(x) is zero iff x is zero
Zero zero iff not nonzero and Mul is zero iff any term is zero. Should be deducible
real from nonzero (or visa-versa)
positive If each term in a Mul is positive or negative, it is expr is real and expr.evalf() > 0
positive if there are an even number of negative terms
Add is positive if at least one positive term and the
rest are nonnegative
positive**real = positive
negative**even = positive
negative**odd = not positive
exp(real) = positive
factorial(integer) = positive
abs(nonzero) = positive (note, this really should be
not zero, not nonzero, because it is true even for
complex non-zero numbers).
Trace(positive_definite) = positive
Determinant(positive_definite) = positive
MatrixElement on the diagonal is positive if the matrix
is positive_definite
Integer Integer + Integer = Integer int(expr.round()) == expr
Integer + not Integer = not Integer Rational (the class) == not Integer
Integer*Integer = Integer (otherwise it would evaluate to
Integer*Irrational = not Integer (in general, if there is Integer)
exactly one irrational, it is irrational)
odd/even = not integer
Abs(x) is integer iff x is integer (not correct; only
true if x is also real)
MatrixElement is integer if the Matrix is IntegerElements
Same with Determinant and Trace
Rational Rational + Rational = Rational
Rational + not rational = not rational (in general, if
exactly one non-rational, it is not rational)
Same for Mul

Notes:

  • It’s hard to tell which implications are really double implications. Each one would have to be checked.
  • There are a lot “if Q.assumption(expr) in conjuncts(assumptions)” which are completely irrelevant to the handler in question. I have a hard time believing that these wouldn’t work without this bit of code.
  • Some of these apply to single constants (like pi), which could technically be viewed as subexpression or computational
  • I don’t think there’s a need to special-case things like “IdentityMatrix is always invertible” in the code. You can just add the fact Equivalent(Q.invertible(A), True) when A is an IdentityMatrix, and it will take care of itself. This may sound silly, but I think we can use the same idea for the computational assumptions.
  • I’m not sure how the Factorization stuff in the matrix expressions work.
  • Most subexpressions are just vectorized over the same assumption, either via And or Or. A few are interesting, though. For example integer*integer is even if integer + integer is odd.
  • The current handlers code is just terrible. Half the time it uses the new assumptions, half the time it uses things like “if not as_real_imag()[1]” (instead of Q.real). There are a ton of unnecessary redundancies (not just logically duplicate, but actually duplicate in that the current code would still compute the same thing if certain lines of code were removed, such as many duplicate “if self._number()” calls). Some of the logic is wrong (I’ve pointed out some instances of this above). In many places, the fuzzyness of the logic is not taken into account. In those places that do, some use fuzzy_or and so on, and some write the difficult to read for loop. The few handlers that are documented have confusing docstrings, which mention restricted cases of what is actually implemented, or even cases that aren’t even relevant to the particular assumption at hand (though to be sure, the truth tables for the bounded assumption are quite helpful). Some functions are implemented, but seemingly at random. The code is hard to read, mostly because most of it feels duplicated, but also because it can be hard to convert loops and if blocks to three-valued fuzzy logic.