Decidability of Innermost Termination and Context-Sensitive Termination for Semi-Constructor Term Rewriting Systems

被引:2
|
作者
Uchiyama, Keita [1 ]
Sakai, Masahiko [1 ]
Sakabe, Toshiki [1 ]
机构
[1] Nagoya Univ, Grad Sch Informat Sci, Chikusa Ku, Nagoya, Aichi 4648603, Japan
关键词
Context-Sensitive Termination; Dependency Pair; Innermost Termination;
D O I
10.1016/j.entcs.2008.03.051
中图分类号
TP301 [理论、方法];
学科分类号
081202 ;
摘要
Yi and Sakai [13] showed that the termination problem is a decidable property for the class of semi-constructor term rewriting systems, which is a superclass of the class of right-ground term rewriting systems. Decidability was shown by the fact that every non-terminating TRS in the class has a loop. In this paper we modify the proof of [13] to show that both innermost termination and mu-termination are decidable properties for the class of semi-constructor TRSs.
引用
收藏
页码:21 / 34
页数:14
相关论文
共 50 条
  • [1] Innermost termination of context-sensitive rewriting
    Giesl, J
    Middeldorp, A
    [J]. DEVELOPMENTS IN LANGUAGE THEORY, 2003, 2450 : 231 - 244
  • [2] Using Context-Sensitive Rewriting for Proving Innermost Termination of Rewriting
    Alarcon, Beatriz
    Lucas, Salvador
    [J]. ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2009, 248 : 3 - 17
  • [3] Termination of innermost context-sensitive rewriting using dependency pairs
    Alarcon, Beatriz
    Lucas, Salvador
    [J]. FRONTIERS OF COMBINING SYSTEMS, PROCEEDINGS, 2007, 4720 : 73 - +
  • [4] Termination of context-sensitive rewriting
    Zantema, H
    [J]. REWRITING TECHNIQUES AND APPLICATIONS, 1997, 1232 : 172 - 186
  • [5] Decidability of Termination and Innermost Termination for Term Rewriting Systems with Right-Shallow Dependency Pairs
    Uchiyama, Keita
    Sakai, Masahiko
    Sakabe, Toshiki
    [J]. IEICE TRANSACTIONS ON INFORMATION AND SYSTEMS, 2010, E93D (05) : 953 - 962
  • [6] Termination of (Canonical) context-sensitive rewriting
    Lucas, S
    [J]. REWRITING TECHNIQUES AND APPLICATIONS, 2002, 2378 : 296 - 310
  • [7] Decidability of termination for semi-constructor TRSs, left-linear shallow TRSs and related systems
    Wang, Yi
    Sakai, Masahiko
    [J]. TERM REWRITING AND APPLICATIONS, PROCEEDINGS, 2006, 4098 : 343 - 356
  • [8] Proving Termination of Context-Sensitive Rewriting with MU-TERM
    Alarcon, Beatriz
    Gutierrez, Raul
    Iborra, Jose
    Lucas, Salvador
    [J]. ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2007, 188 : 105 - 115
  • [9] Polynomials for proving termination of context-sensitive rewriting
    Lucas, S
    [J]. FOUNDATIONS OF SOFTWARE SCIENCE AND COMPUTATION STRUCTURES, PROCEEDINGS, 2004, 2987 : 318 - 332
  • [10] Termination of canonical context-sensitive rewriting and productivity of rewrite systems
    Lucas, Salvador
    [J]. ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2015, (200): : 18 - 31