; Ackermann's function (define (A x y) (cond ((= y 0) 0) ((= x 0) (* 2 y)) ((= y 1) 2) (else (A (- x 1) (A x (- y 1)))))) ; (A 1 10) ; => 1024 ; (A 1 10) ; (A 0 (A 1 9)) ; (A 0 (A 0 (A 1 8))) ; (A 0 (A 0 (A 0 (A 1 7)))) ; (A 0 (A 0 (A 0 (A 0 (A 1 6))))) ; (A 0 (A 0 (A 0 (A 0 (A 0 (A 1 5)))))) ; (A 0 (A 0 (A 0 (A 0 (A 0 (A 0 (A 1 4))))))) ; (A 0 (A 0 (A 0 (A 0 (A 0 (A 0 (A 0 (A 1 3)))))))) ; (A 0 (A 0 (A 0 (A 0 (A 0 (A 0 (A 0 (A 0 (A 1 2))))))))) ; (A 0 (A 0 (A 0 (A 0 (A 0 (A 0 (A 0 (A 0 (A 0 (A 1 1)))))))))) ; (A 0 (A 0 (A 0 (A 0 (A 0 (A 0 (A 0 (A 0 (A 0 2))))))))) ; (A 0 (A 0 (A 0 (A 0 (A 0 (A 0 (A 0 (A 0 4)))))))) ; (A 0 (A 0 (A 0 (A 0 (A 0 (A 0 (A 0 8))))))) ; (A 0 (A 0 (A 0 (A 0 (A 0 (A 0 16)))))) ; (A 0 (A 0 (A 0 (A 0 (A 0 32))))) ; (A 0 (A 0 (A 0 (A 0 64)))) ; (A 0 (A 0 (A 0 128))) ; (A 0 (A 0 256)) ; (A 0 512) ; 1024 ; (A 2 4) ; => 65536 ; (A 3 3) ; => 65536 (define (f n) (A 0 n)) ; f(n) = A(0, n) = 2n (define (g n) (A 1 n)) ; g(n) = A(1, n) = 2^n if n > 0 ; Proof: ; Base case ; if n = 1: g(n) = A(1, 1) = 2 = 2^1 ; ; Inductive case ; Suppose g(n) = 2^n for n >= 1, then ; g(n + 1) = A(1, n + 1) = A(0, A(1, n)) = A(0, g(n)) ; = A(0, 2^n) ; g(n) = 2^n by the inductive hypothesis ; = 2*2^n = 2^(n + 1) (define (h n) (A 2 n)) ; h(n) = A(2, n) = 2^2^2 .. ^2 where there are n 2s for n > 0 ; e.g. h(1) = 2, h(2) = 2^2, h(3) = 2^2^2 ; ; Proof: ; Base case ; h(1) = A(2, 1) = 2 ; ; Inductive case ; For n >= 1 ; Suppose h(n) = 2^2...^2 ; n 2s ; ; h(n + 1) = A(2, n + 1) = A(1, A(2, n)) ; = A(1, h(n)) ; Definition of h ; = g(h(n)) ; Definition of g ; = 2^h(n) ; Because h(n) > 0, g(h(n)) = 2^(h(n)) from previous proof. ; = 2^(2^2 ... ^2) ; n 2s between the parens by inductive hypothesis ; = 2^2^2 ... ^2 ; (n + 1) 2s because ^ is right associative (define (k n) (* 5 n n)) ; k(n) = 5n^2