Geodesic
On some slowly terminating term rewriting systems
Sbornik. Mathematics, Tome 206 (2015) no. 9, pp. 1173-1190 Cet article a éte moissonné depuis la source Math-Net.Ru

Voir la notice de l'article

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},
     year = {2015},
     volume = {206},
     number = {9},
     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
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
%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/

[1] J. W. Klop, “Term rewriting systems”, Handbook of logic in computer science, v. 2, Handb. Log. Comput. Sci., 2, Oxford Univ. Press, New York, 1992, 1–116 | DOI | MR

[2] Term rewriting systems. Terese, Cambridge Tracts Theoret. Comput. Sci., 55, eds. M. Bezem, J. W. Klop, R. de Vrijer, Cambridge Univ. Press, Cambridge, 2003, xxii+884 pp. | MR | Zbl

[3] H. E. Rose, Subrecursion: functions and hierarchies, Oxford Logic Guides, 9, The Clarendon Press, Oxford Univ. Press, New York, 1984, xiii+191 pp. | MR | Zbl

[4] L. Kirby, J. Paris, “Accessible independence results for Peano arithmetic”, Bull. London Math. Soc., 14:4 (1982), 285–293 | DOI | MR | Zbl

[5] N. Dershowitz, J.-P. Jouannaud, “Rewrite systems”, Handbook of theoretical computer science, v. B, Elsevier, Amsterdam, 1990, 243–320 | MR | Zbl

[6] N. Dershowitz, G. Moser, “The hydra battle revisited”, Rewriting computation and proof, Lecture Notes in Comput. Sci., 4600, Springer, Berlin, 2007, 1–27 | DOI | MR | Zbl

[7] H. Touzet, “Encoding the hydra battle as a rewrite system”, Mathematical foundations of computer science 1998 (Brno), Lecture Notes in Comput. Sci., 1450, Springer, Berlin, 1998, 267–276 | DOI | MR | Zbl

[8] L. D. Beklemishev, “The worm principle”, Logic Colloquium {'}02, Lect. Notes Log., 27, Assoc. Symbol. Logic, La Jolla, 2006, 75–95 | MR | Zbl

[9] M. Hamano, M. Okada, “A relationship among Gentzen's proof-reduction, Kirbi–Paris' hydra game, and Buchholz's hydra game”, Math. Logic Quart., 43:1 (1997), 103–120 | DOI | MR | Zbl

[10] L. D. Beklemishev, “Representing worms as a term rewriting system”, Mini-workshop: Logic, combinatorics and independence results, Report No. 52/2006, Mathematisches Forschungsinstitut Oberwolfach, Oberwolfach Rep., 3:4 (2006), 3093–3095 | DOI

[11] W. Buchholz, “Another rewrite system for the standard hydra battle”, Mini-workshop: Logic, combinatorics and independence results, Report No. 52/2006, Oberwolfach Rep., 3:4 (2006), 3099–3101 | DOI

[12] H. Zankl, S. Winkler, A. Middeldorp, “Beyond polynomials and Peano arithmetic – automation of elementary and ordinal interpretations”, J. Symbolic Comput., 69 (2015), 129–158 | DOI | MR | Zbl

[13] F. Baader, T. Nipkow, Term rewriting and all that, Cambridge Univ. Press, Cambridge, 1998, xii+301 pp. | DOI | MR | Zbl

[14] J. H. Gallier, “What's so special about Kruskal's theorem and the ordinal $\Gamma_0$? A survey of some results in proof theory”, Ann. Pure Appl. Logic, 53:3 (1991), 199–260 | DOI | MR | Zbl

[15] L. D. Beklemishev, “Reflection principles and provability algebras in formal arithmetic”, Russian Math. Surveys, 60:2 (2005), 197–268 | DOI | DOI | MR | Zbl

[16] L. Beklemishev, “Calibrating provability logic: from modal logic to reflection calculus”, Advances in modal logic, 9, Coll. Publ., London, 2012, 89–94 | MR | Zbl