Essays/Ackermann's Function

Ackermann's function is defined on the non-negative integers as follows:

   ack=: c1`c1`c2`c3 @. (#.@(,&*))
   c1=: >:@]                        NB. if 0=x, 1+y
   c2=: <:@[ ack 1:                 NB. if 0=y, (x-1) ack 1
   c3=: <:@[ ack [ ack <:@]         NB. else,   (x-1) ack x ack y-1

   2 ack 3
9
   3 ack 2
29

Lemma: If x ack y is f&.(3&+) y , then (x+1) ack y is f^:(1+y)&.(3&+) 1 .

Proof: By induction on y .

(x+1) ack 0                         NB. Basis
x ack 1                             NB. Definition
f&.(3&+) 1                          NB. x&ack
f^:(1+0)&.(3&+) 1                   NB. ^:

(x+1) ack y                         NB. Induction
x ack (x+1) ack y-1                 NB. Definition
f&.(3&+) (x+1) ack y-1              NB. x&ack
f&.(3&+) f^:(1+y-1)&.(3&+) 1        NB. Inductive Hypothesis
_3&+ f 3&+ _3&+ f^:(1+y-1) 3&+ 1    NB. &.
_3&+ f f^:(1+y-1) 3&+ 1             NB. +
_3&+ f^:(1+y) 3&+ 1                 NB. ^:
f^:(1+y)&.(3&+) 1                   NB. &.
                                               QED

Using the lemma (or otherwise), it can be shown that:

0&ack =  >:&.(3&+)                  NB. successor
1&ack = 2&+&.(3&+)                  NB. addition
2&ack = 2&*&.(3&+)                  NB. multiplication
3&ack = 2&^&.(3&+)                  NB. power
4&ack = ^/@(#&2)&.(3&+)             NB. power tower
5&ack = 3 : '^/@(#&2)^:(1+y)&.(3&+) 1'

---

See also

MathWorld

---

Contributed by Roger Hui. Substantially the same text previously appeared in Vector, Volume 9, Number 2, October 1992.