This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.

The Ackermann function

module elementary-number-theory.ackermann-function where
Imports 
open import elementary-number-theory.natural-numbers

Idea

The Ackermann function is a fast growing binary operation on the natural numbers.

Definition

ackermann : ℕ → ℕ → ℕ
ackermann zero-ℕ n = succ-ℕ n
ackermann (succ-ℕ m) zero-ℕ = ackermann m 1
ackermann (succ-ℕ m) (succ-ℕ n) = ackermann m (ackermann (succ-ℕ m) n)