On some slowly terminating term rewriting systems

被引：4

作者：

Beklemishev, L. D. ^{[1
]}

Onoprienko, A. A. ^{[2
]}

机构：

[1] Russian Acad Sci, Steklov Math Inst, Moscow 117901, Russia

[2] Moscow MV Lomonosov State Univ, Fac Mech & Math, Moscow, Russia

来源：

SBORNIK MATHEMATICS | 2015年 / 206卷 / 09期

基金：

俄罗斯科学基金会;

关键词：

term rewriting systems; Peano arithmetic; Worm principle; HYDRA BATTLE;

D O I：

10.1070/SM2015v206n09ABEH004493

中图分类号：

O1 [数学];

学科分类号：

0701 ; 070101 ;

摘要：

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 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.

引用

页码：1173 / 1190

页数：18

共 16 条

[1]

[Anonymous], 2003, CAMBRIDGE TRACTS THE, V55

[2]

Baader Franz, 1998, Term Rewriting and All That, DOI DOI 10.1017/CBO9781139172752

[3]

Beklemishev L., 2006, OBERWOLFACH REP, V3, P3093, DOI 10.4171/OWR/2006/52

[4] Reflection principles and provability algebras in formal arithmetic [J].

Beklemishev, LD .

RUSSIAN MATHEMATICAL SURVEYS, 2005, 60 (02) :197-268

[5]

Beklemishev Lev., 2012, Advances in modal logic, V9, P89

[6]

Beklemishev LD, 2006, LECT NOTES LOGIC, V27, P75

[7]

Buchholz W., 2006, OBERWOLFACH REP, V3, P3099, DOI 10.4171/OWR/2006/52

[8]

Dershowitz N., 1990, HDB THEORETICAL COMP, P243

[9]

Dershowitz N, 2007, LECT NOTES COMPUT SC, V4600, P1

[10]

GALLIER JH, 1991, ANN PURE APPL LOGIC, V53, P199, DOI 10.1016/0168-0072(91)90022-E

← 1 2 →