Qalculate / libqalculate

Qalculate! library and CLI
https://qalculate.github.io/
GNU General Public License v2.0
1.72k stars 140 forks source link

Adding Unification ability (long term enhancement) #104

Open vvs- opened 5 years ago

vvs- commented 5 years ago

Currently Qalculate! suffers from very specialized expression simplifications. It's impossible to do more sophisticated transformations. Implementing such generic transformation framework would have great benefits, enabling more powerful transformations.

It can find solutions for e.g.

x^x=2^2
sin(x)^2+cos(x)^2=sin(x)

but it can't solve very similar

x^(1/x)=2^(1/2)
1-cos(x)^2=sin(x)
hanna-kn commented 5 years ago

x^(1/x)=a (or x^(x^b)=a) is considerably more complicated to solve than x^x=a, which each easy to solve using the Lambert W function.

The second example illustrates the incomplete simplification of trigonometric functions in Qalculate! (sin(x)^2+cos(x)^2 is simplified to 1, but 1 - cos(x)^2 is not simplified to sin(x)^2). Thanks to recent changes sin(x)^2+cos(x)^2=sin(x) will however now at least return the solution x = 0.5π + 2πn (previously avoided because it required use of the n variable, representing any integer).

Qalculate! needs a generic method for numerical approximation of equations, similar to how the Newton-Raphson method is currently used for solving high degree equations.

vvs- commented 5 years ago

Numerical solutions is a good thing to have indeed. They are not exact though.

What I thought of is a framework to search for generic patterns in expression tree, similar to a compiler's global optimization pass. So, instead of a local transformation tied to particular node it would be possible to apply some more universal transformations before trying specific solutions. It's impossible to predict all possible combinations of special cases, so a more generic approach would be more sane.

Trigonometric expressions are really hard in this regard, but at least it would be easier to solve many similar cases, like e.g. sin(atan(x))/cos(atan(x)) etc.

P.S. Compare x=log(4)/W(log(4)) for the first case and x=e^(-W₋₁(-log(2)/2)) for the second. But I guess that Qalculate! Lambert W function presently doesn't support that.

vvs- commented 5 years ago

BTW, using only local simplification has more subtle consequences when there are several alternatives. This equation is solved: 1/(1-sin(x)^2)+1/(1-cos(x)^2)=1/sin(x)^4. While this one does not: 1/(1-sin(x)^2)+1/(1-cos(x)^2)=1/cos(x)^4. The choice of a function is arbitrary though.

It could be disambiguated by using patterns to test that it is the same function on both sides before selecting a particular branch. Even if it could be resolved by other means, I sincerely doubt that it would be generic enough.

vvs- commented 5 years ago

Considering the above example, it's even worse than I thought. I'm getting spurious solutions for one equation but not the other, so it's even indeterminate.

hanna-kn commented 5 years ago

The current trigonometry changes is work in progress and inconsistencies are expected. I've also found an old bug, affecting some trigonometric expressions in exact mode, which I'm trying to track down. 1/(1-sin(x)^2)+1/(1-cos(x)^2)=1/sin(x)^4 is problematic, but 1/(1-sin(x)^2)+1/(1-cos(x)^2)=1/cos(x)^4 currently returns the correct (although unnecessary complicated) solutions.

I'm not really familiar enough with trigonometry and I'm unsure how a truly generic solution to simplification of expressions with different trigonometric functions should behave. One alternative is to transform sin(x) to i*e^(-i*x)/2 - i*e^(i*x)/2 and cos(x) to e^(-i*x)/2 + e^(i*x)/2, etc., but in most cases it only seems make the expressions more complicated and it is difficult to transform back to trigonometric functions.

vvs- commented 5 years ago

Yes, that's why I prefer generic framework and skeptical about specific optimizations.

But you seems to be missed the post above. The solutions I'm getting for those equations are not determinate. Sometimes I get solution for the first and after restarting Qalculate! and working some more, I'm getting the other equation solved but not the first.

BTW, your optimization for issue #106 strangely doesn't work for these equations.

hanna-kn commented 5 years ago

BTW, your optimization for issue #106 strangely doesn't work for these equations.

sqrt(2)/2 is currently not transformed to 1/sqrt(2), or vice versa, and asin(1/sqrt(2)) was not handled (I've fixed it locally).

vvs- commented 5 years ago

What's particularly bad about local optimizations is that they doesn't have enough context to make a right decision. So, I see the generic solution as a framework that enables specific optimizations to gather all necessary context information to make an informed decision. Like, for example, which transformation branch to pursue to obtain a solution. Pattern matching comes to mind, but there could be other options as well.

hanna-kn commented 5 years ago

The reason 1/(1-sin(x)^2)+1/(1-cos(x)^2)=1/sin(x)^4 fails is that sin(x)*cos(x) is transformed to sin(2x)/2. Currently the behaviour is somewhat random (dependent on the order of terms in the expression), but I haven't yet been able to reproduce the erratic you're describing.

vvs- commented 5 years ago

I didn't change the order of terms between runs. It looks more like a race condition to me. I didn't check if there are actually several threads though, so I may be wrong. But if this is indeed a race condition, it can't be reproduced in a debugger.

vvs- commented 5 years ago

Here is what I see. Expression is the same, but Qalculate! runs were different. Another possibility is some internal state which affects different expressions. screenshot from 2018-10-03 18-22-55 screenshot from 2018-10-03 18-25-37

hanna-kn commented 5 years ago

Here is what I see. Expression is the same, but Qalculate! runs were different. Another possibility is some internal state which affects different expressions.

The first is the same I get, and the second is what I see if I disable sin(x)*cos(x)=sin(2x)/2 transformation. This is what I would expect if the internal order of terms differs (differences in the user provided order should however normally never give different results). The internal order of functions is determined by the pointer and might thus potentially change between runs.

(You will get a cleaner result if the solve() function is used.)

vvs- commented 5 years ago

AFAIK, modern Linux distributions are supposed to randomize pointers for security reasons.

vvs- commented 5 years ago

I'm not really familiar enough with trigonometry and I'm unsure how a truly generic solution to simplification of expressions with different trigonometric functions should behave.

Some more thoughts about implementation of generic framework for simplification of expressions:

vvs- commented 5 years ago

That #113 brought forward the above general issue: how to choose among several alternative simplification strategies?

There could be many alternative representations, e.g. e^(i*pi) or -1, abs(x) or sqrt(x^2), sin(x)^2 or 1-cos(x)^2, sin(x) or cos(x-pi/2) etc. Some of them are better than others in particular circumstances. They all could be tried if there would be efficient strategy. Another option would be a hint from human user.

vvs- commented 5 years ago

So, I should admit that my assumptions about inner workings of heuristics in core library could be wrong sometimes. But that's the point: it's hard to reason about operational semantics in general purpose imperative programming language, like C++. People tend to use denotational semantics, even if subconsciously. And the choice of strategy made by algorithm should be flexible, i.e. user should have complete control over it. Separating that decision process from core library is one of possible solutions. Right now it's a black box with almost no user control over it, except for too many oversimplistic options, cluttering UI.

Every advanced CAS used domain specific language with powerful run-time evaluation and optimization for that purpose.

vvs- commented 4 years ago

After working for sometime with several proof assistants I'm now convinced that the enhancement I was talking about in this issue should be properly called Unification.

Every such application is supposed to have a database of rules (theorems or programs) which are applied to the conjecture in certain order until a solution is found. This is a semi-automatic process which is guided by user. There are plenty of implementations, including Jape, Coq or Lean, but these are for a different domain, i.e. theorem proving or software verification.

This description neatly fits to CAS or to CAS-like calculator. Such functionality would be a killer feature.