講演抄録/キーワード |
講演名 |
2009-12-17 16:20
右線形右シャローな項書換え系における文脈依存停止性の決定可能性について ○御宿義勝・酒井正彦・坂部俊樹・草刈圭一朗・西田直樹(名大) SS2009-40 |
抄録 |
(和) |
依存対が右線形右シャローである項書換え系のクラスでは,停止性および最内停止性が決定可能であることが示されている(内山ら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. |
キーワード |
(和) |
文脈依存停止性 / 決定可能性 / 右シャロー / / / / / |
(英) |
context-sensitive termination / decidability / right-shallow / / / / / |
文献情報 |
信学技報, vol. 109, no. 343, SS2009-40, pp. 31-36, 2009年12月. |
資料番号 |
SS2009-40 |
発行日 |
2009-12-10 (SS) |
ISSN |
Print edition: ISSN 0913-5685 Online edition: ISSN 2432-6380 |
著作権に ついて |
技術研究報告に掲載された論文の著作権は電子情報通信学会に帰属します.(許諾番号:10GA0019/12GB0052/13GB0056/17GB0034/18GB0034) |
PDFダウンロード |
SS2009-40 |