Differences between revisions 11 and 12
 ⇤ ← Revision 11 as of 2007-09-05 21:18:46 → Size: 1791 Editor: RogerHui Comment: ← Revision 12 as of 2008-12-08 10:45:38 → ⇥ Size: 1771 Editor: anonymous Comment: converted to 1.6 markup Deletions are marked like this. Additions are marked like this. Line 22: Line 22: `(x+1) ack 0 ` Basis [[BR]]`x ack 1 ` Definition [[BR]]`f&.(3&+) 1 ` `x&ack` [[BR]]`f^:(1+0)&.(3&+) 1 ` `^:` [[BR]] `(x+1) ack 0 ` Basis <
>`x ack 1 ` Definition <
>`f&.(3&+) 1 ` `x&ack` <
>`f^:(1+0)&.(3&+) 1 ` `^:` <
> Line 27: Line 27: `(x+1) ack y ` Induction [[BR]]`x ack (x+1) ack y-1 ` Definition [[BR]]`f&.(3&+) (x+1) ack y-1 ` `x&ack` [[BR]]`f&.(3&+) f^:(1+y-1)&.(3&+) 1 ` Inductive Hypothesis [[BR]]`_3&+ f 3&+ _3&+ f^:(1+y-1) 3&+ 1 ` `&.` [[BR]]`_3&+ f f^:(1+y-1) 3&+ 1 ` `+` [[BR]]`_3&+ f^:(1+y) 3&+ 1 ` `^:` [[BR]]`f^:(1+y)&.(3&+) 1 ` `&.` [[BR]] `(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 ` `&.` <
> Line 49: Line 49: [[BR]] <
> Line 53: Line 53: [http://mathworld.wolfram.com/AckermannFunction.html MathWorld] [[MathWorld:AckermannFunction|MathWorld]] Line 55: Line 55: [[BR]] <
> Line 58: Line 58: Substantially the same text previously appeared in [http://www.vector.org.uk Vector], Substantially the same text previously appeared in [[http://www.vector.org.uk|Vector]],

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'```