FranckQC commented on issue #10211: URL: https://github.com/apache/tvm/issues/10211#issuecomment-1057160549
Hi @yuanfz98 Thanks for your interest in the pass! That's great, I didn't know that there was an arith::Analyzer which was already able to algebraic simplifications of terms! When I worked on the CSE pass, I designed it with the idea that it should be easy to extend it for working with terms modulo some equations (by just replacing the EquivalentTerms() function as you did), but I though that we would have to write the normalization procedures on terms for doing that (which would simplify terms within an algebraic structure). And writing such normalization functions is quite a bit annoying to do (it implies deciding on some order terms, sorting them, etc). So I left it for a potential future work. I wasn't even sure that the efforts to implement such normalization procedures would be worth it, because I didn't know how often semantically equivalent computations appear in a TIR program. But as we already have this Simplify() method from arith::Analyzer that does simplification work, we can reuse it without even thinking about it. That's great! Too bad that arith::Analyzer can't deal with commutativity. I had a quick look at how RewriteSimplifier (which is used by Simplify()) is implemented, and it works by stating rewriting rules that could be applied. They are tried in the order in which they appear with the TVM_TRY_REWRITE() directive. So instead of computing a normal form in an algebraic structure as I described above, it seems that they try to apply rewriting rules (in a specific order), and they keep applying them, hoping that it will converge to the simplified term. I guess it often does some interesting simplifications, but it is not guaranteed to lead to the simplified term if it exists (unlike a normalization procedure simplifying a term in an algrebraic structure like a Monoid, a Group or a Ring). And without limiting the number of rewriting steps, it would not even be guaranteed to terminate. The reason why they can't define a commutativity rule is therefore likely because it would create infinite loops of rewriting: With the rule x+y --> y+x, the term a+b can be rewritten to b+a, which can again be rewritten to a+b, etc. Of course, we could limit the rewriting to a fixed number of steps (and they already do it : Simplify() calls the RewriteSimplifier a fixed amount of times, by default 2) to avoid the infinite rewriting, but then this rule for commutativity would be useless. In order to deal with commutativity, one really has to decide an order on subterms and to re-order terms using this order. In short, for rewriting rules that can be applied again and which lead back to the original term (i.e, A --> B --> A), this strategy of just stating rewrite rules by priority won't work unfortunately. I guess it's just a limitation of the approach they have used for implementing Simplify() (which was a very good idea for TVM, as they deal with much more than the axioms of algebraic structures!). Simplify() will do the amount of work that it can do and it will be better than nothing. Very well spotted @yuanfz98 ! -- This is an automated message from the Apache Git Service. To respond to the message, please log on to GitHub and use the URL above to go to the specific comment. To unsubscribe, e-mail: [email protected] For queries about this service, please contact Infrastructure at: [email protected]
