McCarthy91 Terminates

Description of the problem

Fix three natural number parameters \(a,b,c\) such that \(a \> b\). Let me define a function recursively as follow (in pseudo-code)

function f
   input: a natural number n
   output: a natural number
begin
   if n < c then
      return f ( f (n + a) )
   else
      return n - b
   end if
end

Today I would like to show that the recursion terminates for every input \(x\).

A solution

First, observe that the recursion terminates at the first step if the input \(x\) is greater or equal to \(c\). This means, we need to show that recursion terminates when the input is in the range \(\{0,1,\ldots,c-1\}\).

Let us inspect the way this function is evaluated on the stack. Assume that we start with 0. The recursion will iterate as

0 f => a f f => 2a f f f => 3a f f f f => ...

until we find a number \(m\) such that \((m-1)a < c \leq ma\). Then the number of f’s we applied starts decreasing until we hit a point where we find another number \(\ell\) such that \(ma-\ell b < c \leq ma - (\ell-1)b\). If at this point the number of f’s on the stack is 0 then we stop. Otherwise, we repeat this 2-step procedure.

I will change the problem, and make it slightly more general. Assume we define a recursive sequence of pairs of integers \((x_n,y_n)\) as follows \[ (x_{n+1},y_{n+1}) = \begin{cases} (x_n,0) & \text{ if } y_n = 0\\ (x_n + a, y_n + 1) & \text{ if } x_n < c\\ (x_n - b, y_n - 1) & \text{ otherwise } \end{cases} \] Then the problem of showing that the recursion terminates translates into showing the sequence above becomes stationary when the first term \((x_0,y_0)\) is set to \((x,1)\).

Lemma: If there are two indices \(n \> m\) such that \(x_n = x_m\) then \(y_n < y_m\).

Proof: (By way of contradiction) Assume \(y_n \geq y_m\). This means between the indices \(m\) and \(n\) (inclusive), we saw the cases \(x_i < c\) with \(y_i \> 0\) more than the cases \(x_i \geq c\) with \(y_i \> 0\). Respectively, let \(r\) be the number of the cases \(x_i < c\) and let \(\ell\) be the number of cases \(x_i \geq c\) from \(i=n\) to \(i=m\). Then we get that \(r \geq \ell\) by our assumption and \[ x_n = x_m = x_n + ra - \ell b \] which is impossible as \(a \> b\).

Proposition: For every \(x\in\{0,1,\ldots,c-1\}\) the recursive sequence we defined above for every initial value of the form \((x,m)\) will always stabilize.

Proof: (By way of contradiction) Assume the sequence does not stabilize for a specific \(1\leq x < c\). We consider the first component \((x_n)\) of the recursive sequence only. Note that the recursive sequence is designed so that when \(x_n\) is larger than \(c\), the next terms in the sequence are forced to be smaller until \(x_n\) becomes smaller than \(c\). Thus if the sequence is not stationary it must visit the region \(\{0,1,\ldots,c-1\}\) infinitely often. Then by pigeon-hole principle there must be a number \(z\in \{0,1,\ldots,c-1\}\) which our sequence \((x_n)\) must visit infinitely often. That is, there must be a subsequence \(n_1 < n_2 < \cdots < n_k < \cdots\) such that \(x_{n_i} = z\). But then the Lemma above indicates that we have a strictly decreasing sequence of natural numbers \[ y_{n_1} \> y_{n_2} \> \cdots \> y_{n_k} \> \cdots \geq 0 \] which is impossible. Thus the sequence \((y_n)\) must stabilize which is possible only when \(y_n=0\) after some point.

A little bit of history on McCarthy91

The original version of the function is defined and used by McCarthy in a series papers in the 70’s. That version uses the parameters \(a=11\), \(b=10\) and \(c=101\). Then Knuth asked a similar question using real number parameters \(a\), \(b\) and \(c\). The fact the function terminates with real parameters is formally verified by Cowles using ACL2. The case I did here is somewhat in between.

An implementation in lisp

OK. Here is an implementation in lisp

(defun mccarthy (n a b c)
   (if (< n c) (mccarthy (mccarthy (+ n a) a b c) a b c)
               (- n b)))
MCCARTHY

I will trace this function to show the effect of its computation on the stack.

(trace mccarthy)
(mccarthy 74 11 10 101)
1> (MCCARTHY 74 11 10 101)
| 2> (MCCARTHY 85 11 10 101)
|   3> (MCCARTHY 96 11 10 101)
|   | 4> (MCCARTHY 107 11 10 101)
|   | <4 (MCCARTHY 97)
|   | 4> (MCCARTHY 97 11 10 101)
|   |   5> (MCCARTHY 108 11 10 101)
|   |   <5 (MCCARTHY 98)
|   |   5> (MCCARTHY 98 11 10 101)
|   |   | 6> (MCCARTHY 109 11 10 101)
|   |   | <6 (MCCARTHY 99)
|   |   | 6> (MCCARTHY 99 11 10 101)
|   |   |   7> (MCCARTHY 110 11 10 101)
|   |   |   <7 (MCCARTHY 100)
|   |   |   7> (MCCARTHY 100 11 10 101)
|   |   |   | 8> (MCCARTHY 111 11 10 101)
|   |   |   | <8 (MCCARTHY 101)
|   |   |   | 8> (MCCARTHY 101 11 10 101)
|   |   |   | <8 (MCCARTHY 91)
|   |   |   <7 (MCCARTHY 91)
|   |   | <6 (MCCARTHY 91)
|   |   <5 (MCCARTHY 91)
|   | <4 (MCCARTHY 91)
|   <3 (MCCARTHY 91)
|   3> (MCCARTHY 91 11 10 101)
|   | 4> (MCCARTHY 102 11 10 101)
|   | <4 (MCCARTHY 92)
|   | 4> (MCCARTHY 92 11 10 101)
|   |   5> (MCCARTHY 103 11 10 101)
|   |   <5 (MCCARTHY 93)
|   |   5> (MCCARTHY 93 11 10 101)
|   |   | 6> (MCCARTHY 104 11 10 101)
|   |   | <6 (MCCARTHY 94)
|   |   | 6> (MCCARTHY 94 11 10 101)
|   |   |   7> (MCCARTHY 105 11 10 101)
|   |   |   <7 (MCCARTHY 95)
|   |   |   7> (MCCARTHY 95 11 10 101)
|   |   |   | 8> (MCCARTHY 106 11 10 101)
|   |   |   | <8 (MCCARTHY 96)
|   |   |   | 8> (MCCARTHY 96 11 10 101)
|   |   |   |   9> (MCCARTHY 107 11 10 101)
|   |   |   |   <9 (MCCARTHY 97)
|   |   |   |   9> (MCCARTHY 97 11 10 101)
|   |   |   |   | 10> (MCCARTHY 108 11 10 101)
|   |   |   |   | <10 (MCCARTHY 98)
|   |   |   |   | 10> (MCCARTHY 98 11 10 101)
|   |   |   |   |   11> (MCCARTHY 109 11 10 101)
|   |   |   |   |   <11 (MCCARTHY 99)
|   |   |   |   |   11> (MCCARTHY 99 11 10 101)
|   |   |   |   |   12> (MCCARTHY 110 11 10 101)
|   |   |   |   |   <12 (MCCARTHY 100)
|   |   |   |   |   12> (MCCARTHY 100 11 10 101)
|   |   |   |   |   13> (MCCARTHY 111 11 10 101)
|   |   |   |   |   <13 (MCCARTHY 101)
|   |   |   |   |   13> (MCCARTHY 101 11 10 101)
|   |   |   |   |   <13 (MCCARTHY 91)
|   |   |   |   |   <12 (MCCARTHY 91)
|   |   |   |   |   <11 (MCCARTHY 91)
|   |   |   |   | <10 (MCCARTHY 91)
|   |   |   |   <9 (MCCARTHY 91)
|   |   |   | <8 (MCCARTHY 91)
|   |   |   <7 (MCCARTHY 91)
|   |   | <6 (MCCARTHY 91)
|   |   <5 (MCCARTHY 91)
|   | <4 (MCCARTHY 91)
|   <3 (MCCARTHY 91)
| <2 (MCCARTHY 91)
| 2> (MCCARTHY 91 11 10 101)
|   3> (MCCARTHY 102 11 10 101)
|   <3 (MCCARTHY 92)
|   3> (MCCARTHY 92 11 10 101)
|   | 4> (MCCARTHY 103 11 10 101)
|   | <4 (MCCARTHY 93)
|   | 4> (MCCARTHY 93 11 10 101)
|   |   5> (MCCARTHY 104 11 10 101)
|   |   <5 (MCCARTHY 94)
|   |   5> (MCCARTHY 94 11 10 101)
|   |   | 6> (MCCARTHY 105 11 10 101)
|   |   | <6 (MCCARTHY 95)
|   |   | 6> (MCCARTHY 95 11 10 101)
|   |   |   7> (MCCARTHY 106 11 10 101)
|   |   |   <7 (MCCARTHY 96)
|   |   |   7> (MCCARTHY 96 11 10 101)
|   |   |   | 8> (MCCARTHY 107 11 10 101)
|   |   |   | <8 (MCCARTHY 97)
|   |   |   | 8> (MCCARTHY 97 11 10 101)
|   |   |   |   9> (MCCARTHY 108 11 10 101)
|   |   |   |   <9 (MCCARTHY 98)
|   |   |   |   9> (MCCARTHY 98 11 10 101)
|   |   |   |   | 10> (MCCARTHY 109 11 10 101)
|   |   |   |   | <10 (MCCARTHY 99)
|   |   |   |   | 10> (MCCARTHY 99 11 10 101)
|   |   |   |   |   11> (MCCARTHY 110 11 10 101)
|   |   |   |   |   <11 (MCCARTHY 100)
|   |   |   |   |   11> (MCCARTHY 100 11 10 101)
|   |   |   |   |   12> (MCCARTHY 111 11 10 101)
|   |   |   |   |   <12 (MCCARTHY 101)
|   |   |   |   |   12> (MCCARTHY 101 11 10 101)
|   |   |   |   |   <12 (MCCARTHY 91)
|   |   |   |   |   <11 (MCCARTHY 91)
|   |   |   |   | <10 (MCCARTHY 91)
|   |   |   |   <9 (MCCARTHY 91)
|   |   |   | <8 (MCCARTHY 91)
|   |   |   <7 (MCCARTHY 91)
|   |   | <6 (MCCARTHY 91)
|   |   <5 (MCCARTHY 91)
|   | <4 (MCCARTHY 91)
|   <3 (MCCARTHY 91)
| <2 (MCCARTHY 91)
<1 (MCCARTHY 91)
91