39. Ackermann’s Function

⍺ ack ⍵ ←→ f⍢(3∘+) ⍵   ⇒  (⍺+1)ack ⍵ ←→ f⍣(1+⍵)⍢(3∘+) 1

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

   ack←{
     0=⍺: 1+⍵
     0=⍵: (⍺-1) ∇ 1
     (⍺-1) ∇ ⍺ ∇ ⍵-1
   }

   2 ack 3
9
   3 ack 2
29

Lemma: If ⍺ ack ⍵ ←→ f⍢(3∘+) ⍵ , then (⍺+1)ack ⍵ ←→
f⍣(1+⍵)⍢(3∘+) 1 . (⍢ is the under operator where f⍢g y ←→ g⍣¯1 f g y .)

Proof: By induction on ⍵ .

(⍺+1) ack 0	basis
⍺ ack 1	definition of ack
f⍢(3∘+) 1	antecedent of lemma
f⍣(1+0)⍢(3∘+) 1	⍣
(⍺+1) ack ⍵	induction
⍺ ack (⍺+1) ack ⍵-1	definition of ack
f⍢(3∘+) (⍺+1) ack ⍵-1	antecedent of lemma
f⍢(3∘+) f⍣(1+⍵-1)⍢(3∘+) 1	inductive hypothesis
¯3∘+ f 3∘+ ¯3∘+ f⍣(1+⍵-1) ⊢3∘+ 1	⍢ and ⊢
¯3∘+ f f⍣(1+⍵-1) ⊢3∘+ 1	+
¯3∘+ f⍣(1+⍵) ⊢3∘+ 1	⍣
f⍣(1+⍵)⍢(3∘+) 1	⍢
	QED

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

0∘ack = 1∘+⍢(3∘+)
1∘ack = 2∘+⍢(3∘+)
2∘ack = 2∘×⍢(3∘+)
3∘ack = 2∘*⍢(3∘+)
4∘ack = */∘(⍴∘2)⍢(3∘+)
5∘ack = {*/∘(⍴∘2)⍣(1+⍵)⍢(3∘+) 1}

From http://xkcd.com/207

Appeared in J [101, 109] and in APL [96].