項書き換えに基づく計算量解析の自動化

2009 年度 研究成果報告書

• 研究課題/領域番号: 20800022
• 研究種目: 若手研究(スタートアップ)
• 配分区分: 補助金
• 研究分野: 情報学基礎
• 研究機関: 北陸先端科学技術大学院大学
• 研究代表者: 廣川 直 北陸先端科学技術大学院大学, 情報科学研究科, 助教 (50467122)
• 研究協力者: モーザー ゲーオグ University of Innsbruck, Institute for Computer Science, Research Assistant
• 研究期間 (年度): 2008 – 2009
• キーワード: 項書き換え / 計算モデル / 計算量

研究概要

探索やソートアルゴリズムを開発したとき、「入力の大きさに対しどれくらいの速度(ステップ数)で動作するか」という自然な疑問が生じる。現在に至るまで時間的計算量は、プログラムごとに手作業で解析するものと認識されていた。本研究では、関数型プログラムの計算モデルである項書き換え系に対して、解析を自動化する強力な理論を構築した。さらにそれに基づく計算量自動解析ツールを実装した。既存手法との比較実験を行った結果、解析精度の劇的な向上が確認された。

研究成果

• [雑誌論文] KBO Orientability (2009)
  • 著者名/発表者名: Harald Zankl, Nao Hirokawa, Aart Middeldorp
  • 雑誌名: Journal of Automated Reasoning 43(2) ページ: 173-201
  • 査読あり
• [学会発表] The Subterm Criterion in Complexity Analysis (2009)
  • 著者名/発表者名: Nao Hirokawa, Georg Moser
  • 学会等名: In Proceedings of the 10th International Workshop on Termination
  • 発表場所: Leipzig, Germany
  • 年月日: 2009-06-04
• [学会発表] Uncurrying for Termination. In Proceedings of the 15th International Conferences on Logic for Programming (2008)
  • 著者名/発表者名: Nao Hirokawa, Aart Middeldorp, Harald Zankl
  • 学会等名: Artificial Intelligence and Reasoning, Sydney, Australia, Lecture Notes in Computer Science
  • 発表場所: Sydney, Australia
  • 年月日: 2008-11-27
• [学会発表] Complexity, Graphs, and the Dependency Pair Method (2008)
  • 著者名/発表者名: Nao Hirokawa, Georg Moser
  • 学会等名: In Proceedings of the 15th International Conferences on Logic for Programming, Artificial Intelligence and Reasoning, Sydney, Australia, Lecture Notes in Computer Science
  • 発表場所: Sydney, Australia
  • 年月日: 2008-11-27
• [図書] 「ソフトウェア基礎」, 「定理証明と検証法」, 「SAT」 (2010)
  • 著者名/発表者名: 廣川直
  • 出版者: 電子情報通信学会
• [備考]
  • URL: http://www.jaist.ac.jp/~hirokawa/