書き換えシステムの合流性自動判定法の研究

2012 年度 研究成果報告書

• 研究課題/領域番号: 22500002
• 研究種目: 基盤研究(C)
• 配分区分: 補助金
• 応募区分: 一般
• 研究分野: 情報学基礎
• 研究機関: 東北大学
• 研究代表者: 外山 芳人 東北大学, 電気通信研究所, 教授 (00251968)
• 研究分担者: 青戸 等人 東北大学, 電気通信研究所, 准教授 (00293390)
• 研究期間 (年度): 2010 – 2012
• キーワード: 書き換えシステム / 合流性 / 自動検証 / 停止性 / モジュラ性

研究概要

項書き換えシステムの理論は定理自動証明や計算モデルでひろく利用されている。近年、項書き換えシステムの停止性自動証明システムが数多く開発されているにもかかわらず、合流性自動証明システムについてはほとんど研究されていない。本研究では、さまざまな手法に基いて項書き換えシステムの合流性自動証明システムACPを開発することである。研究成果としては、リダクション保存完備化による合流性自動証明、片側減少ダイアグラムによる可換性自動証明、多項式サイズ正規形を保証する経路順序、永続性をもちいた合流性自動証明などがある。合流性に関する国際ワークショップ(IWC2012)における合流性自動判定システムの第1回コンペティションにおいて、本研究で開発されたACPは、参加3システム中第1位の成績で優勝することができた。

研究成果

• [雑誌論文] 片側減少ダイアグラム法による項書き換えシステムの可換性証明法 (2013)
  • 著者名/発表者名: 的場正樹,青戸等人,外山芳人
  • 雑誌名: コンピュータソフトウェア 巻: Vol.30,No.1 ページ: 187-202
  • URL: https://www.jstage.jst.go.jp/article/jssst/30/1/30_1_187/_article/-char/ja/
  • 査読あり
• [雑誌論文] A reduction-preserving completion for proving confluence of non-terminating term rewriting systems (2012)
  • 著者名/発表者名: Takahito Aoto , Yoshihito Toyama
  • 雑誌名: Logical Methods in Computer Science 巻: Vol.8, No.1:31 ページ: 1-29
  • URL: http://www.lmcs-online.org/ojs/viewarti cle.php?id=1099&layout=abstract
  • 査読あり
• [雑誌論文] 無限項書き換えシステムにおける強頭部正規化可能性および一般生成性の自動反証 (2012)
  • 著者名/発表者名: 岩見宗弘,青戸等人
  • 雑誌名: コンピュータソフトウェア 巻: Vol.29,No.1 ページ: 211-239
  • URL: https://www.jstage.jst.go.jp/article/jssst/29/1/29_1_1_211/_article/-char/ja/
  • 査読あり
• [雑誌論文] 多項式サイズ正規形を保証する項書き換えシステムの経路順序 (2012)
  • 著者名/発表者名: 磯部耕己,青戸等人,外山芳人
  • 雑誌名: コンピュータソフトウェア 巻: Vol.29,No.1 ページ: 176-190
  • URL: https://www.jstage.jst.go.jp/article/jssst/29/1/29_1_1_176/_article/-char/ja/
  • 査読あり
• [雑誌論文] Program transformation templates for tupling based on term rewriting (2010)
  • 著者名/発表者名: Yuki Chiba, Takahito Aoto , Yoshihito Toyama
  • 雑誌名: IEICE Transactions on Information and Systems 巻: Vol.E93-D, No.5 ページ: 963-973
  • URL: http://search.ieice.org/bin/pdf.php?lan g=E&year=2010&fname=e93-d_5_963&abst=
  • 査読あり
• [学会発表] Termination of rule-based calculi for uniform semi-unification (2013)
  • 著者名/発表者名: Takahito Aoto , Munehiro Iwami
  • 学会等名: the 7th International Conference on Language and Automata Theory and Applications (LATA 2013)
  • 発表場所: Bilbao, Spain
  • 年月日: 20130402-05
• [学会発表] Rational term rewriting revisited:decidability and confluence (2012)
  • 著者名/発表者名: Takahito Aoto , Jeroen Ketema
  • 学会等名: the 6th International Conference on Graph Transformation (ICGT 2012)
  • 発表場所: Bremen, Germany
  • 年月日: 20120924-29
• [学会発表] Transformations by templates for simply-typed term rewriting (2012)
  • 著者名/発表者名: Yuki Chiba , Takahito Aoto
  • 学会等名: the 6th International Workshop on Higher-Order Rewriting (HOR 2012)
  • 発表場所: Nagoya, Japan
  • 年月日: 20120528-0602
• [学会発表] Natural inductive theorems for higher-order rewriting (2011)
  • 著者名/発表者名: Takahito Aoto, Toshiyuki Yamada , Yuki Chiba
  • 学会等名: the 22nd International Conference on Rewriting Techniques and Applications (RTA 2011)
  • 発表場所: Novi Sad, Serbia
  • 年月日: 20110530-0601
• [学会発表] Reduction-preserving completion for proving confluence of non-terminating term rewriting systems (2011)
  • 著者名/発表者名: Takahito Aoto , Yoshihito Toyama
  • 学会等名: the 22nd International Conference on Rewriting Techniques and Applications (RTA 2011)
  • 発表場所: Novi Sad, Serbia
  • 年月日: 20110530-0601
• [学会発表] Automated confluence proof by decreasingdiagrams based on rule-labelling (2010)
  • 著者名/発表者名: Takahito Aoto
  • 学会等名: the 21st International Conference on Rewriting Techniques and Applications (RTA 2010)
  • 発表場所: Edingburgh, UK
  • 年月日: 20100709-21
• [備考]
  • URL: http://www.nue.riec.tohoku.ac.jp/index-j.html