@article{oai:nagoya.repo.nii.ac.jp:00019002,
 author = {御宿, 義勝 and 酒井, 正彦 and 坂部, 俊樹 and 草刈, 圭一朗 and 西田, 直樹 and MISHUKU, Yoshimasa and SAKAI, Masahiro and SAKABE, Toshiki and KUSAKARI, Keiichirou and NISHIDA, Naoki},
 issue = {343},
 journal = {電子情報通信学会技術研究報告SS, ソフトウェアサイエンス},
 month = {Dec},
 note = {依存対が右線形右シャローである項書換え系のクラスでは,停止性および最内停止性が決定可能であることが示されている(内山ら2008年).しかし,文脈依存停止性の決定可能性は同クラスのうち,さらに左シャローであるクラスでしか示されていない.文脈依存書換えでは依存鎖中に停止しない項が存在することが,その停止性の解析を困難にしている.本論文ではまず,内山らの決定手続きが働かない左シャローでない項書換え系を例示する.次に,この困難性をもたらす原因を取り除くための十分条件を追加し,このクラスで文脈依存停止性が決定可能となることを示す., It is known that termination and innermost termination are decidable for term rewriting systems (TRSs for short) whose dependency pairs are all right-linear and right-shallow (Uchiyama et al, 2008). However, decidability of context-sensitive termination requires left-shallow restriction to those TRSs. The difficulty of context-sensitive termination analysis is caused by existence of non-terminating terms in dependency chains. In this paper, we first show a left-non-shallow TRS as a counterexample against the decision procedure. Then, we give a sufficient condition to make the procedure work properly, and show that context-sensitive termination is decidable for the class.},
 pages = {31--36},
 title = {右線形右シャローな項書換え系における文脈依存停止性の決定可能性について},
 volume = {109},
 year = {2009}
}