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/5498f6ed-244b-44ce-b93d-4964f3c4fcb0n%40googlegroups.com.
