search

semantic-math / math-rules

Manipulate math-ast ASTs based on algebraic rules
MIT License
4 stars 1 forks source link

provide a way to `or` rules together #10

Open kevinbarabash opened 7 years ago

kevinbarabash commented 7 years ago

For instance, we'd like a single rule for a + 0 => a and 0 + a => a. It would be nice if there we could create a rule that would match either of these situations from simpler rules.

tkosan commented 7 years ago

In some CASs commutativity and associativity are built into the matcher, and in other CASs they are explicitly encoded in rewrite rules. In MathPiper they are encoded in rewrite rules.

kevinbarabash commented 7 years ago

@tkosan could you post an example of how MathPip encodes commutativity and associativity in its rewrite rules?

tkosan commented 7 years ago

@kevinbarabash here are MathPiper's rewrite rules for addition:

MathPiper's addition rewrite rules

There are a number of examples of commutatively in these rules. Associativity would be achieved by using parentheses in the head of a rule.

tkosan commented 7 years ago

@kevinbarabash here is an example of associativity being used: 

200 # (x_ / y_)/ z_ <-- x/(y*z);
230 # x_ / (y_ / z_) <-- (x*z)/y;