The Ackermann function
Content created by Egbert Rijke.
Created on 2023-04-08.
Last modified on 2023-04-08.
module elementary-number-theory.ackermann-function where
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)
Recent changes
- 2023-04-08. Egbert Rijke. Refactoring elementary number theory files (#546).