Proofs: Palindrome partition by backtracking

Correctness of palindrome partition by backtracking full

This proof shows: correctness.

We prove that PALINDROME-PARTITIONS outputs every palindromic partition of $s = s[0..n-1]$ exactly one time, in increasing lexicographic order of the sequences of piece lengths, and that it stops. Indices are 0-based and $s[i..j]$ includes both ends.

Lemma 1 (the table). After lines L1 to L4, $\mathrm{pal}[i][j]$ is true if and only if $s[i..j]$ is a palindrome, for $0 \le i \le j \le n - 1$, and $\mathit{ends}[i]$ is the increasing list of all $j$ such that $s[i..j]$ is a palindrome.

Proof. By induction on $j - i$. If $j - i \le 1$, the string $s[i..j]$ is a palindrome if and only if $s[i] = s[j]$, which is what line L3 computes. If $j - i \ge 2$, then $s[i..j]$ is a palindrome if and only if $s[i] = s[j]$ and $s[i+1..j-1]$ is a palindrome, because the mirror pairs of $s[i..j]$ are the pair $(i, j)$ and the mirror pairs of $s[i+1..j-1]$. The entry $\mathrm{pal}[i+1][j-1]$ is in row $i + 1$, which line L1 fills before row $i$, and it is correct by the induction hypothesis since $(j-1) - (i+1) < j - i$. Line L4 appends $j$ to $\mathit{ends}[i]$ exactly when $\mathrm{pal}[i][j]$ is true, and line L2 visits $j$ in increasing order. $\square$

Let $\mathcal{P}(i)$ be the list of the palindromic partitions of the suffix $s[i..n-1]$, sorted in increasing lexicographic order of their sequences of piece lengths. So $\mathcal{P}(n)$ holds one element, the empty partition. For $i < n$, each partition of $s[i..n-1]$ has a unique first piece $s[i..j]$, which is a palindrome, followed by a partition of $s[j+1..n-1]$. So by Lemma 1, $\mathcal{P}(i)$ is the concatenation, over $j$ in $\mathit{ends}[i]$ in increasing order, of the lists "$s[i..j]$ followed by $q$" for $q$ in $\mathcal{P}(j+1)$. Partitions with a shorter first piece come first in the order, and those with the same first piece are ordered by the rest.

Lemma 2 (one frame). Suppose that at some moment the stack is $S_0$ with the frame $(i, 0)$ pushed on top, and $\mathit{path}$ is a list of pieces $\pi$ whose total length is $i$. Then the loop of lines L6 to L11 runs until the stack is $S_0$ again, without reading or changing $S_0$ before that moment. In this time it outputs exactly $\pi$ followed by $q$ for each $q$ in $\mathcal{P}(i)$, in the order of $\mathcal{P}(i)$. When the stack is $S_0$ again, $\mathit{path}$ is $\pi$ without its last piece if $i > 0$, and $\pi$ if $i = 0$.

Proof. By strong induction on $n - i$.

Case $i = n$. Line L7 reads the frame $(n, 0)$, and line L8 outputs $\pi$, which is $\pi$ followed by the empty partition, the only element of $\mathcal{P}(n)$. Then it pops the frame and removes the last piece of $\mathit{path}$ if $n > 0$.

Case $i < n$. Let $\mathit{ends}[i] = (j_0 < j_1 < \cdots < j_{m-1})$, with $m \ge 1$ because $s[i..i]$ is a palindrome. We show by induction on $k$ that, for $0 \le k \le m$, the loop reaches a state where the top frame is $(i, k)$, the stack below it is $S_0$, $\mathit{path} = \pi$, and the outputs so far are $\pi$ followed by the elements of $\mathcal{P}(i)$ with first piece $s[i..j_0], \ldots, s[i..j_{k-1}]$. For $k = 0$ this is the given state. If the claim holds for some $k < m$, then line L8 does not apply since $i < n$, line L9 does not apply since $k < m$, and lines L10 and L11 set the top frame to $(i, k + 1)$, append the piece $s[i..j_k]$ to $\mathit{path}$ and push $(j_k + 1, 0)$. Now $\mathit{path}$ is $\pi$ followed by $s[i..j_k]$, of total length $j_k + 1$, and $n - (j_k + 1) < n - i$. By the induction hypothesis of the lemma, applied with $S_0$ followed by $(i, k+1)$ in the role of $S_0$, the loop outputs $\pi$, then $s[i..j_k]$, then $q$, for each $q$ in $\mathcal{P}(j_k + 1)$ in order, and comes back to the top frame $(i, k + 1)$ with $\mathit{path} = \pi$, since $j_k + 1 > 0$ and the last piece is removed. These are the elements of $\mathcal{P}(i)$ with first piece $s[i..j_k]$, so the claim holds for $k + 1$. At $k = m$, line L9 applies: it pops the frame, so the stack is $S_0$, and it removes the last piece of $\mathit{path}$ if $i > 0$. By the decomposition of $\mathcal{P}(i)$ above, the outputs are $\pi$ followed by each element of $\mathcal{P}(i)$, in order. In all these steps only the top frame and the frames above it are read or changed, so $S_0$ is untouched. $\square$

Theorem. PALINDROME-PARTITIONS stops, and it outputs each palindromic partition of $s$ exactly one time, in increasing lexicographic order of the sequences of piece lengths.

Proof. Line L5 makes the stack hold only the frame $(0, 0)$ with $\mathit{path}$ empty, of total length 0. Lemma 2 with $S_0$ empty and $i = 0$ shows that the loop comes to an empty stack, so it stops at line L6, and the outputs are the elements of $\mathcal{P}(0)$, the partitions of $s$, each one time and in order. For $n = 0$ the output is the single empty partition. Each step of the loop either pushes a frame for a new partial partition or pops a frame, and Lemma 2 shows that each pushed frame is popped; the number of partial partitions is finite, so the number of steps is finite. $\blacksquare$