Geodesic
On some slowly terminating term rewriting systems
Sbornik. Mathematics, Tome 206 (2015) no. 9, pp. 1173-1190

Voir la notice de l'article provenant de la source Math-Net.Ru

We formulate some term rewriting systems in which the number of computation steps is finite for each output, but this number cannot be bounded by a provably total computable function in Peano arithmetic $\mathsf{PA}$. Thus, the termination of such systems is unprovable in $\mathsf{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.
Keywords: term rewriting systems, Peano arithmetic, Worm principle. 
@article{SM_2015_206_9_a0,
     author = {L. D. Beklemishev and A. A. Onoprienko},
     title = {On some slowly terminating term rewriting systems},
     journal = {Sbornik. Mathematics},
     pages = {1173--1190},
     publisher = {mathdoc},
     volume = {206},
     number = {9},
     year = {2015},
     language = {en},
     url = {http://geodesic.mathdoc.fr/item/SM_2015_206_9_a0/}
}
TY  - JOUR
AU  - L. D. Beklemishev
AU  - A. A. Onoprienko
TI  - On some slowly terminating term rewriting systems
JO  - Sbornik. Mathematics
PY  - 2015
SP  - 1173
EP  - 1190
VL  - 206
IS  - 9
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/SM_2015_206_9_a0/
LA  - en
ID  - SM_2015_206_9_a0
ER  - 
%0 Journal Article
%A L. D. Beklemishev
%A A. A. Onoprienko
%T On some slowly terminating term rewriting systems
%J Sbornik. Mathematics
%D 2015
%P 1173-1190
%V 206
%N 9
%I mathdoc
%U http://geodesic.mathdoc.fr/item/SM_2015_206_9_a0/
%G en
%F SM_2015_206_9_a0
L. D. Beklemishev; A. A. Onoprienko. On some slowly terminating term rewriting systems. Sbornik. Mathematics, Tome 206 (2015) no. 9, pp. 1173-1190. http://geodesic.mathdoc.fr/item/SM_2015_206_9_a0/