On some slowly terminating term rewriting systems
Lev D. Beklemishev, Anastasiya Aleksandrovna Onoprienko · Sbornik Mathematics · 2015
We formulate some term rewriting systems in which the num- ber of computation steps is finite for each output, but this number can- not be bounded by a provably total computable function in Peano arith- metic PA. Thus, the termination of such systems is unprovable in PA. These systems are derived from an independent combinatorial result known as the Worm principle; they can also be viewed as versions of the well-known Hercules-Hydra game introduced by Paris and Kirby. Bibliography: 16 titles.