The Ackermann function

[Alexander van der Vekens]

I wonder how the Ackermann function (see Wikipedia https://en.wikipedia.org/wiki/Ackermann_function) can be defined in Methamath/set.mm. 

The Ackermann function with two arguments (introduced by Rózsa Péter) is defined recursively:

Maybe the following variant of the Ackermann function (with only one argument) is easier to be defined with the means of set.mm (and could serve as a starting point):

I am not so familiar with the definitions `recs` (see -df-recs) or `rec` (see ~df-rec) for transfinite recursion, so I have no idea how to start. Were/are there already any attempts to formalize the Ackermann funktion with Metamath? Is there any material (beyond the comments in set.mm and the Metamath Book) how to formalize such recursive definitions?

I would like to prove some properties of the Ackermann function, but for this, I need an appropriate definition first...

[Alexander van der Vekens]

Sorry, copying the definitions from Wikipedia did not work properly. Here are the definitions again (hopefully readable now):

a(0,m)     = m+1

a(n+1,0)   = a(n,1)

a(n+1,m+1) = a (n,a(n+1,m))

and

A_1(n) = 2n                for n >= 1,

A_k(1) = 2                 for k >= 2,

A_k(n) = A_(k-1)(A_k(n-1)) for n >= 2, k >= 2.

[Alexander van der Vekens]

The Ackermann function was already mentioned before in this Google group (in the context of Metamath Zero, see https://groups.google.com/g/metamath/c/raGj9fO6U2I/m/Y8mGHAW8AQAJ):

• The one thing that is a bit complicated is non-primitive induction and recursion. Wikipedia says that functions like the Ackermann function are definable in PA, but it's not obvious to me how to do this. I'm assuming we have an iota operator, so that we can extract functions from unique existence proofs. If we have a predicate that says "the Ackermann function is defined at (m,n)" then we can prove this predicate by double induction, but I don't know how to define this predicate. Any ideas?

Does this help somehow?

[Thierry Arnoux]

Maybe I would try as follows, using the seq operator instead of recs, and the definition as an iterated 1-ary function:

Let's say F : NN0 --> NN0 is a function we want to apply repeatedly.

Then B = ( f e. _V |-> seq 0 ( ( g e. _V , i e. _V |-> ( f o. g ) ) , _I ) ) should be the n-th iterate of f: ( ( B ` f ) ` 3 ) = ( f o. ( f o. f ) ) )

We can then define the Ackermann function as follows:

Ack = seq 0 ( ( f e. _V , i e, _V |-> ( n e. NN0 |-> ( ( ( B ` f ) ` n ) ` 1 ) ) , ( n e. NN0 |-> ( n + 1 ) ) )

That is, we would have:

• Using ~seq1 : ( Ack ` 0 ) = ( n e. NN0 |-> ( n + 1 ) )
• Using ~seqp1 : ( ( Ack ` ( m + 1 ) ) ` n ) = ( ( ( B ` ( Ack ` m ) ) ` n ) ` 1 )
  

Then I would derive the other definition of the Ackermann function as a property.

BR,
_
Thierry

--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/a74a9fd3-8572-4a1f-8a2f-36d7d6e20172n%40googlegroups.com.

[Jim Kingdon]

On 4/28/24 06:29, 'Thierry Arnoux' via Metamath wrote:

Maybe I would try as follows, using the seq operator instead of recs, and the definition as an iterated 1-ary function:

I didn't try to check every step, but this looks about right.

As for the larger question of how to formalize recursive definitions, generally via seq somehow. It can be a bit hard to get your head around how seq is being used in a particular proof, but using seq is almost always easier than trying to use recs or rec directly.

[Alexander van der Vekens]

I successfully defined the Ackermann function in set.mm as proposed by Thierry, see Git repository, PR #3979. Some adjustments of the suggestion were necessary, especially for the "initial values" of the sequence builder `seq`. Another oddity is the second argument i e. _V which is needed, but not used. Since I had problems with it first, I started with `rec` and the theorems provided in section "Finite recursion". I was very successful with this approach, but its results were based on the ordinal numbers `_om` and not the nonnegative numbers `NN0`, which made calculations with numbers greater than 5 difficult. Therefore, I switched to the approach using `seq`, and the initial extra work paid off at the end. 

For more information see https://github.com/metamath/set.mm/pull/3979