講演名 2005-12-22
左線形シャローなどの項書換え系の停止性の決定性
王 易, 酒井 正彦, 西田 直樹, 草刈 圭一朗, 坂部 俊樹,
PDFダウンロードページ PDFダウンロードページへ
抄録(和) 本稿では, 左線形シャロー項書換え系の停止性が決定可能であることを示す. 本手法の手続きは依存グラフにおける引数の伝播の分析と, 木オートマトン技術による項の到達可能性の検証で構成される. また, 提案する手法が他のクラスにも適用可能かを検討する.
抄録(英) In this paper, we show that the termination is decidable for left-linear shallow term rewriting systems. The decision procedure consists of the analysis of argument propagation in the dependency graph and the reachability between two terms that is verified by using tree automata techniques. We also explore the potentiality of this method to other rewriting systems such as growing TRSs.
キーワード(和) 依存対 / グローイング項書換え系 / 木オートマトン / 決定手続き
キーワード(英) dependency pair / growing TRSs / tree automata / decision procedure
資料番号 COMP2005-50
発行日

研究会情報
研究会 COMP
開催期間 2005/12/15(から1日開催)
開催地(和)
開催地(英)
テーマ(和)
テーマ(英)
委員長氏名(和)
委員長氏名(英)
副委員長氏名(和)
副委員長氏名(英)
幹事氏名(和)
幹事氏名(英)
幹事補佐氏名(和)
幹事補佐氏名(英)

講演論文情報詳細
申込み研究会 Theoretical Foundations of Computing (COMP)
本文の言語 ENG
タイトル(和) 左線形シャローなどの項書換え系の停止性の決定性
サブタイトル(和)
タイトル(英) Decidability of Termination for Left-Linear Shallow Term Rewriting Systems and Related
サブタイトル(和)
キーワード(1)(和/英) 依存対 / dependency pair
キーワード(2)(和/英) グローイング項書換え系 / growing TRSs
キーワード(3)(和/英) 木オートマトン / tree automata
キーワード(4)(和/英) 決定手続き / decision procedure
第 1 著者 氏名(和/英) 王 易 / Yi WANG
第 1 著者 所属(和/英) 名古屋大学大学院情報科学研究科
Graduate School of Information Science, Nagoya University
第 2 著者 氏名(和/英) 酒井 正彦 / Masahiko SAKAI
第 2 著者 所属(和/英) 名古屋大学大学院情報科学研究科
Graduate School of Information Science, Nagoya University
第 3 著者 氏名(和/英) 西田 直樹 / Naoki NISHIDA
第 3 著者 所属(和/英) 名古屋大学大学院情報科学研究科
Graduate School of Information Science, Nagoya University
第 4 著者 氏名(和/英) 草刈 圭一朗 / Keiichiro KUSAKARI
第 4 著者 所属(和/英) 名古屋大学大学院情報科学研究科
Graduate School of Information Science, Nagoya University
第 5 著者 氏名(和/英) 坂部 俊樹 / Toshiki SAKABE
第 5 著者 所属(和/英) 名古屋大学大学院情報科学研究科
Graduate School of Information Science, Nagoya University
発表年月日 2005-12-22
資料番号 COMP2005-50
巻番号(vol) vol.105
号番号(no) 499
ページ範囲 pp.-
ページ数 5
発行日