Proving termination with multiset orderings

26 Oct 2022

[ 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)