search

fredrik-johansson / fungrim

Fungrim: the Mathematical Functions Grimoire
MIT License
113 stars 15 forks source link

Storing formulas for Rubi #8

Open certik opened 5 years ago

certik commented 5 years ago

Can Fungrim store all the formulas for Rubi, so that SymPy and SymEngine can use it as a reference "ab-initio data" to be used to generate the fast decision tree for fast integration?

I read your introductory blog post and I think this is a great idea. SymPy can have a functionality to retrieve any formula from your database and be able to use it.

fredrik-johansson commented 5 years ago

That would be quite nice.

I think it's not enough to just add the integration formulas; you need some additional explicit data representing the decision tree. It should be doable, but I have not studied Rubi in detail so I can't really comment on what this would involve.

There is a more immediate, minor technical obstacle: I have not added any indefinite integrals yet to Fungrim, because I still need to figure out how to formalize indefinite integration in a good way.

First of all "the" indefinite integral is not well-defined because there's no consistent way to pick the constant of integration automatically (as far as I can see, at least). The output thus probably needs to be the set of all antiderivatives, so you would have something like

Equal(IndefiniteIntegrals(x**2, x), SetBuilder(x**3/3 + C, C, Element(C, CC)))

A way to make this less cumbersome would be to literally state that what you have is a representative of this set:

Element(x**3/3, IndefiniteIntegrals(x**2, x))

This does look a bit backwards, though; a third option would be introduce some kind of composite operator like

IndefiniteIntegralEqual(x**2, x, x**3/3)

defined to be semantically equivalent to either of the two formulas above, and which could be rendered to TeX simply as \int x^2 dx = x^3/3 + C.

The second problem is formalizing limit, derivative and antiderivative operations properly. The Limit and Derivative operators that already exist are ambiguous, which should be fixed. In particular, for derivatives, it's strictly speaking necessary to distinguish between directional derivatives, two-sided real derivatives, complex derivatives, formal derivatives, and probably some more variations too. This doesn't matter as long as the assumptions for the formulas restrict the variable of differentiation/integration to the interior of the holomorphic domain (for the function and all subexpressions in its definition), because then all the notions coincide. It does, however, matter if you want to define (directional) derivatives and indefinite integrals on branch cuts and for functions defined with removable singularities.

certik commented 5 years ago

Additional data can be represented in the Rubi module in SymPy or SymEngine. Right now the rules are stored manually in: https://github.com/sympy/sympy/tree/master/sympy/integrals/rubi/rules, it's in the form pattern (integral) -> replacement (either antiderivative or another, simpler, integral). I can imagine all these identities to be stored in Fungrim, and SymPy will just reference them by hashes.

What SymPy would gain is a dedicated page at Fungrim for each formula, thus better robustness, verification (#13), nice latex notation, possibly some references to books, etc.

fredrik-johansson commented 5 years ago

There is now a syntax for indefinite integral rules (see examples at the bottom of http://fungrim.org/topic/Natural_logarithm/), but it's not general enough to support replacement of an integral by another integral. I'm still thinking about the proper formalizations to use...