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 I tried that in Haskell, the denominator is 5552 digits, way too big for floating point precision.
The social network of the future: No ads, no corporate surveillance, ethical design, and decentralization! Own your data with Mastodon!