Proofs: Kannan-Bachem algorithm

The row-insertion Kannan-Bachem algorithm returns the Hermite normal form full

This proof shows: correctness, termination.

Let $A$ be an $m \times n$ integer matrix with rows $a_1, \dots, a_m$. For a list of integer vectors $S$, let $L(S)$ be the lattice of their integer combinations. For a nonzero vector $w$, $\operatorname{lead}(w)$ is the index of its first nonzero entry among the first $n$ entries. As in the implementation, every row carries $m$ extra entries, so the algorithm works on the rows of $[A \mid I_m]$; all statements about "$H$" refer to the first $n$ entries, and $\operatorname{lead}$ ignores the extra ones.

A list of nonzero rows $h_1, \dots, h_s$ with $c_k = \operatorname{lead}(h_k)$ is in Hermite form if $c_1 < c_2 < \cdots < c_s$, $h_k[c_k] > 0$ for all $k$, and $0 \le h_l[c_k] < h_k[c_k]$ for all $l < k$.

Claim. KANNAN-BACHEM$(A)$ stops, and returns $H$ and $U$ with $U$ unimodular, $UA = H$, and $H$ the Hermite normal form of $A$: its nonzero rows are in Hermite form, they are followed by zero rows, and their number is the rank of $A$.

Termination. The loop of line L2 has $m$ steps. In each, the loop of line L4 has at most $s$ steps, where $s \le m$ is the number of stored rows, and the loops of lines L11 and L12 have at most $s^2$ steps.

Unimodular steps. Every change to the rows of $[A \mid I_m]$ is one of the following, each of which is an invertible integer row operation whose inverse is also integral:

• Line L8 replaces the pair $(h, w)$ with $(x h + y w,\ (h_c / g)\, w - (w_c / g)\, h)$, where $h_c = h[c]$, $w_c = w[c]$ and $g = x h_c + y w_c = \gcd(h_c, w_c) > 0$. Its matrix $\begin{pmatrix} x & y \\ -w_c/g & h_c/g \end{pmatrix}$ has integer entries and determinant $(x h_c + y w_c)/g = 1$.
• Line L10 negates a row (determinant $-1$).
• Line L13 subtracts an integer multiple of one row from another (determinant $1$).

The stored rows, the rows set aside as zero, and the rows not yet inserted are always the rows of $V [A \mid I_m]$ for a unimodular $V$, up to their order. At the end, $U$ lists the extra parts of the rows in the output order, and the first $n$ entries give $H$, so $H = UA$ and $U$ is unimodular (a permutation of the rows of $V$). In particular $L(H) = L(A)$.

Invariant. Before step $t$ of line L2, the stored rows $h_1, \dots, h_s$ are in Hermite form and $L(h_1, \dots, h_s) = L(a_1, \dots, a_{t-1})$.

Before step $1$ there are no stored rows. Assume the invariant before step $t$, and let $w = a_t$.

The loop of line L4. We show that at the start of the iteration with index $k$, (i) $\operatorname{lead}(w) > c_{k-1}$ if $w \ne 0$ and $k > 1$, (ii) the rows $h_1, \dots, h_{k-1}$ have leading columns $c_1 < \cdots < c_{k-1}$ with positive leading entries, and (iii) the rows $h_k, \dots, h_s$ are unchanged. This holds for $k = 1$. If line L5 breaks, nothing changes. If $\operatorname{lead}(w) > c_k$, the iteration changes nothing and (i) holds for $k + 1$. If $\operatorname{lead}(w) = c_k = c$, then $h_k$ and $w$ are both zero in the columns before $c$, so the new rows of line L8 are also zero there. The new $h_k$ has $h_k[c] = x h_c + y w_c = g > 0$, so its leading column is still $c_k$ with a positive entry. The new $w$ has $w[c] = (h_c w_c - w_c h_c)/g = 0$, so it is zero or has $\operatorname{lead}(w) > c_k$.

Insertion. When the loop ends at index $k$ (by the break, or with $k = s + 1$), either $w = 0$, or $c_{k-1} < \operatorname{lead}(w)$ and, if $k \le s$, $\operatorname{lead}(w) < c_k$: the break happens at the first $k$ with $\operatorname{lead}(w) < c_k$, and $\operatorname{lead}(w) \ne c_j$ for all $j$ since an equality would have led to a gcd step. If $w \ne 0$, line L10 makes its leading entry positive and inserts it at position $k$. In both cases the stored rows now have strictly increasing leading columns and positive leading entries, and they span $L(a_1, \dots, a_t)$, since the unimodular steps preserve the lattice spanned by the stored rows together with $w$, and a zero $w$ adds nothing.

Reduction. Renumber the stored rows $h_1, \dots, h_s$ with pivots $p_k = h_k[c_k] > 0$. Lines L11 to L13 treat $l = s - 1, \dots, 1$. For fixed $l$ and $k$, line L13 sets $h_l \leftarrow h_l - \lfloor h_l[c_k] / p_k \rfloor h_k$, which gives $0 \le h_l[c_k] < p_k$. Since $h_k$ is zero in the columns before $c_k$, this changes $h_l$ only in the columns $c_k$ and later, so it does not undo the reductions at $c_{l+1}, \dots, c_{k-1}$, which were done earlier for this $l$, and it does not change the leading entry of $h_l$, since $c_l < c_k$. It does not change any row other than $h_l$, so the rows $h_{l+1}, \dots, h_s$ treated before stay reduced. After the loop, $0 \le h_l[c_k] < p_k$ for all $l < k$, so the stored rows are in Hermite form. The steps are unimodular, so the lattice is still $L(a_1, \dots, a_t)$. This proves the invariant for $t + 1$.

End. After step $m$, the stored rows $h_1, \dots, h_s$ are in Hermite form and span $L(A)$. Rows in echelon form with nonzero leading entries are linearly independent, so $s = \dim_{\mathbb{Q}} \mathbb{Q} L(A) = \operatorname{rank} A$. Every zero $w$ was set aside, which gives the $m - s$ zero rows at the bottom of $H$. A matrix whose nonzero rows are in Hermite form and whose zero rows come last is, by definition, in Hermite normal form, and it is the Hermite normal form of $A$ because $H = UA$ with $U$ unimodular. By the uniqueness theorem for the Hermite normal form, it does not depend on the order of the steps. $\blacksquare$

Remark (sizes). The invariant says that after each insertion the stored rows are the Hermite normal form of $a_1, \dots, a_t$. If the entries of $A$ are at most $B \ge 1$ in absolute value and $a_1, \dots, a_t$ have rank $r_t$, every entry of that form is at most $r_t \cdot r_t^{r_t/2} B^{r_t}$. Indeed, let $P$ be the pivot columns and $A_S$ a set of $r_t$ independent rows among $a_1, \dots, a_t$; the $r_t \times r_t$ block $A_S[P]$ is nonsingular, with determinant $d$. Each pivot is at most $\prod_k p_k$, which divides $d$, since $L(A_S) \subseteq L(H)$. Each entry of the form in a column $j$ is $\sum_k h[c_k]\, z_{kj}$, where $z_{kj} = \det A_S[P, k \to j] / d$ by Cramer's rule, so it is at most $\sum_k p_k |\det A_S[P, k \to j]| / |d| \le r_t \cdot r_t^{r_t/2} B^{r_t}$ by the Hadamard bound. During one insertion, line L8 combines $w$ with a row $h_k$ of the previous form, not yet changed by (iii), and line L13 combines $h_l$ with a row $h_k$, $k > l$, that is already a row of the new form, since the reduction goes from the bottom up. With the Euclidean cofactors $|x| \le |w_c|/g$ and $|y| \le |h_c|/g$, each such step multiplies the largest absolute value of the changed row by at most $2S + 1$, where $S$ is the bound above. So the lengths of the numbers in the first $n$ entries grow by $O(\log S)$ per step, with $O(s^2)$ steps per insertion, and stay polynomial in $m$, $n$ and the length of $B$. The tests check the bound on the final form. The argument does not bound the extra entries, the transform $U$, when $A$ has dependent rows; for a nonsingular square $A$, $U = H A^{-1}$ is unique and bounded by Cramer's rule.