; 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