partial function version of the Ackermann function must be total

Question

In mcs.pdf, it has Problem 7.25. (I only solve somewhat important problems referred to in the chapter contents because I have learnt one Discrete Mathematics book before and read mcs to ensure no importants things are omitted.)

One version of the the Ackermann function $A:\mathbb{N}^2 \to \mathbb{N}$ is defined recursively by the following rules: $$ \begin{align*} A(m, n)&::=2n &&\text{if } m = 0 \text{ or } n \le 1, &(\text{A-base})\\ A(m, n)&::=A(m-1,A(m,n-1)) &&\text{otherwise} &(AA) \end{align*} $$ Prove that if $B:\mathbb{N}^2 \to \mathbb{N}$ is a partial function that satisfies this same definition, then $B$ is total and $B=A$.

This problem is a bit weird since we can directly prove $A$ is total based on the definition and get the unique value of $A(m,n)$ as what wikipedia says by decreasing one of $m,n$ at each step until $m=0$ or $n=1$ where we can use the base case). Then why is the (partial) function $B$ needed?

(This question is edited after hinted by JulioDiEgidio's comment. As this comment says, I directly edit the question instead of using "Edited:" delimeter)

Answer 1

By reading Section 7.3, I think it is like e.g. with the "Collatz recurrence", where that constant function is one and maybe not the only one function satisfying the definition/specification. Here, assuming $B$ is a function that satisfies the "Ackermann recurrence", 1) prove that it is total; and, 2) I suppose they mean, prove it is unique: i.e., with functional extensionality, prove that, for any such $A$ and $B$, for every input, $A$ and $B$ return the same output -- or, I don't know what they mean.

Incidentally, note that in that context "function" and "partial function" are simply synonym, i.e. every function is born as a partial function, and one has to prove if a (partial) function is total.

Notice also that the WP article on the Ackermann function gives definitions that are not even easily seen equivalent to the one you are given in the book: also, at the very place you have linked, WP only gives a sketch of an argument for termination/totality, while you are asked to prove it (rigorously?) and using the framework, axioms, and definitions that are given in the book.

And your book is indeed more "sophisticated" than WP, since you are given a recurrence and have to consider the functions that fit the bill. And the last question in the exercise, as said, I simply read: prove that there is one and only one function that satisfies that recurrence.