Are commutative versions of rewrite rules necessary?
eg x*0 == 0*x == x
Constant arguments are moved to the RHS by const_prop.isle
Is it just an optimisation?
ah for constants it is not necessary to have rules for both, because we do move constants to the right hand side
for non-constants, it is currently necessary to write both rules
we want to eventually be able to mark certain things as commutative in ISLE, so that the compiler essentially macro-expands the commutativity for us, but that requires quite a bit of design and we haven't spent time on it yet
Yup, and to give a little more context in case it helps, another alternative might be to have a generic commutativity rule that creates both forms of every commutative operator in the egraph, to maximize possible rule applications; but we made a conscious tradeoff not to do this because it would significantly increase the size of the egraph and rule application cost
in contrast, duplicating rules when needed is relatively low-cost, because the ISLE compiler can merge them and run them all in sublinear cost
Both sound very interesting
I wonder if it would be possible to generate rewrite rules just by listing an opcodes properties (eg associative, commutative, neutral element, absorbing element)
that's kind of along the lines of what we're thinking with commutativity in particular: marking a term with type (Value Value) Value
as commutative and then using it on the LHS should automatically expand into two LHSes (or an or-pattern)
which is kind of the moral equivalent of fusing/composing with a general commutativity rule
Maybe ISLE needs a macro system :cold_sweat:
Oh no! This is the part of the conversation where I run away screaming :-)
fwiw, I've tried to "hold the line" on complexity in the language, because I think we get benefits from simplicity in terms of analyzability, verifiability, ability to have a coherent mental model and understand bugs, etc. It's easy to argue for expressivity from the PoV of the backend author but it carries hidden costs. I'd be worried if we ever gained either generics/polymorphism or a macro system, and so far we've gotten along without them
(this may be a little bit unfashionable, and can also lead to ignorance of true benefits a la Golang's eventual adoption of generics, but we are a DSL and can afford different tradeoffs, and also it seems problems that initially call for big hammers can often be solved in different ways after some thought)
Good point on the expressiveness vs analyzability tradeoff
Maybe having a few predefined properties that could be attached to an operator would get 80% of the benefit with 10% of the effort
eg semigroup, monoid, group
kmeakin has marked this topic as resolved.
kmeakin has marked this topic as unresolved.
What about marking instructions as commutative, rather than rewrite rules?
ie when generating extractors for commutative instructions, generate an extractor that matches both versions:
(decl bor (Type Value Value) Value)
(extractor
(bor ty x y)
(or
(inst_data ty (InstructionData.Binary (Opcode.Bor) (value_array_2 x y)))
(inst_data ty (InstructionData.Binary (Opcode.Bor) (value_array_2 y x))))
)
So, IIUC, the egraph would not be bloated
That's more-or-less the consequence of what is proposed above ("marking a term with type (Value Value) Value
as commutative"): the idea is that we'd put a flag on the decl
, and then any use of the term in the LHS of a rule would turn into what you describe
Chris Fallin said:
That's more-or-less the consequence of what is proposed above ("marking a term with type
(Value Value) Value
as commutative"): the idea is that we'd put a flag on thedecl
, and then any use of the term in the LHS of a rule would turn into what you describe
Oh I see, I thought you were referring to rewrite rules, not constructors
Last updated: Dec 23 2024 at 12:05 UTC