This looks great (at least for a first try). I will start with this and then see how far I can get. I wondered if seq was flexible enough for such a definition, so I thought that ~rec or ~recs would be needed. If ~seq is sufficient, so much the better.
Thierry Arnoux schrieb am Sonntag, 28. April 2024 um 15:29:32 UTC+2: > Maybe I would try as follows, using the seq operator instead of recs, and > the definition as an iterated 1-ary function > <https://en.wikipedia.org/wiki/Ackermann_function#Definition:_as_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 > > > On 28/04/2024 11:25, 'Alexander van der Vekens' via Metamath wrote: > > 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? > > > Alexander van der Vekens schrieb am Sonntag, 28. April 2024 um 11:21:11 > UTC+2: > >> 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 schrieb am Sonntag, 28. April 2024 um 11:13:45 >> UTC+2: >> >>> 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: >>> >>> [image: {\displaystyle {\begin{array}{lcl}\operatorname {a} >>> (0,m)&=&m+1\\\operatorname {a} (n+1,0)&=&\operatorname {a} >>> (n,1)\\\operatorname {a} (n+1,m+1)&=&\operatorname {a} (n,\operatorname {a} >>> (n+1,m))\end{array}}}] >>> >>> 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): >>> >>> [image: {\displaystyle {\begin{array}{lcl}A_{1}(n)&=&2n&{\text{wenn >>> }}n\geq 1,\\A_{k}(1)&=&2&{\text{wenn }}k\geq >>> 2,\\A_{k}(n)&=&A_{k-1}(A_{k}(n-1))&{\text{wenn }}n\geq 2,k\geq >>> 2.\end{array}}}] >>> >>> 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... >>> >> -- > 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 [email protected]. > To view this discussion on the web visit > https://groups.google.com/d/msgid/metamath/a74a9fd3-8572-4a1f-8a2f-36d7d6e20172n%40googlegroups.com > > <https://groups.google.com/d/msgid/metamath/a74a9fd3-8572-4a1f-8a2f-36d7d6e20172n%40googlegroups.com?utm_medium=email&utm_source=footer> > . > > -- 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 [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/6a28ea33-a690-4c22-81c5-e7021e574db7n%40googlegroups.com.
