Ackermann's Function in Iterative Form: A Proof Assistant Experiment

TL;DR

This paper demonstrates formalising Ackermann's function in an iterative form within Isabelle/HOL, showcasing how proof assistants can handle complex recursive functions and establish their properties.

Contribution

It introduces an iterative formulation of Ackermann's function and proves its equivalence to the recursive version using a proof assistant, highlighting formalisation of difficult recursions.

Findings

Proof of termination for the iterative Ackermann's function

Equivalence between iterative and recursive formulations established

Demonstrates formalisation of complex recursions in Isabelle/HOL

Abstract

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.