Imperative Programming vs. Functional Programming

1. What does the following program do, i.e., what is the value of r in terms of p and q? Assume the array is large enough.
2. How large should the array be?
3. How much time will the program spend?
4. How much time do you need to figure all this out?
5. Write a functional program to compute the same r. Compare. :-)

a[1] = p;
a[2] = q;
n = 2;
while (n != 1) {
  if (a[n-1] == 0) {
    a[n-1] = a[n] + 1;
    n = n - 1;
  }
  else if (a[n] == 0) {
    a[n-1] = a[n-1] - 1;
    a[n] = 1;
  }
  else {
    a[n+1] = a[n] - 1;
    a[n] = a[n-1];
    a[n-1] = a[n-1] - 1;
    n = n + 1;
  }
}
r = a[1];

Solution

I only answer 1 and 5. 2 and 3 are difficult and will be answered in the future.

The program seems to use the array and the index n together as a stack to simulate calls and returns of a recursive function (which is the function the question asks for). Sometimes parameters are placed on the stack; other times parameters are removed and return values are placed on the stack. Below I interpret the program in this light and guess the function.

Notation: I write a stack's content as R⊲x to mean that the top is x, and R stands for the rest of the stack. This notation can be nested, e.g., ((R⊲w)⊲x)⊲y means the top is y, beneath that are x and then w, and the rest is R; I also declare ⊲ to be left-associative so I can write R⊲w⊲x⊲y. I write [] for the empty stack's content, usually for the rest of the stack, e.g., initially the stack has []⊲p⊲q, and at the end the stack has []⊲answer. Naturally, when I write like R⊲w⊲x⊲y, R may be [].

The program is equivalent to:

The function computed seems to take 2 parameters. I will define a function f of 2 parameters by drawing inspirations from the program. When I do that, I do not claim that the program computes f yet (I'm just defining f to be whatever I like); but afterwards, I can prove it.

When the program transforms the stack from R⊲0⊲y to R⊲y+1, it seems to return from a call, i.e., replacing parameters by a return value. It inspires f(0,y) = y+1.

When the program transforms the stack from R⊲x⊲0 to R⊲x-1⊲1 (if x≠0), it seems to change parameters and call again, adopting the new call's return value as the old call's, so nothing more needs to be done except continuing. It inspires f(x,0) = f(x-1,1) if x≠0.

When the program transforms the stack from R⊲x⊲y to R⊲x-1⊲x⊲y-1 (if x≠0 and y≠0), it seems to change 2 parameters to 3 parameters, which is strange. I think this is to set up two nested calls: x and y-1 are for the inner call, and then x-1 and the inner call's return value are for the outer call. It inspires f(x,y) = f(x-1, f(x, y-1)) if x≠0 and y≠0.

So I define f to be

f(0, y) = y+1
f(x, 0) = f(x-1, 1) if x≠0
f(x, y) = f(x-1, f(x, y-1)) if x≠0 and y≠0

This is the Ackermann-Péter function.

Now I still have to prove that the program computes f. To do this, I focus on the loop body. Each iteration transforms an old stack to a new stack. I will prove:

∀x,y,R· R⊲x⊲y is transformed after finitely many iterations to R⊲f(x,y)

(Below I abbreviate “transformed after finitely many iterations” as “transformed”.)

Then we will know the loop starts with []⊲p⊲q and ends with []⊲f(p,q), after which the loop is exited and r = f(p,q) at the end.

In the proof, I use implicitly that f takes pairs of natural numbers to natural numbers, and all numbers in all stack contents are natural numbers throughout program execution if p,q are natural numbers.

Proof by induction on x:

• Prove ∀y,R· R⊲0⊲y is transformed to R⊲f(0, y)

  R⊲0⊲y is transformed to R⊲y+1
  which equals R⊲f(0, y).

• Assume ∀y,R· R⊲m⊲y is transformed to R⊲f(m, y)
  Prove ∀y,R· R⊲m+1⊲y is transformed to R⊲f(m+1, y)

  By induction on y:

  • Prove ∀R· R⊲m+1⊲0 is transformed to R⊲f(m+1, 0)

    R⊲m+1⊲0 is transformed to R⊲m⊲1
    then is transformed to R⊲f(m, 1) (outer induction hypothesis)
    which equals f(m+1, 0).

  • Assume ∀R· R⊲m+1⊲n is transformed to R⊲f(m+1, n)
    Prove ∀R· R⊲m+1⊲n+1 is transformed to R⊲f(m+1, n+1)

    R⊲m+1⊲n+1 is transformed to R⊲m⊲m+1⊲n
    then is tranformed to R⊲m⊲f(m+1, n) (inner induction hypothesis)
    then is transformed to R⊲f(m, f(m+1, n)) (outer induction hypothesis)
    which equals R⊲f(m+1, n+1)

A functional program (or any program that does not shy away from recursion) to compute the same thing looks like the three equations defining f and is much clearer. Here is a Haskell version:

r = f p q
  where
    f 0 y = y+1
    f x 0 = f (x-1) 1
    f x y = f (x-1) (f x (y-1))

Here is an SML version:

val r = let
  fun f 0 y = y+1
    | f x 0 = f (x-1) 1
    | f x y = f (x-1) (f x (y-1))
in f p q
end