The Ackermann function

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-04-08.
Last modified on 2024-10-24.

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

Idea

The Ackermann-Péter function is a fast growing binary operation on the natural numbers.

Definition

The Ackermann-Péter function

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

The simplified Ackermann function

simplified-ackermann-ℕ : ℕ → ℕ
simplified-ackermann-ℕ n = ackermann-péter-ℕ n n

Recent changes