English
The two-argument Ackermann function A: N×N → N is defined by A(0,n)=n+1; A(m+1,0)=A(m,1); A(m+1,n+1)=A(m,A(m+1,n)). It is a classic fast-growing function and serves as a fundamental example of a recursive function not primitive recursive.
Русский
Функция Аккермана A: ℕ×ℕ → ℕ задана рекуррентно: A(0,n)=n+1; A(m+1,0)=A(m,1); A(m+1,n+1)=A(m,A(m+1,n)). Применяется как пример быстро растущей рекурсивной функции, не являющейся примитивно-рекурсивной.
LaTeX
$$$$A: \mathbb{N} \times \mathbb{N} \to \mathbb{N},\quad A(0,n)=n+1,\quad A(m+1,0)=A(m,1),\quad A(m+1,n+1)=A(m, A(m+1,n)).$$$$
Lean4
/-- The two-argument Ackermann function, defined so that
- `ack 0 n = n + 1`
- `ack (m + 1) 0 = ack m 1`
- `ack (m + 1) (n + 1) = ack m (ack (m + 1) n)`.
This is of interest as both a fast-growing function, and as an example of a recursive function that
isn't primitive recursive. -/
def ack : ℕ → ℕ → ℕ
| 0, n => n + 1
| m + 1, 0 => ack m 1
| m + 1, n + 1 => ack m (ack (m + 1) n)
