Essays/Ackermann's Function
< Essays
Jump to navigation
Jump to 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 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
Contributed by Roger Hui. Substantially the same text previously appeared in Vector, Volume 9, Number 2, October 1992.