[ANN] SymbolicIntegration.jl - indefinite integration with Symbolics.jl symbols

For a while now I have been developing SymbolicIntegration.jl, that lets you solve symbolic integrals in julia! it has for now two different methods to arrive at the antiderivative:

  • Risch algorithm
  • Rule based method using >3000 rules

Example usage:

julia> integrate(sqrt(4 - 12*x + 9*x^2)+sqrt(1+x),x;verbose=true)
┌-------Applied rule 0_1_0 on ∫(sqrt(1 + x) + sqrt(4 - 12x + 9(x^2)), x)
| ∫( a + b + ..., x) => ∫(a,x) + ∫(b,x) + ...
└-------with result: ∫(sqrt(4 - 12x + 9(x^2)), x) + ∫(sqrt(1 + x), x)
┌-------Applied rule 1_2_1_1_3 on ∫(sqrt(4 - 12x + 9(x^2)), x)
| ∫((a + b * x + c * x ^ 2) ^ p, x) => if 
|       !(contains_var(a, b, c, p, x)) &&
|       (
|             b ^ 2 - 4 * a * c == 0 &&
|             p !== -1 / 2
|       )
| ((b + 2 * c * x) * (a + b * x + c * x ^ 2) ^ p) / (2 * c * (2 * p + 1))
└-------with result: (1//36)*((4 - 12x + 9(x^2))^(1//2))*(-12 + 18x)
┌-------Applied rule 1_1_1_1_4 on ∫(sqrt(1 + x), x)
| ∫((a + b * x) ^ m, x) => if 
|       !(contains_var(a, b, m, x)) &&
|       m !== -1
| (a + b * x) ^ (m + 1) / (b * (m + 1))
└-------with result: ((1 + x)^(3//2)) / (3//2)
((1 + x)^(3//2)) / (3//2) + (1//36)*((4 - 12x + 9(x^2))^(1//2))*(-12 + 18x)

please try it and tell me what you think, also report any bugs or functions that the package is not able to integrate opening issues on github, thanks!!!

42 Likes

Amazing work!

1 Like

Very cool, congrats.

Just for my personal interest, do you have to write these rules by hand?

Because it looks like a nightmare

5 Likes

good job!

1 Like

Somebody did: it comes from https://rulebasedintegration.org/

Sadly, the maintainer of that did pass away relatively recently, so the Julia package will likely be the spiritual successor.

12 Likes

exactly, i used the rules from the mathematica package, that contains 6700 integration rules. to convert them to julia I created a script to translate them automatically, but there was stil a lot of translation by hand, just reading mathematica code and writing julia equivalent. Right now approx 3400 rules are translated.

15 Likes

Very exciting work! Last I checked, Mathematica has a more sophisticated pattern syntax and better support for associative-commutative pattern matching. Did you have to work around this issue, or was the translation straightforward?

1 Like

Exactly, you got the point! The translation was definitely not straightforward, yes I extended SymbolicUtils pattern matching this summer, creating the “defslots” that allow to match a pattern with some default values, and improving the handling of commutative pattern matching. Also I improved pattern matching of powers with negative exponents, that was quite difficult and still not completely solved. Here you can read in more detail.

On top of that the old SymbolicUtils pattern matching was too slow to handle the thousands of rules I needed, so in the last weeks I rebuilt it from scratch improving ttfx from 14 min to 12 sec! I am so happy about it, on my blog post you can read in more detail

19 Likes

I’m interesting in the possibilities of SymbolicIntegration. I have tried using SymbolicIntegration, and on my computer it takes a while to import all the rules. It seems like rules are imported every time I use the package. Is that correct?

yeah probably you tried before version 3.3.0, that i released in the last days. As i said above i have rewrittent the pattern matching system from scratch, and now it takes ~12 sec on my laptop (macbook m1 2020) to load all the rules and precompile the integrate function, while before version 3.3.0 was 14 minutes

When I was young, I watch Dr Who and one episode talks about Block Transfer Computation.

A Block Transfer Computation was a mathematical process used to create objects and affect spacetime in other ways through the power of pure mathematics. The process usually involved chanting.

Computers could not do Block Transfer Computations, as the calculations themselves would alter the nature of the computer. Though they were working on technological means to do so, the Logopolitans were destroyed before they completed it. As such, organic life forms had to do the work as morphologically unstable living organic matter could handle the stress of reality-changes caused by block transfer mathematics.

I really believe that Integration is Block Transfer Computation because computers cannot do Integration. This seems to be true when that episode of Dr Who first came out.

Then I discovered Mathematica…

2 Likes

And now you discovered SymbolicIntegration.jl

3 Likes

Currently SymbolicIntegration.jl has the same rules as Rubi? Or it aims to incorporate more rules?

Right now it’s aiming to incorporate them all, and it has a few other integrators as well like a Reisch method.

2 Likes

I see that you added awareness of commutativity beyond top level in SymbolicUtils.jl. However, the following simple factorization rule still doesn’t work with SymbolicUtils v4.10.0:

julia> @syms a b c
(a, b, c)

julia> r = @rule ~a*~b + ~a*~c => ~a * (~b+~c)
~a * ~b + ~a * ~c => ~a * (~b + ~c)

julia> r(a*b + a*c)
a*(b + c)

julia> r(b*a + b*c)

julia> 

The last line of code returned nothing due to a failed match, as the expression is internally stored as a*b + b*c and fails to match the LHS of the factorization rule, ~a*~b + ~a*~c. So commutativity is not fully taken into account. Is this a known issue?

1 Like

That’s strange, I I think should work because the @rule macro tries all possible ordering for commutative operations… I will investigate

I think that default symbols in SymbolicUtils are supposed to be Numbers, which are not necessarily commutative. If you declare @syms a::Real b::Real c::Real it does indeed apply the rule.

2 Likes

It still fails one of the cases with your suggested change:

julia> using SymbolicUtils

julia> @syms a::Real b::Real c::Real
(a, b, c)

julia> r = @rule ~a*~b + ~a*~c => ~a * (~b+~c)
~a * ~b + ~a * ~c => ~a * (~b + ~c)

julia> r(a*b + a*c)

julia> r(a*b + b*c)
(a + c)*b

What’s strange is that the matching succeeds in the latter case which involves nontrivial reordering with commutativity but not the former simpler case.

1 Like

For now the rule macro doesn’t really make a difference and treats Number as commutative, so the showed example should work

Yes, so internally the arguments of a operation are ordered pretty much randomly, but DIFFERENT from what is showed on the repl. So the order you see is not the actual order of the arguments in memory.

Anyway I have investigated and the reason sometimes this example fails is because the macro now doesn’t actually try every permutation of arguments in every commutative operation, it stops trying when it finds a matching permutation for a sub expression… The full explanation would be quite long so I won’t go into further detail. I could fix it but I don’t have time

1 Like