Consider the algorithm "M(x): if x<0 return -x, else return M(x-M(x-1))/2". This algorithm terminates for all real x, though this is not so easy to prove. In fact, Peano Arithmetic cannot prove the statement "M(x) terminates for all natural x". Paper to come! Joint work with @jeffgerickson and @alreadydone

@gnivasch @jeffgerickson @alreadydone I couldn't get much from a Python implementation because it already overflowed its stack for M(3), so I had to try working out small arguments by hand. This is piecewise linear and positive with discontinuities at a countable well-ordered set of points of order type \(\omega^\omega\)?

@gnivasch @jeffgerickson @alreadydone And termination follows from the fact that each recursive call jumps over at least one discontinuity, so well-ordering implies that infinitely-deep recursion is impossible?

@11011110 @jeffgerickson @alreadydone Not \(\omega^\omega\), but \(\varepsilon_0\)