Simplification plan

[shashi]

I've been trying to make the symbolic simplifier (currenlty simply_constants) worth using.

I attempted to write a type (that itself behaves like an Expression) that simplifies linear combinations of Expressions. It turns out that Rewrite does it very similarly. I think there's value in using Rewrite instead to do it: it will not only work for LinearCombination type of terms, but a lot of other cases as well.

My assessment has lead me to make this plan that I'm willing to implement. Note that many of these features existed in Simplify.jl, but weren't using Rewrite.jl to implement them. @HarrisonGrodin probably intended to do these same things:

I'm going to use the word Term below to mean ModelingToolkit.Expression and/or Rewrite.AbstractTerm. I think they should all be represented with the same type, which is a detail I intend to take care of.

1. Make Variables maintain their domain: this is at least a type such as Number or an AbstractArray{Number}, this can be tedious to define, so I propose all @variable defs are Numbers by default, but we can optionally allow users to specify other domains. I say at least a type because it might well be SpecialSets of values
2. Make Variables also maintain a list of properties. This is extra information useful for transformations such as Square, Hermitian, Orthonormal.
   So the @variables syntax could be:

• @variables x y z[1:10] (behaves as it does now, but also designates each variable as a Number).
• @variables type=AbstractMatrix{<:Number} A B C[1:10]
• @variables type=AbstractMatrix{<:Number} props=[Orthonormal] Q[1:10] Defines 10 orthonormal matrix variables. One might even make this simpler by assuming: @variables props=[Orthonormal] Q[1:10] means Q is a AbstractMatrix of numbers by default.

3. For every f we care about (e.g. nice mathematical functions) define
   f(a::Term, b::Term) = term(termtype(f, a, b), f, a, b; props=promote_props(f,a,b)) (and the methods that work with generic as and bs.).

• termtype(f, a, b) allows us to decide what kind of rules apply when simplifying f(a,b) for example, termtype(*, a, b) would return ACTerm() if the domain of a and b are numbers, but will generally return ATerm() (btw @HarrisonGrodin ATerm doesn't yet exist?). By default it returns FreeTerm() so we only need to define this on + and * to get an amazing simplifier in comparison to the status quo.
• promote_props(f,a,b): Defines properties of the resultant term. E.g. Q1 + Q2 is hermitian if Q1 and Q2 are too (note that the props stuff is optional at all times.)

4. Rule definition enhancements: I would like to propose an extended syntax for better flexibility than what Rewrite currently provides:

@rules RuleSet begin
    :x + :z => iszero(z) => x
    :A * :A' => hasprop(A, Orthonormal) => I
end

I am asking that it be allowed to 1) distinguish between exact matches e.g. the symbols + and *, and ' in the examples, v.s. variable matches e.g. :A ``:x and :z, 2) an additional custom predicate initial match pattern in the rule definition syntax. We can compile this to maximally efficient functions much like Rewrite does right now.

This is going to be the first, surface level phase of simplifier. Another level of simplification would involve writing expressions as polynomials of made up variables (for terms that cannot be simplified) and then performing polynomial GCD to coerce it into various useful forms: (e.g. reduce number of flops). That's a problem for another day.

cc @YingboMa @MasonProtter @HarrisonGrodin @dpsanders @ChrisRackauckas

[MasonProtter]

So a couple random thoughts:

1. If you want your symbolic variables to have types, then the expressions containing them also should be typed. For instance, if you have @variable x::Number then Term(sin, x) should also be typed, i.e. Term{Number}(sin, x). This makes for a ton of additional work. If you want your variables to be abstractly typed, you can't use julia's type inference:

julia> Core.Compiler.return_type(sin, Tuple{Number})
Any

so you'll have to essentially roll your own type system. The simplification rule systems will also need to be made to know about types which is a lot of added complexity.

2. Before Rewrite.jl is ready for this, it needs a way to have terms contain foreign, non-symbolic objects. For instance, you cannot currently have a Term 1 + x, unless you define 1 symbolically in terms of the successor function or something. I think it needs a type AtomicTerm which can store data that wasn't defined in Rewrite.jl.

Neither of these points should necessarily discourage this line of development, but I just wanted to clarify that there's a lot of missing machinery to do this.

[shashi]

so you'll have to essentially roll your own type system

The rules (by way of something like promote_domain) are not hard to define on all the functions listed by DiffRules.rules() for example (can be done in a for loop)! So it will work as well as ForwardDiff for example. And having an Any will just result in a free theory -- this doesn't change the meaning of the expression, only affects what simplifications apply.

I think it needs a type AtomicTerm which can store data that wasn't defined in Rewrite.jl.

Yeah, I'm working on that.

[shashi]

Rewrite is currently written to manipulate Julia AST. It deals with symbols without care for the current scope and namespacing.

In MTK we want to represent expression trees as concrete values that have properties like domains by virtue of how they're constructed.

I wish Rewrite would just work on any type that has a head and children defined on it.

[dpsanders]

Closed because it has been done?

[ChrisRackauckas]

#326

[dpsanders]

Fantastic!