Python Math Equivalence Testing

Question

I have two lines in Python,

A m * B s / (A m + C m) 

and

 C m * B s / (C m + A m) 

which are equivalent functions of the disordered set (A, C) and the disordered set (B). m and s indicate units that can be replaced by the same, but not with a different device.

So far, I have performed permutations of A, B, and C and tested them using eval and the SymPy == operator. This has several disadvantages:

• for more complex expressions, I have to generate a large number of permutations (in my case, 8 nested for loops)
• I need to define A, B, C as characters, which is not optimal when I don’t know what parameters I will have (so I have to generate them all)> terribly inefficient and ruin the variable namespace)

Is there a python way to check equivalence? It should work with arbitrary expressions.

Answer 1

Here is a simplified approach based on my previous answer.

The idea is that if two expressions are equivalent in permutations, a permutation that transfers one to another should map the ith character in the first line (ordered by the index of the first occurrence) to the ith character in the second line (again ordered by the index of the first occurrence ) This principle can be used to construct a permutation, apply it to the first line, and then check the equality with the second line - if they are equal, they are equivalent, otherwise they are not.

Here is one possible implementation:

 import re # Unique-ify list, preserving order def uniquify(l): return reduce(lambda s, e: s + ([] if e in s else [e]), l, []) # Replace all keys in replacements with corresponding values in str def replace_all(str, replacements): for old, new in replacements.iteritems(): str = str.replace(old, new) return str class Expression: units = ["m", "s"] def __init__(self, exp): self.exp = exp # Returns a list of symbols in the expression that are preceded # by the given unit, ordered by first appearance. Assumes the # symbol and unit are separated by a space. For example: # Expression("A m * B s / (A m + C m)").symbols_for_unit("m") # returns ['A', 'C'] def symbols_for_unit(self, unit): sym_re = re.compile("(.) %s" % unit) symbols = sym_re.findall(self.exp) return uniquify(symbols) # Returns a string with all symbols that have units other than # unit "muted", that is replaced with the empty string. Example: # Expression("A m * B s / (A m + C m)").mute_symbols_for_other_units("m") # returns "A m * s / (A m + C m)" def mute_symbols_for_other_units(self, unit): other_units = "".join(set(self.units) - set(unit)) return re.sub("(.) ([%s])" % "".join(other_units), " \g<2>", self.exp) # Returns a string with all symbols that have the given unit # replaced with tokens of the form $0, $1, ..., by order of their # first appearance in the string, and all other symbols muted. # For example: # Expression("A m * B s / (A m + C m)").canonical_form("m") # returns "$0 m * s / ($0 m + $1 m)" def canonical_form(self, unit): symbols = self.symbols_for_unit(unit) muted_self = self.mute_symbols_for_other_units(unit) for i, sym in enumerate(symbols): muted_self = muted_self.replace("%s %s" % (sym, unit), "$%s %s" % (i, unit)) return muted_self # Define a permutation, represented as a dictionary, according to # the following rule: replace $i with the ith distinct symbol # occurring in the expression with the given unit. For example: # Expression("C m * B s / (C m + A m)").permutation("m") # returns {'$0':'C', '$1':'A'} def permutation(self, unit): enum = enumerate(self.symbols_for_unit(unit)) return dict(("$%s" % i, sym) for i, sym in enum) # Return a string produced from the expression by first converting it # into canonical form, and then performing the replacements defined # by the given permutation. For example: # Expression("A m * B s / (A m + C m)").permute("m", {"$0":"C", "$1":"A"}) # returns "C m * s / (C m + A m)" def permute(self, unit, permutation): new_exp = self.canonical_form(unit) return replace_all(new_exp, permutation) # Test for equality under permutation and muting of all other symbols # than the unit provided. def eq_under_permutation(self, unit, other_exp): muted_self = self.mute_symbols_for_other_units(unit) other_permuted_str = other_exp.permute(unit, self.permutation(unit)) return muted_self == other_permuted_str # Test for equality under permutation. This is done for each of # the possible units using eq_under_permutation def __eq__(self, other): return all([self.eq_under_permutation(unit, other) for unit in self.units]) e1 = Expression("A m * B s / (A m + C m)") e2 = Expression("C m * B s / (C m + A m)") e3 = Expression("A s * B s / (A m + C m)") f1 = Expression("A s * (B s + D s) / (A m + C m)") f2 = Expression("A s * (D s + B s) / (C m + A m)") f3 = Expression("D s") print "e1 == e2: ", e1 == e2 # True print "e1 == e3: ", e1 == e3 # False print "e2 == e3: ", e2 == e3 # False print "f1 == f2: ", f1 == f2 # True print "f1 == f3: ", f1 == f3 # False 

As you pointed out, this checks for row equivalence under permutations, ignoring mathematical equivalence, but that's half the battle. If you had a canonical form for mathematical expressions, you could use this approach for two expressions in canonical form. Perhaps one of the cute Simplify could do the trick.

Answer 2

Instead of repeating all possible permutations, suppose that exists and is trying to build it. I believe that this is done correctly, the failure of the algorithm would imply the existence of a permutation.

Here is the outline of the idea applied to the above expressions:

let:

 str1 = "A m * B s / (A m + C m)" str2 = "C m * B s / (C m + A m)" 

We are looking for a permutation of the set (A, C), which will make the expressions identical. Relabel A and C as X1 and X2 according to the order of their first appearance in str2, therefore:

 X1 = C X2 = A 

because C appears before A in str2. Then create an array Y such that y [i] is the ith character of A or C in the order of the first occurrence in str1. So:

 Y[1] = A Y[2] = C 

Since A appears before C in str1.

Now build str3 from str2, replacing A and C with X1 and X2:

 str3 = "X1 m * B s / (X1 m + X2 m)" 

And then start replacing Xi for Y [i]. First, X1 becomes Y [1] = A:

 str3_1 = "A m * Bs / (A m + X2 m)" 

At this point, compare str3_1 and str1 with the first occurrence of any of Xi, in this case X2, since these two lines are equal:

 str3_1[:18] = "A m * B s / (A m + " str1[:18] = "A m * B s / (A m + " 

You have a chance to build a permutation. If they were unequal, you would not prove that a suitable permutation does not exist (because any permutation would have to make at least this replacement) and could deduce nonequivalence. But they are equal, so go to the next step, replacing X2 with Y [2] = C:

 str3_2 = "A m * B s / (A m + C m)" 

And this equals str1, so you have your permutation (A-> C, C-> A) and have shown the equivalence of the expressions.

This is only a demonstration of the algorithm for a specific case, but it should generalize. Not sure which lowest order you could get, but it should be faster than n! generating all permutations on n variables.

If I understand the meaning of units correctly, they limit which variables can be swapped and others can be swapped. Thus, A can be replaced by C in the above expressions, because both have units "m", but not with B, which have "s" units. You can handle this as follows:

build the expressions str1_m and str2_m from str1 and str2, removing all characters that do not have m units, and then execute the above algorithm for str1_m and str2_m. If the build fails, the permutation does not exist. If the build is successful, save this permutation (call it m-permutation) and build str1_s and str2_s from str1 and str2, deleting all characters that don't have s-units, then run the algorithm again for str1_s and str2_s. If construction is not completed, they are not equivalent. If that succeeds, the final permutation will be a combination of m-permutation and s-permutation (although you probably don't even need to create it, you just need it to exist).

Answer 3

If you pass a string to the Sympy sympify() function, it will automatically create characters for you (there is no need to define all of them).

 >>> from sympy import * >>> x Traceback (most recent call last): File "<stdin>", line 1, in <module> NameError: name 'x' is not defined >>> sympify("x**2 + cos(x)") x**2 + cos(x) >>> sympify("diff(x**2 + cos(x), x)") 2*x - sin(x) 

Answer 4

I did this once, in one simulator of mathematical teachings. Well, in my case, I knew which variables would be used.

So, I checked the result by putting the values ​​inside vars.

 A = 10 B = 20 C = 30 m = Math.e s = Math.pi 

So we decide:

 s1 = 'A m * B s / (A m + C m)' s2 = 'C m * B s / (C m + A m)' 

If s1! = S2, it is proved that there is no equivalence

Using this method, it is impossible to say that two expressions are equivalent, but you can say that both of them are not equivalent

 if s1 != s2: print "Not equivalent" else: print "Try with another sample" 

Good .. I hope this can help you.

Answer 5

This, like all other answers to date, is not a reliable solution to the problem, but instead contains more useful information for our future meticulous friend to solve this problem.

I present a complex example using the Euler formula https://en.wikipedia.org/wiki/Euler%27s_formula

I am sure that all other overflow answers up to date will fail in my example.

I show that all suggestions on the sympy site also do not work on my example. ( https://github.com/sympy/sympy/wiki/Faq )

 #SOURCE FOR HELPERS: https://github.com/sympy/sympy/wiki/Faq import sympy import sympy.parsing.sympy_parser ExampleExpressionString1 = 'exp( i*( (x0 - 1)*(x0 + 2) ) )' ExampleExpressionSympy1 = sympy.parsing.sympy_parser.parse_expr(ExampleExpressionString1) ExampleExpressionString2 = 'i*sin( (x0 - 1)*(x0 + 2) ) + cos( (x0 - 1)*(x0 + 2) )' ExampleExpressionSympy2 = sympy.parsing.sympy_parser.parse_expr(ExampleExpressionString2) print '(ExampleExpressionSympy1 == ExampleExpressionSympy2):' print ' ', (ExampleExpressionSympy1 == ExampleExpressionSympy2) print '(ExampleExpressionSympy1.simplify() == ExampleExpressionSympy2.simplify()):' print ' ', (ExampleExpressionSympy1.simplify() == ExampleExpressionSympy2.simplify()) print '(ExampleExpressionSympy1.expand() == ExampleExpressionSympy2.expand()):' print ' ', (ExampleExpressionSympy1.trigsimp() == ExampleExpressionSympy2.trigsimp()) print '(ExampleExpressionSympy1.trigsimp() == ExampleExpressionSympy2.trigsimp()):' print ' ', (ExampleExpressionSympy1.trigsimp() == ExampleExpressionSympy2.trigsimp()) print '(ExampleExpressionSympy1.simplify().expand().trigsimp() == ExampleExpressionSympy2.simplify().expand().trigsimp()):' print ' ', (ExampleExpressionSympy1.simplify().expand().trigsimp() == ExampleExpressionSympy2.simplify().expand().trigsimp()) 

MORE NOTES:

I suspect that this is a difficult problem to solve in general and reliable. To correctly verify mathematical equivalence, you need to not only try the permutation of orders, but also have a library of mathematical equivalent transformations and try all these permutations.

I believe this may be a solvable problem, because Wolfram Alpha seems to have an “alternative expression” section that seems to do the trick of providing all permutations most of the time on arbitrary expressions using these equivalents.

IN CONFIRMATION:

I suggest the following with the expectation that it will break:

 import sympy import sympy.parsing.sympy_parser Expression.simplify().expand().trigsimp()