Essays/Ackermann's Function

From J Wiki
Jump to: navigation, search

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'



See also

MathWorld



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