@@ -26,15 +26,16 @@ In addition, the following must be defined for a `Weight`:
2626* ` Hash ` : maps weight to ` size_t ` .
2727* ` ApproxEqual ` : approximate equality (for inexact weights)
2828* ` Quantize ` : quantizes wrt delta (for inexact weights)
29- * ` Divide ` : $\forall a,b,c$ s.t. $\text{Times}(a, b) = c \Rightarrow b' =
30- \text{Divide}(c, a, \mathtt{DIVIDE\_ LEFT})$ if a left semiring,
31- $b'.\text{Member}()$ and $\text{Times}(a, b') = c \Rightarrow a' =
32- \text{Divide}(c, b, \mathtt{DIVIDE\_ RIGHT})$ if a right semiring and
33- $a'.\text{Member}()$ and $\text{Times}(a', b) = c \Rightarrow b' =
34- \text{Divide}(c, a) = \text{Divide}(c, a, \mathtt{DIVIDE\_ ANY}) =
35- \text{Divide}(c, a, \mathtt{DIVIDE\_ LEFT}) = \text{Divide}(c, a,
36- \mathtt{DIVIDE\_ RIGHT})$ if a commutative semiring, $b'.\text{Member}()$
37- and $\text{Times}(a, b') = \text{Times}(b', a) = c$
29+ * ` Divide ` : $\forall a,b,c$ s.t.
30+ * * Left semiring* : $\text{Times}(a, b) = c \Rightarrow b' =
31+ \text{Divide}(c, a, \mathtt{DIVIDE\_ LEFT})$, $b'.\text{Member}()$
32+ * * Right semiring* : $\text{Times}(a, b') = c \Rightarrow a' =
33+ \text{Divide}(c, b, \mathtt{DIVIDE\_ RIGHT})$, $a'.\text{Member}()$
34+ * * Commutative semiring* : $\text{Times}(a', b) = c \Rightarrow b' =
35+ \text{Divide}(c, a) = \text{Divide}(c, a, \mathtt{DIVIDE\_ ANY}) =
36+ \text{Divide}(c, a, \mathtt{DIVIDE\_ LEFT}) = \text{Divide}(c, a,
37+ \mathtt{DIVIDE\_ RIGHT})$, $\text{Times}(a,b') = \text{Times}(b', a) =
38+ c$.
3839* ` ReverseWeight ` : the type of the corresponding reverse weight. Typically the
3940 same type as ` Weight ` for a (both left and right) semiring. For the left
4041 string semiring, it is the right string semiring.
0 commit comments