Add inversion from weighted#655
Conversation
* add monoid module * clean up * fix doctest * fix * wip * remove incorrect rule * add disjoint set tests and fix bug * lint * drop jax monoid defs * drop incorrect comment * add assert * reduce nondeterminism and add assertions * fix inconsistent stream numbering and missing constant factors
| ) | ||
|
|
||
|
|
||
| def match_reduce(term: Term) -> tuple | None: |
There was a problem hiding this comment.
This is a very strange function. Surely there's a more comprehensible way to write this, even if it ends up being more verbose.
There was a problem hiding this comment.
Agreed. Unfortunately, I'm not sure how to write this in a way that doesn't enumerate operations. The subclassing relation between operations is implicit, and we want to match all subclasses (and leave open the possibility that new ones could be created).
|
|
||
| More specifically, this transform implements the identity | ||
| reduce(⨁, reduce(⨂, body2, {vv: v()}), {v: reduce(×, body1, S1)} ∪ S2) | ||
| = reduce(⨁, reduce(⨂, reduce(⨁, body2, {vv: v()}), S1), S2) |
There was a problem hiding this comment.
This equation is quite hard to parse and appears to be wrong (what binds v on the RHS?). Is it out of date wrt what is now happening in the rule?
There was a problem hiding this comment.
It should read:
reduce(⨁, reduce(⨂, body2, {vv: v()}), {v: reduce(×, body1, S1)} ∪ S2)
= reduce(⨁, reduce(⨂, reduce(⨁, body2, {vv: body1}), S1), S2)
|
Note: the mapping of |
jfeser
force-pushed
the
jf-weighted-lifting
branch
from
0daf135 to
1d38f0d
Compare
2 participants
Depends on #653