Equality Equations (in C ++ or with Unix tools) (isomorphism of algebra functions)

Question

I'm looking for an C ++ open source library (or just an open source Unix tool): Equality checking on equations .

Equations can be built at runtime as AST Trees, string, or other format.

The equations will be mostly simple algebras with some assumptions about unknown functions. The domain will be integer arithmetic (no floating point problems, since the problems associated with this are well known) Thanks @hardmath for this, I assumed it was known).

Example: Input may contain a phi function, with assumptions about this (in most cases) phi(x,y)=phi(y,x) and try to solve:

equality_test( phi( (a+1)*(a+1) , a+b ) = phi( b+a, a*a + 2a + 1 )

It can be fuzzy or any equality test - I mean that it does not always have to succeed (it can return “false” even if the equations are equal).

If there is a problem with the supporting assumptions described above about the phi function, I can handle this, so simple linear equality algebra testers are welcome.

• Could you recommend some C / C ++ programming libraries or Unix tools? (Open source)
• If possible, can you attach an example of how such an equality test might look in a given library / tool?

PS If such equality_test could (if successful) return an isomorphism - (what I mean, a kind of "mapping") between two given equations, it would be very desirable. But tools without such features are also welcome.

PS By “fuzzy tester” I mean that in internal solutions the equation will be “fuzzy” from the point of view of searching for the “isomorphism” of two functions, and not from the point of view of testing for random inputs - I could implement this, of course, but I try to find something with better accuracy.

PPS There is another problem why I need a better solution to improve performance than "testing all inputs." The above equation is a simple form of my internal problem , where I have no comparison between the variables in the equations . That is, I have eq1=phi( (a+1)*(a+1) , a+b ) and eq2=phi( l+k, k*k + 2k + 1 ) , and I should find out that a==k and b==l . But this subproblem, with which I can cope with the “brute force” approach (even the asymptotic complexity of this approach), there are only a few variables, let it be 8. Therefore, I will need to make this test equation for every possible mapping. If there is a tool that does all this work, I would be very grateful and could contribute to such a project. But I do not require such functionality, just the system_test () equation will be enough, I can easily cope with the rest.

Summarizing:

• equal_test () is just one of many sub-tasks that I have to solve, so computational complexity matters.
• it should not be 100% reliable, but a higher probability than just testing equations with several random inputs and variable mapping is welcome :).
• conclusion "yes" or "no" (all additional information may be useful, but in the future at this stage I need "Yes" / "No")

Answer 1

Your topic is one of an automatic theoretical proof , for which a number of free open source software packages have been developed. Many of them are designed to test evidence, but what you ask is a search for evidence.

Working with the abstract theme of equations will be the theory of mathematicians called varieties . These theories have good properties regarding the existence and regularity of their models.

Perhaps you mean equations that deal specifically with real numbers or another system, which adds some axioms to the theory in which proof is sought.

If in principle there is an algorithm for determining whether a logical statement can be proved in a theory, this theory is called decidable. For example, the theory of real closed fields is decidable, as Tarski showed in 1951. However, the practical implementation of such an algorithm is absent and, possibly, impossible.

Here are a few open source packages that might be worth learning something about how to be guided by your design and development:

Tac: A Common and Adaptable Interactive Theorem Tool

Prover9: automatic theoretical verification for first-order logic and equator

E (quational) Theoretical Run

Answer 2

I'm not sure about any library, but how do you do it yourself by creating a random set of inputs for your equation and substituting it into both equations that need to be compared. This will give you an almost correct result if you create a significant amount of random data.

Edit: You can also try http://www.wolframalpha.com/

from

  (x+1)*(y+1) equals x+y+xy+2 

and

  (x+1)*(y+1) equals x+y+xy+1 

Answer 3

I think you can get pretty far using Reverse Polish Notation.

• Write out your equation using RPN

• Apply transforms to bring all expressions into the same form, for example. * A + BC → + * AB * AC (which is the equivalent of RPN A * (B + C) → A * B + A * C), ^ * BCA → * ^ BA ^ CA ((B * C) ^ A → B ^ A * C ^ A)

• "Sorting" the arguments of a symmetric binary operator, so that on the one hand there appear "lighter" operations (for example, A * B + C → C + A * B)

• You will have a problem with dummy variables, such as sum indices. In my opinion, there is no other way, but try each combination of their correspondence on both sides of the equation.

In general, the problem is very complicated.

However, you can try to hack: use an optimizing compiler (C, Fortran) and compile both sides of the equation to optimize machine code and compare the outputs. It may or may not work.

Answer 4

The Maxima Opensource (GPL) project has a tool similar to the Wolfram Alpha equal tool :

 (a+b+c)+(x+y)**2 equals (x**2+b+c+a+2*x*y+y**2) 

is (equal ()) which solves the formulas:

 (%i1) is(equal( (a+b+c)+(x+y)**2 , (x**2+b+c+a+2*x*y+y**2) )); (%o1) true 

For this purpose, he uses the rational simplified - ratsimp to simplify the difference between the two equations. When the difference of two equations simplifies to zero, we know that they are equal for all possible values:

 (%i2) ratsimp( ((a+b+c)+(x+y)**2) - ((x**2+b+c+a+2*x*y+y**2)) ); (%o2) 0 

This answer simply shows the direction (like the other answers). If you know about something like this, it can be used as part of a C ++ Unix programming program - ? . Good C / C ++ binds a similar tool to this. Please write a new answer.