Induction Ackerman function

• Jan 16th 2013, 01:38 PM
MachinePL1993
Induction Ackermann function
Hello,

I have to prove by induction that the following Ackerman function that takes pairs $\displaystyle \mathbb{N} \times \mathbb{N}$ always halts:

$\displaystyle A(x,y) =$ $\displaystyle \begin{cases} y + 1, &\text{dla } x=0\\A(x - 1, 1) &\text{dla } x>0 \ i \ y=0\\A(x - 1, A(x,y - 1)) &\text{dla } wpp \end{cases}$

How should I go about proving that when the function halts, then it returns a natural number? I don't need this assumption to prove that the first two cases of the formula halt, but for the third one, which takes $\displaystyle \langle x-1,A(x,y-1) \rangle$ I think I need to know that the second value is positive, which I have no idea how to surmise this.
• Jan 16th 2013, 02:31 PM
emakarov
Re: Induction Ackerman function
You do nested inductions: the outer one on x and the inner one on y. The induction statement (and hypothesis) for x is that A(x - 1, y) terminates for all y. It is important that the universal quantifier on y is included in the induction statement.