[Someone]

For Simplify, I expect its a black, or at least gray box to Mathematica maintainers, too.

It will have simple rules such as constant folding, “replace x - x by zero”, “replace zero times something with the conditions under which ‘something’ has a value”, etc, lots of more complex but still easy to understand rules with conditionals such as “√x² = |x| if x is real”, and some weird logic that decides the order in which to try simplification rules.

There’s an analogy with compilers. In LLVM, most optimization passes are easy to understand, but if you look at the set of default optimization passes, there’s no clear reason for why it looks like it looks, other than “in our tests, that’s what performed best in a reasonable time frame”.

[kccqzy]

A lot of problems look like this. A while ago I was working on a calendar event optimization (think optimizing “every Monday from Jan 1, 2026 to March 10, 2026” + “every Monday from March 15, 2026 to March 31, 2026” to simply “every Monday from Jan 1, 2026 to March 31, 2026”). I wrote a number of intuitive and simple optimization passes as well as some unit tests. To my horror, some passes need to be repeated twice in different parts of the pipeline to get the tests to pass.

[AlotOfReading]

You can simplify most of those problems by writing the constraints down in conjunctive/disjunctive normal forms and applying standard simplification on them, like you're back in school. That also eliminates things like repetition, since doing so also makes the problem declarative. If you need the recursive loops, you're guaranteed to be to stratify them for any reasonable problem. If you wanted, you could solve the problem optimally from this point by finding the prime implicants, or just accept a suboptimal solution that runs faster than you have any reason to care about, like datalog and sql do.

That doesn't work in general for mathematica because it's too powerful.

[LegionMammal978]

Even for boolean logic problems, a minimum-size CNF or DNF will not necessarily be the cheapest solution in terms of gates. As far as I know, hardly anyone has even attempted automatic minimization in terms of general binary operators.

[AlotOfReading]

That's true, it'll just be the minimal solution in SOP. I'm willing to call that good enough. My experience is that in practice you're often better off just relying on the fact that modern computers can execute billions of them per second.

[evanb]

As a term-rewriting system the rule x-x=0 presumably won’t be in Simplify, it’ll be inside - (or Plus, actually). Instead I’d expect there to be strategies. Pick a strategy using a heuristic, push evaluation as far as it’ll go, pick a strategy, etc. But a lot of the work will be normal evaluation, not Simplify-specific.