消去法による項書換え系の停止性判定について

• 中村 正樹

  北陸先端科学技術大学院大学 情報科学研究科

• 外山 芳人

  北陸先端科学技術大学院大学 情報科学研究科

書誌事項

タイトル別名

• On Proving Termination by General Dummy Elimination

抄録

従来の停止性判定法を適用できない項書換えシステム(TRS)の停止性を示すために, Ferreiraは一般消去法を提案した.一般消去法は, 規則に現れる適当な関数記号を消去することでより単純な構造のTRSに変換する.変換後のTRSが停止性を持つならば元のTRSも停止性を持つという性質があるため, 一般消去法は停止性判定に有効である.一方, ArtsとGieslは, TRSの規則に現れる関数定義記号の出現に注目し, 無限書換え列の本質を簡潔に記述できる依存対の概念を導入した.本稿では, 一般消去法が変換後に付け加える規則に注目し, 不必要な規則を除くことで一般消去法を改良する.改良一般消去法においても, 変換後のTRSが元のTRSの停止性を保証していることを依存対の概念を用いることで示す.

収録刊行物

• 電子情報通信学会技術研究報告. COMP, コンピュテーション

  電子情報通信学会技術研究報告. COMP, コンピュテーション 98 (432), 57-64, 1999-11-16

  一般社団法人電子情報通信学会

キーワード

• 項書換え系
• 停止性
• 変換
• 消去法
• 依存対

詳細情報

• CRID: 1573105977190727680
• NII論文ID: 110003191684
• NII書誌ID: AN10013152
• 本文言語コード: ja
• データソース種別:
  • CiNii Articles