How to write conditional rules

[vitrun]

When trying to define rule:tan(x-y) -> (tan(x)-tan(y))/(1+tan(x)*tan(y))，with x (and y) not equal to pi/2 + k*pi (k = 1, 2, 3...). I found:

1. It is hard to write the Conditional Applier. It not that easy to describe the pattern of pi/2 + k*pi.
2. The correctness of the rule depends on its applying order. Consider tan(197*pi/394 - y),197*pi/394 must to be simplified before the mentioned rule is applied, . However, as I know, in egraph, the rules can be applied in any order.

Is there some way to achieve this, or do I misunderstand something?

[mwillsey]

You are correct that this is a difficult rule to write correctly. In general, the e-graph is building up a monotonically increasing equivalence relation. That is, if x = y right now, it can say so, but if x != y right now, then they may still become equal in the future! So it's impossible to say whether or not two things are provable unequal in general while equality saturation is running. You can, however, use domain knowledge to do this. A simple example is checking if something is zero. You cannot really say that x != 0, but if you later learn that x = 2, then you can proceed because you know there is no way to learn that 2 = 0. So your condition will have to be conservative in that way: waiting for x or y to take on a form that you know can never be equal to pi/2 + k*pi.

[vitrun]

Thanks for your reply. I agree that we have to be conservative. However, I wonder how to do this:

waiting for x or y to take on a form that you know can never be equal to pi/2 + k*pi

In general, x or y can be arbitrarily complex. Since we have to prove not even one this kind of form exists, we have to wait for the moment it wont take on any new forms, which means the sub-egraph x or y is saturated, right? However, it's not easy to tell whether an egraph is saturable. Though possible, it is not natural to realize using egg up to my knowledge. Is egraph analysis a suitable tool? Every time a new term is added to the eclass, its form is checked and result remembered. It may be tedious to write analysis for every condition though. By using domain knowledge, do you suggest using some external utils to prove it?

[pavpanchekha]

In general you'd do this with some kind of e-class analysis, not by checking saturation, but you're right that this is tricky to do in general. It's worth looking at what expressions you actually see in practice; perhaps in all practical cases, say, x and y are constants or linear expressions, in which case it's pretty to easy to track their values.

[vitrun]

Hi, @pavpanchekha
What I'm trying to do is using e-graph to simplify mathematical expressions. A practical case is tan(π/2-x), Let's consider following two rules:

• tan(π/2 - α) -> cot(α)
• tan(α - β) -> (tan(α) - tan(β)) / (1 + tan(α)tan(β))

Obviously, the first rule should be applied, and the second should not. To achieve that, I need to guard α and β against the form of π/2 + k*π. It may be easy when α is a constant, e.g, 2. However, When it comes to complex expressions such as(25/19+7/38)*π, things become tricky. Inspired by @mwillsey , I think we need to be able to tell whether α and β would take on any new forms or not. Here is what I'm trying to do:

• In an analysis, last updated iteration of the e-class is recorded
• Add some condition for the second rule: if the last updated iteration is smaller than current iteration, meaning no new forms of α are added, then it's the time to search this e-class for pattern π/2 + k*π and decide if the rule can be applied.

The problems are:

• We can not rule out the possibilities that new forms will keep coming up. It seems quite like telling the saturability of this small e-graph.
• Can I count on last updated iteration? if in iteration n, no expressions are inserted or merged into the e-class, in iteration n+1 or later iterations, will there be new expressions again?

Any comments, or the other way around?

[pavpanchekha]

You're still trying to find a way to detect saturation and then search the e-class for a pattern. In general this won't work because it's hard to detect saturation. Instead of trying to detect when it's safe to say x doesn't match pattern p, try to find a different pattern p', so that if x matches p' then it definitely doesn't match p. For example, perhaps in your semantics x is not considered to be have the form pi/2 + k * pi (of course it may have that form for some values of x, but for other values of x it won't, and maybe this is what you mean by equality). Then if you have the expression tan(x - y) you can prove both the left and right hand don't have the bad form and you can move on with the rewrite.