|
This article is cited in 4 scientific papers (total in 4 papers)
On some slowly terminating term rewriting systems
L. D. Beklemisheva, A. A. Onoprienkob a Steklov Mathematical Institute of Russian Academy of Sciences
b Lomonosov Moscow State University, Faculty of Mechanics and Mathematics
Abstract:
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.
Received: 25.03.2015 and 21.06.2015
Citation:
L. D. Beklemishev, A. A. Onoprienko, “On some slowly terminating term rewriting systems”, Mat. Sb., 206:9 (2015), 3–20; Sb. Math., 206:9 (2015), 1173–1190
Linking options:
https://www.mathnet.ru/eng/sm8519https://doi.org/10.1070/SM2015v206n09ABEH004493 https://www.mathnet.ru/eng/sm/v206/i9/p3
|
Statistics & downloads: |
Abstract page: | 722 | Russian version PDF: | 201 | English version PDF: | 9 | References: | 67 | First page: | 42 |
|