pappAck — Mathlib

English

The code for the partially applied Ackermann function.

Русский

Код частично применённой функции Аккермана.

LaTeX

$$$$pappAck : \\mathbb{N} \\to Code.$$$$

Lean4

/-- The code for the partially applied Ackermann function.
This is used to prove that the Ackermann function is computable. -/
def pappAck : ℕ → Code
  | 0 => .succ
  | n + 1 => step (pappAck n)
where/-- Yields single recursion step on `pappAck`. -/
   step (c : Code) : Code := .curry (.prec (.comp c (.const 1)) (.comp c (.comp .right .right))) 0

Похожие утверждения