Symbolic expression bounds

I have a symbolic expression (the real expression can be anything the Symbolic Toolbox supports) but for example we can use the following:

expr = sym('a + b')

Also, I know that a and b are integers and that their "legal" values go from 1 to 7.

I would like to figure out what are the bounds of expr. In this case, the min value would be 2 and the max value would be 14.

Is there any way to do this type of analysis?

Thanks Joan

[Andrew Newell]

Judging by your response below, this isn't a complete statement of your real problem. Try editing your question to provide more detail. For example, is the user only allowed certain variable names? Do you know in advance what the allowed variables are?

[Walter Roberson]

Would it not also be necessary to prove that the output was integral?

[Joan Puig]

The user is only allowed to use certain variables.

With the symvar function I can extract them and make sure that they are all known.

Each one of this variables has a set of properties (value bounds, matrix size, and if they are integers or reals) which I know and I can use to help the solver.

Answer 1

[Walter Roberson]

Unfortunately there is no theoretical way to do that for arbitrary expressions.

For the special case of linear operations, you can use the linear minimizer or maximizer: see http://www.mathworks.com/help/toolbox/mupad/linopt/index.html

More generally for expressions in one variable, you would differentiate the expression, find the zeros of that, differentiate the expression again, evaluate at the zeros to determine whether you are looking at a min, max, or saddle point. Solving for the zeros might be difficult or impossible though...

For expressions in multiple variables, the question of the range becomes equivalent to the question of finding the global extrema. It is known that there is no general algorithm for that, but there are some classes of expressions that it can be solved for.

[Walter Roberson]

At the MuPad level you could ask,

solve(a+b<LowIndex or a+b>HighIndex) assuming a::integer and b::integer and a>=1 and a<=7 and b>=1 and b<=7;

If the empty set is returned then either solve() was too weak for the task and it failed to notice that, or solve() was able to prove that no combination satisfies the limit.

If a non-empty set is returned, then either solve() was able to establish that there is a combination that is outside the bounds or else solve() was able to decide that it was not strong enough to create a solution.

In the case where solve() decides it is too weak for a solution, I cannot tell from the documentation exactly what it will return. In Maple it would return the call unevaluated.

There are other ways to write the expression to be solved. See

http://www.mathworks.com/help/toolbox/mupad/stdlib/solve.html

and http://www.mathworks.com/help/toolbox/mupad/stdlib/assume.html

[Joan Puig]

This approach would work and it would be relatively easy to construct the equations to solve.

You made a good observation: I would also need to prove that the result is an integer. Do you have any ideas to figure that out?

[Walter Roberson]

I am not sure of the best way to express negation in MuPad's solve()

Perhaps something like,

EXPRESSION minus LowValue..HighValue <> {}

[Joan Puig]

While there doesn't seem to be any out of the box solutions, I am going to accept this answer as it provides some good ideas and allowed me to implement apartial solution to the problem

Answer 2

[Andrew Newell]

It makes little sense to use the Symbolic Toolbox for such an operation because comparisons like max and min are not allowed on symbolic objects and it is trivial to do in MATLAB:

a = 1:7;
b = 1:7;
min(a+b), max(a+b)

[Joan Puig]

The problem is that the user types in the expression so I can't hard code them into MATLAB code.

This expressions are then used to calculate an index into a matrix and I need to prove that the user didn't enter an equation that will create an index out of bounds error.

I am thinking something along this lines: http://en.wikipedia.org/wiki/Formal_verification

[Walter Roberson]

What operations are the user permitted to use in the expression?

[Joan Puig]

The user is allowed to type in any symbolic expression they want.

The workflow is like this:

-Check is that the symbolic expression is correct sym(userInput)

-Check that all the variables in it are known symvar(expr)

-Check that the matrix indicies are within the size of the matrix

[Walter Roberson]

If the user is allowed to type in "any symbolic expression they want" then they could, for example, put 1/(a^d + b^d - c^d) as one of the sub-terms. This is a rational number for all a, b, c, d positive integers, d>=3, if and only if Fermat's Last Theorem holds, and otherwise could become 1/0 . Is your formal verification system prepared to prove Fermat's Last Theorem?

Likewise a similar technique could be used to express the Riemann Zeta function and make assertions about its values.

You have to restrict operations and functions called by quite a bit in order to hope to be able to reliably do formal verification.

[Joan Puig]

I agree, the general problem is not solvable. In practive though, I don't need to be able to verify all inputs.

It would be acceptable to tell the user that we could not verify the input therefore they need to change it if they want to continue.

Answer 3

[Andrew Newell]

If you have a pre-determined set of variables and a finite number of possible values for them, you might be able to use an approach like this:

1. Create a function out of the expression using matlabfunction.
2. Feed all possible values of the variables into your function and find the min and max.