Proofs: Knuth-Plass line breaking algorithm

Knuth-Plass returns a paragraph of least total demerits full

This proof shows: correctness, termination.

We use the definitions and the pseudocode of the page. The items are $x_0, \ldots, x_{m-1}$, all widths are $\ge 0$, every glue has $0 \le z \le w$, and $x_{m-1}$ is a forced penalty. A break sequence to $b$ is a sequence of legal breaks $b_1 < \cdots < b_k = b$ that contains every forced break $< b$. Put $b_0 = -1$. It is feasible if each line $(b_{t-1}, b_t)$ is feasible. Its class is the class of its last line, and the class of the empty sequence ($b = -1$) is decent. Its demerits are the sum of the demerits of its lines, where line $t$ uses the class of line $t - 1$ and whether $b_{t-1}$ is a flagged penalty. For a legal break $b$ and a class $c$, let $\mathrm{OPT}(b, c)$ be the least demerits of a feasible break sequence to $b$ of class $c$, or $\infty$ if there is none. Let $\mathrm{OPT}(-1, \text{decent}) = 0$.

Lemma 1 (the demerits split). Let $\sigma$ be a feasible break sequence to $b$ with last line $(a, b)$, and let $\sigma'$ be its prefix to $a$, of class $c'$. The demerits of $\sigma$ are those of $\sigma'$ plus $\delta(a, b, c')$, where $\delta(a, b, c')$ is the demerits of the line $(a, b)$ after a line of class $c'$. This value depends only on $a$, $b$ and $c'$.

Proof. The measures $L_{ab}$, $Y_{ab}$ and $Z_{ab}$ depend only on the items between $a$ and $b$, so $r$, the badness, the class and the penalty term depend only on $a$ and $b$. The term $\alpha$ depends on whether $x_a$ and $x_b$ are flagged penalties, and the term $\gamma$ on the class of $(a, b)$ and on $c'$. $\square$

Lemma 2 (optimal prefix). If $\mathrm{OPT}(b, c) < \infty$, then $\mathrm{OPT}(b, c) = \min \bigl( \mathrm{OPT}(a, c') + \delta(a, b, c') \bigr)$ over all $a < b$ and classes $c'$ such that $\mathrm{OPT}(a, c') < \infty$, the line $(a, b)$ is feasible with class $c$, and no forced break lies strictly between $a$ and $b$. If no such pair exists, $\mathrm{OPT}(b, c) = \infty$.

Proof. Each such pair gives a feasible break sequence to $b$ of class $c$: take an optimal sequence to $a$ of class $c'$ and add $b$. It contains every forced break $< b$, because those $\le a$ are in the prefix and none lies strictly between $a$ and $b$. By Lemma 1 its demerits are $\mathrm{OPT}(a, c') + \delta(a, b, c')$. So the minimum is $\ge \mathrm{OPT}(b, c)$. Conversely, an optimal sequence to $b$ of class $c$ has a last line $(a, b)$, feasible with class $c$, with no forced break strictly between $a$ and $b$, and its prefix is a feasible sequence to $a$ of some class $c'$ with demerits $\ge \mathrm{OPT}(a, c')$. By Lemma 1, $\mathrm{OPT}(b, c) \ge \mathrm{OPT}(a, c') + \delta(a, b, c')$. $\square$

Lemma 3 (pruning is safe). Let $M(a, b)$ be the width at full shrink of the line $(a, b)$ without the item $x_b$, as in line L10. If $a < b < b'$, then $M(a, b') \ge M(a, b)$. If $M(a, b) > L$, then no line $(a, b')$ with $b' \ge b$ is feasible.

Proof. The line $(a, b')$ contains the items of the line $(a, b)$, plus possibly $x_b$ and later items, and the dropped items after $a$ are the same, except that if the first kept item after $a$ is beyond $b$, the line $(a, b)$ is empty and $M(a, b) = 0$. Each box adds its width $\ge 0$ to $M$, each glue adds $w - z \ge 0$, and each penalty adds 0, so $M(a, b') \ge M(a, b)$. Now let $M(a, b) > L$ and $b' \ge b$. The natural width minus the shrink of the line $(a, b')$ is $M(a, b')$ plus the width of $x_{b'}$ if it is a penalty, so it is $\ge M(a, b') > L$. If the shrink $Z$ is positive, then $L_{ab'} - Z > L$ gives $r = (L - L_{ab'}) / Z < -1$. If $Z = 0$, then $L_{ab'} > L$ and $r = -\infty$. Either way the line is not feasible. $\square$

Lemma 4 (invariant). When line L5 starts for a legal break $b$, the active list holds, for each pair $(a, c')$ with $a < b$, $\mathrm{OPT}(a, c') < \infty$, no forced break strictly between $a$ and $b$, and the line $(a, b)$ feasible, a node $(a, c')$ with $D = \mathrm{OPT}(a, c')$. Every node $(a, c')$ in the list has $D = \mathrm{OPT}(a, c')$ and a chain of links that spells a feasible break sequence to $a$ of class $c'$ with demerits $D$. Moreover, after line L12 for $b$, there is a node $(b, c)$ exactly for the classes with $\mathrm{OPT}(b, c) < \infty$.

Proof. By induction on $b$ over the legal breaks. Nodes enter the list only at line L1 and line L12, and leave it only at line L11.

Values and chains. The start node has $D = 0 = \mathrm{OPT}(-1, \text{decent})$ and an empty chain. A node $(b, c)$ is made at line L12 from a pair $(d, a)$ stored at line L9, with $d = D(a) + \delta(a, b, c')$ for a node $a$ of class $c'$ such that the line $(a, b)$ is feasible of class $c$. The node $a$ was in the list at $b$, so no forced break lies strictly between $a$ and $b$ (a forced break clears the list at line L10 after its own nodes are compared). By induction the chain of $a$ is a feasible sequence to $a$ with demerits $D(a)$, so the chain of the new node is a feasible sequence to $b$ of class $c$ with demerits $d$ (Lemma 1). Hence $d \ge \mathrm{OPT}(b, c)$.

Membership. Take $(a, c')$ as in the first statement. Since $\mathrm{OPT}(a, c') < \infty$, the node $(a, c')$ was created when $a$ was processed, by the last statement for $a$ (or it is the start node). At each legal break $b''$ with $a < b'' < b$, line L10 kept it: $x_{b''}$ is not forced, since no forced break lies strictly between $a$ and $b$, and $M(a, b'') \le L$, since otherwise Lemma 3 would make the line $(a, b)$ infeasible.

The minimum. At $b$, lines L5 to L9 examine all nodes in the list. By membership, every pair of Lemma 2 is examined with its exact value, and every examined node gives a real sequence. So $\min$ over the stored values for class $c$ equals $\mathrm{OPT}(b, c)$ by Lemma 2, and $best[c]$ is none exactly when $\mathrm{OPT}(b, c) = \infty$. Line L12 creates the node $(b, c)$ with $D = \mathrm{OPT}(b, c)$ for these classes. $\square$

Theorem. The algorithm terminates. If some feasible paragraph exists, it returns one with the least total demerits; otherwise it reports failure.

Proof. Termination: the loop of line L2 runs $m$ times, each pass looks at a finite list, and line L14 follows links to strictly smaller positions until $-1$. A paragraph is a break sequence to $m - 1$, and $x_{m-1}$ is a legal break. By Lemma 4, after line L12 for $b = m - 1$ the nodes at $m - 1$ are exactly the classes with $\mathrm{OPT}(m - 1, c) < \infty$, with $D = \mathrm{OPT}(m - 1, c)$. They are not removed afterwards, since the loop ends. If there are none, no feasible paragraph exists and line L13 reports failure. Otherwise line L14 takes the least $D$, which is $\min_c \mathrm{OPT}(m - 1, c)$, the least demerits of any feasible paragraph, and its chain of links is a feasible paragraph with exactly these demerits. $\square$