# 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