I was recently writing test for checking the termination of programs and I wanted to write some difficult condition to verify so that the solver didn't use the if-condition to simplify the goal to proof.
It turned that writing in the if, ackermann(x,y) == 1 (for the definition of Ackermann see Wikipedia) was sufficient to confuse the solver, but I also tried ackermann(x,y) == ackermann(y,x) and of course the solver didn't go better on this instance.
I'm thinking of other programs that imply difficult problems in mathematics, for instance the so-called Collatz problem (also Syracuse, Kakutani, Hasse or Ulam's problem):
while n > 1 do
if(n mod 2) != 0 then n = 3n + 1
else n = n div 2
So my question is, is there any problem with Ackermann's commutativity. Is it known what pairs (if any) of numbers make it commutative?
Aside from $m=n$ the only cases of commutativity are $A(1,0)=A(0,1)$ and $A(2,0)=A(0,2)$. In all other cases $m \gt n \implies A(m,n) \gt A(n,m)$. I don't have a nice proof of that, but the height of the tower is much more important than the numbers that make up the tower. You can find cases where different pairs of arguments give equal values, like $A(0,12)=A(1,11)=A(2,5)=A(3,1)=A(4,0)=13$ and $A(0,65534)=A(1,65533)=A(2,32765)=A(3,13)=A(4,1)=65533$
Looking at the definition, given $A(m,n)$ you can also express it as $A(p,q)$ for every $p \lt m$.