Open
Description
Depends on #59
In #59, unification of multiplicity polynomials is done syntactically (in particular (p + q) + r will not unify with p + (q + r)). This won't be comfortable in the long run, so we need to add some domain-specific knowledge to multiplicity unification.
The goal is to have unification up to all semiring laws, or at least a sufficient approximation. In particular q*(p + (1*r + s)) should unify with (q*p +q*r) + q*s. In AC unification, the hard part is splitting:
p + q unifies with a+b+c in one of two ways: either p = x+y and q=z or p=x and q=y+z (for x,y,z any permutation of a,b,c).
We may choose to be imprecise with regard to splitting to make implementation easier. This is yet to be decided.
Metadata
Metadata
Assignees
Labels
No labels