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                          Basis
x ack 1                              Definition
f&.(3&+) 1                           x&ack
f^:(1+0)&.(3&+) 1                    ^:

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

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

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

Essays/Ackermann's Function

See also