在 A note on A note on the algebra of CuTe Layouts 末尾遗留了一个问题, 就是:
In particular, I am trying to prove $M$ is left divisible by $N_{\varphi(\beta)} r_{\varphi(\beta)}$,
\[\begin{align} r_{\varphi(\beta)} &= M_0 M_1 \cdots M_{i - 1} c, i \lt \alpha, M_i = cK, K \in \mathbb{N} \\ \widehat{M'} &= \frac{M_i}{c} M_{i+1} \cdots M_{\alpha - 1} \infty \\ N_{\varphi(\beta)} &= \frac{M_i}{c} M_{i+1} \cdots M_{j - 1} c', j \lt \alpha \end{align}\]This means we need to prove $c’ \mid M_j$, but I can only prove $c’ \mid M_j \cdots M_{\alpha}$ based on $N_{\varphi(\beta)} r_{\varphi(\beta)} \mid M$.
在与 A note on the algebra of CuTe Layouts 作者邮件沟通之后:
It does seem like a mistake in the proof, thanks for pointing this out. Probably the simplest workaround is to change Definition 2.22 to in addition assume (ordinary) left divisibility for the shape modes $N_i$ as well, thus strengthening the admissibility hypothesis on the pair {S, B}. This is also a good argument for why CuTe always enforces this stronger hypothesis via static assert checks!
其实就是修改 Definition 2.12 admissible for composition 的定义:
Definition 2.12. Let $S = (M_0, \ldots, M_\alpha)$ be a shape tuple, let $M = M_0 \cdots M_\alpha$, and let $B = (N) : (r)$ be a layout of length 1. Then we say that the pair $\lbrace S, B \rbrace$ is admissible for composition (or simply admissible) if:
- $M$ is left divisible by $r$. Write $\widehat{M} = r \cdot \widehat{M}’$.
- With respect to its induced factorization, $\widehat{M}’$ is
weaklyleft divisible by $N$.
即去掉条件 2 的 weakly. 这也是 cute 当前代码实现:
auto layout_a = Layout<Shape<_4, _6, _8, _10>, Stride<_2, _3, _5, _7>>{};
auto layout_b = Layout<Shape<_6>, Stride<_12>>{};
// error: static assertion failed with "Static shape_div failure"
auto ld = composition(layout_a, layout_b);
std::cout << ld << std::endl;
现在让我们回过头再看下 Lemma 2.23, 略作补充.
- 求证 $\lbrace S, B_{\beta}’ \rbrace$ is admissible for composition.
证明: 如上所示, 我们已知 $M$ is left divisibility by $r_{\varphi(\beta)} N_{\varphi(\beta)}$, 此时 division index 是 $j$.
\[\begin{align} M_0 \cdots M_{j-1} c' &= r_{\varphi(\beta)} N_{\varphi(\beta)}, j \lt \alpha, c' \mid M_j \\ \widehat{M'} &= \frac{M_j}{c} M_{j+1} \cdots M_{\alpha - 1} \infty \end{align}\]现在证明 $\widehat{M’}$ is left divisibility by $\frac{M}{r_{\varphi(\beta)} N_{\varphi(\beta)}}$. 此时:
\[\frac{M}{r_{\varphi(\beta)} N_{\varphi(\beta)}} = \frac{M_j}{c} M_{j+1} \cdots M_{\alpha - 1} M_{\alpha}\]此时容易观察到 $\widehat{M’}$ is left divisibility by $\frac{M}{r_{\varphi(\beta)} N_{\varphi(\beta)}}$ 且 division index $j’ = \alpha$. (不好, 我的符号快不够用了…
- 求证 $\lbrace S, B_{1}’ \rbrace$ is admissible for composition.
证明: 已知 $M_0 \cdots M_{i-1} c = r_{\varphi(0)}$, 若 $i = \alpha$, 则结论易证. 现在考虑 $i \lt \alpha$, 此时:
\[\begin{align} \widehat{M'} &= \frac{M_i}{c} M_{i+1} \cdots M_{\alpha - 1} \infty \\ N_{\varphi(0)} &= \frac{M_i}{c} M_{i+1} \cdots M_{j-1} c' \end{align}\]若 $j = \alpha$ 则结论易得. 现在考虑 $j \lt \alpha$, 易得 $M$ is left divisibility by $N_{\varphi(0)} r_{\varphi(0)}$ 且 division index 为 j, 此时:
\[\begin{align} \widehat{M'} &= \frac{M_j}{c'} M_{j+1} \cdots M_{\alpha - 1} \infty \\ N_{\varphi(0)} r_{\varphi(0)} &= M_0 \cdots M_{j-1} c' \\ r_{\varphi(1)} &= M_0 \cdots M_{i_1 - 1} c_1 \\ \end{align}\]由于 $N_{\varphi(0)} r_{\varphi(0)} \mid r_{\varphi(1)}$ 易得 $i_1 \ge j$, 考虑 $i_1 = j$, 此时 $c_1 \mid M_{j}, \frac{r_{\varphi(1)}}{N_{\varphi(0)} r_{\varphi(0)}} = \frac{c_1}{c’}$, 容易观察到 $\widehat{M’}$ is left divisibility by $\frac{c_1}{c’}$, 且 division index = 1, 易证 $\frac{c_1}{c’} \mid \frac{M_j}{c’}, \frac{c_1}{c’} \frac{M_j}{c_1} = \frac{M_j}{c’}$.
考虑 $i_1 \gt j$, 此时:
\[\frac{r_{\varphi(1)}}{N_{\varphi(0)} r_{\varphi(0)}} = \frac{M_j}{c'} M_{j+1} \cdots M_{i_1 - 1} c_1\]容易观察到结论成立.
- Now by Proposition 2.7, we see that the additional disjointness assumption is satisfied.
解: 如下所示:
\[C' = \left( d_0, N_0, \frac{d_1}{N_0 d_0}, N_1, \frac{d_2}{N_1 d_1}, \ldots, N_\alpha, \frac{M}{N_\alpha d_\alpha} \right) : \left( 1, d_0, N_0 d_0, d_1, N_1 d_1, \ldots, d_\alpha, N_\alpha d_\alpha \right)\]很容易观察到 interval of definitio 分别是:
\[[1, d_0 - 1], [d_0, (N_0 - 1) d_0], [N_0 d_0, d_1 - N_0 d_0], [d_1, (N_1 - 1) d_1], \cdots\]互不相交.
