高階項書換えシステムの合流性自動検証に関する研究

2011 年度 研究成果報告書

• 研究課題/領域番号: 21700017
• 研究種目: 若手研究(B)
• 配分区分: 補助金
• 研究分野: 情報学基礎
• 研究機関: 島根大学
• 研究代表者: 岩見 宗弘 島根大学, 総合理工学部, 講師 (70314614)
• 研究期間 (年度): 2009 – 2011
• キーワード: 項書換えシステム / 高階項書換えシステム / 無限項書換えシステム / 合流性 / 強頭部正規化可能性 / 強収束性 / 生成性 / 一般生成性

研究概要

高階項書換えシステムの合流性自動検証のために、様々な書換えシステムの研究を行った。研究成果として、組合せ子の項書換えシステムの多くが強頭部正規化可能性を持たないことを示した。さらに、無限項書換えシステムの強頭部正規化可能性および生成性に対する反証手続きを提案し、反証手続きの正しさを示すとともに、手続きの実装を行った。

研究成果

• [雑誌論文] 無限項書き換えシステムにおける強頭部正規化可能性および一般生成性の自動反証 (2012)
  • 著者名/発表者名: 岩見宗弘, 青戸等人
  • 雑誌名: コンピュータソフトウェア 巻: Vol.29, No.1 ページ: 211-239
  • URL: https://www.jstage.jst.go.jp/article/jssst/29/1/29_1_1_211/_pdf
  • 査読あり
• [雑誌論文] 無限項書き換えシステムにおける性質に関する考察 (2011)
  • 著者名/発表者名: 岩見宗弘, 青戸等人
  • 雑誌名: 京都大学数理解析研究所講究録 巻: No.1769 ページ: 153-157
• [雑誌論文] 左線形かつK-開発閉包な項書換えシステムの合流性に関する考察 (2010)
  • 著者名/発表者名: 岩見宗弘
  • 雑誌名: 京都大学数理解析研究所講究録 巻: No.1712 ページ: 156-161
• [雑誌論文] 無限項書換えシステムにおける強頭部正規化可能性の反証手続き (2010)
  • 著者名/発表者名: 岩見宗弘, 青戸等人
  • 雑誌名: 第12回プログラミングおよびプログラミング言語ワークショップ論文集 ページ: 261-273
  • 査読あり
• [雑誌論文] 組合せ子の強収束性 (2009)
  • 著者名/発表者名: 岩見宗弘
  • 雑誌名: 第8回情報科学技術フォーラム講演論文集 ページ: 251-258
• [備考]
  • URL: http://www.cis.shimane-u.ac.jp/~munehiro/