## Proving termination with multiset orderings

[examples

Ackermann's function

recursion

Stanford

]
The title of this post is identical to the title of a seminal paper
by Nachum Dershowitz and Zohar Manna, both of whom I knew as a graduate student at Stanford.
(I had the privilege of doing directed reading under Zohar’s supervision.)
*Multisets* are collections, like sets except that
multiple occurrences of elements are significant.
Computer scientists typically encounter them as a way of specifying
the concept of sorting: to transform an input list into an output
that is correctly ordered but equal to the input when both are regarded as multisets.
Dershowitz and Manna showed that multisets also provided
natural but strong orderings for proving termination.
I had written about the termination of a rewrite system for Ackermann’s function
in an earlier post
and was advised to contact “Dershowitz, a leading
expert on termination”.
His reply was that the answer I sought was in his 1979 paper!

### Multiset orderings

The idea is to lift an ordering on the elements of multisets to the multisets themselves. The precise definition of how to compare two multisets is somewhat involved, but basically involves cancelling everything they have in common and comparing the largest elements at which they differ. It may suffice to recount a conversation I had long ago with a dubious Rod Burstall: “So if apples are greater than oranges then three apples are greater than two oranges? No: then one apple is greater than a million oranges.” Powerful stuff, and yet this ordering is well-founded (therefore terminating) provided the element ordering is.

A mathematician would probably prefer to replace multisets by non-increasing sequences, compared lexicographically.
Then it’s clear that if the base ordering
has order type $\alpha$ then the corresponding multiset ordering
will have order type $\omega^\alpha$.
Dershowitz and Manna also considered the *iterated* nesting of multisets,
which has order type $\epsilon_0$.
This is easily strong enough for any termination question likely to arise in computer science.

### Ackermann’s function (again)

In the interest of saving you from having to keep referring to the previous post on Ackermann’s function, let’s recall its definition:

\[\begin{align*} A(0,n) & = n+1\\ A(m+1,0) & = A(m,1)\\ A(m+1,n+1) & = A(m,A(m+1,n)). \end{align*}\]Called the generalised exponential, it is an attempt to extend the sequence
*successor*, *addition*, *multiplication*, *exponentiation* indefinitely according to its first argument.
It grows fast: faster than any primitive recursive function, which is
easy to prove.

Ackermann’s function can easily be expressed in terms of a stack computation, or equivalently as a term rewriting system:

\[\DeclareMathOperator{\Suc}{Suc} \DeclareMathOperator{\ack}{ack} \newcommand{\cons}{\mathbin{\#}} \begin{align*} \Box \cons n\cons 0\cons L &\longrightarrow \Box \cons \Suc n \cons L\\ \Box \cons 0\cons \Suc m\cons L &\longrightarrow \Box \cons 1\cons m \cons L\\ \Box \cons \Suc n\cons \Suc m\cons L &\longrightarrow \Box \cons n\cons \Suc m\cons m \cons L \end{align*}\](In Isabelle, # separates list elements.)

### Defining the functions in Isabelle/HOL

As before, both definitions of Ackermann’s function can be typed straight into Isabelle/HOL. The termination of the standard version is proved automatically. It’s by the lexicographic combination of the two arguments, which works despite the nested recursion in the third line.

fun ack :: "[nat,nat] ⇒ nat" where "ack 0 n = Suc n" | "ack (Suc m) 0 = ack m 1" | "ack (Suc m) (Suc n) = ack m (ack (Suc m) n)"

Now we declare the stack version.
Last time,
the termination of the stack computation was shown by explicit reasoning
about its domain. The declaration below still uses the `function`

keyword,
which means that the termination proof will come later.

function ackloop :: "nat list ⇒ nat" where "ackloop (n # 0 # l) = ackloop (Suc n # l)" | "ackloop (0 # Suc m # l) = ackloop (1 # m # l)" | "ackloop (Suc n # Suc m # l) = ackloop (n # Suc m # m # l)" | "ackloop [m] = m" | "ackloop [] = 0" by pat_completeness auto

Only this time, termination will be proved with the help of multisets.

### Proving termination via multisets

Recall that the multiset ordering is based on an ordering of the element type. The elements of our multisets will be pairs of natural numbers, ordered lexicographically (the first component dominating). If the first two elements of the stack are $z$ and $y$, then the multiset will contain the pair $(y,z)$, and each further stack element $x$ will contribute the pair $(x+1,0)$ to the multiset. The following function accomplishes this:

fun ack_mset :: "nat list ⇒ (nat×nat) multiset" where "ack_mset [] = {#}" | "ack_mset [x] = {#}" | "ack_mset (z#y#l) = mset ((y,z) # map (λx. (Suc x, 0)) l)"

It’s not difficult to check that for each of the recursive calls made by the stack-based computation, the corresponding multiset decreases according to the multiset ordering and therefore the recursion terminates. More details are in the paper; it’s Example 3, on page 471. The program in that paper reflects the conventions of 1979: it is coded in a variant of Algol with $z$ a global variable rather than a stack element.

The most difficult case of termination I had to formalise explicitly, below. It’s for the first recursive call. That the multiset ${(m,n+1)}$ is less than ${(m+1,0),(0,n)}$ requires step-by-step reasoning. The cases for the other two recursive calls are proved automatically.

lemma case1: "ack_mset (Suc n # l) < add_mset (0,n) {# (Suc x, 0). x ∈# mset l #}" proof (cases l) case (Cons m list) have "{#(m, Suc n)#} < {#(Suc m, 0)#}" by auto also have "… ≤ {#(Suc m, 0), (0,n)#}" by auto finally show ?thesis by (simp add: Cons) qed auto

The following command asks Isabelle—specifically, Alex Krauss’s function package— to check termination
with reference to the function `ack_mset`

,
supplying the result proved above as a lemma.

termination by (relation "inv_image {(x,y). x<y} ack_mset") (auto simp: wf case1)

Since the supplied tactic proved the termination subgoals, termination is established. Isabelle will now supply unconditional recursion equations for the function.

### Proving the two definitions equivalent

Last time, I introduced an additional function as part of the proof that the stack-based computation was equivalent to the traditional version of Ackermann’s function. This had educational value perhaps, but the equivalence can be proved without it. The following result is all we need:

lemma ackloop_ack: "ackloop (n # m # l) = ackloop (ack m n # l)" by (induction m n arbitrary: l rule: ack.induct) auto

As in the earlier post,
a one line proof is possible thanks to `ack.induct`

, the induction rule
specific to Ackermann’s function.
And now we are done!

theorem "ack m n = ackloop [n,m]" by (simp add: ackloop_ack)

- Download the Isabelle proof development.
- Blanchette et al. describe much more advanced proofs such as Goodstein’s theorem, using their formalisation of nested multisets.