Ackermann's function can be expressed using an iterative algorithm, which essentially takes the form of a term rewriting system. Although the termination of this algorithm is far from obvious, its equivalence to the traditional recursive formulation--and therefore its totality--has a simple proof in Isabelle/HOL. This is a small example of formalising mathematics using a proof assistant, with a focus on the treatment of difficult recursions.

翻译：Ackermann的功能可以用一种迭代算法来表达,这种算法基本上采取术语重写系统的形式。虽然这种算法的终止远非显而易见,但它与传统的累进式配方是等同的,因此,它在伊莎贝尔/HOL中拥有一个简单的证明。 这是一个使用一名校对助理将数学正规化的小型例子,重点是处理困难的累进。