Theorems · Definition · logic and foundations
ack
ℕ → ℕ → ℕ
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.
- Defined in
- Mathlib.Computability.Ackermann
- Cited by
- 41 results in Mathlib
- Foundations
- Depth 49 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites0
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Nothing in Mathlib beyond the foundations.
Cited by41
Results whose statement or proof uses this declaration.
- ack_strictMono_rightstatement · cited by 8
- ack_succ_succstatement and proof · cited by 8
- ack_strictMono_leftstatement · cited by 6
- ack_zerostatement · cited by 6
- ack_mono_leftstatement · cited by 5
- ack_mono_rightstatement · cited by 5
- ack_succ_zerostatement and proof · cited by 5
- add_lt_ackstatement · cited by 4
- ack_add_one_sq_lt_ack_add_threestatement · cited by 2
- ack_succ_right_le_ack_succ_leftstatement and proof · cited by 2
- one_lt_ack_succ_leftstatement · cited by 1
- Nat.Partrec.Code.eval_pappAckstatement and proof · cited by 1