Automated Complexity Analysis for Term Rewriting

• Project/Area Number: 20800022
• Research Category: Grant-in-Aid for Young Scientists (Start-up)
• Allocation Type: Single-year Grants
• Research Field: Fundamental theory of informatics
• Research Institution: Japan Advanced Institute of Science and Technology
• Principal Investigator: HIROKAWA Nao Japan Advanced Institute of Science and Technology, 情報科学研究科, 助教 (50467122)
• Research Collaborator: MOSER Georg University of Innsbruck, Institute for Computer Science, Research Assistant
• Project Period (FY): 2008 – 2009
• Project Status: Completed (Fiscal Year 2009)
• Budget Amount: ¥2,535,000 (Direct Cost: ¥1,950,000、Indirect Cost: ¥585,000); Fiscal Year 2009: ¥1,508,000 (Direct Cost: ¥1,160,000、Indirect Cost: ¥348,000); Fiscal Year 2008: ¥1,027,000 (Direct Cost: ¥790,000、Indirect Cost: ¥237,000)
• Keywords: 項書き換え / 計算モデル / 計算量 / 情報基礎

Research Abstract

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

Research Products

• [Journal Article] KBO Orientability (2009)
  • Author(s): Harald Zankl, Nao Hirokawa, Aart Middeldorp
  • Journal Title: Journal of Automated Reasoning 43(2) Pages: 173-201
  • NAID: 120002260314
  • Peer Reviewed
• [Presentation] Uncurrying for Innermost Termination and Derivational Complexity (2010)
  • Author(s): Harald Zankl, Nao Hirokawa, Aart Middeldorp
  • Organizer: 5^<th> International Workshop on Higher-Order Rewriting
  • Place of Presentation: エジンバラ大学(イギリス)(発表確定)
  • Year and Date: 2010-07-14
• [Presentation] The Subterm Criterion in Complexity Analysis (2009)
  • Author(s): Nao Hirokawa, Georg Moser
  • Organizer: In Proceedings of the 10th International Workshop on Termination
  • Place of Presentation: Leipzig, Germany
  • Year and Date: 2009-06-04
• [Presentation] Uncurrying for Termination. In Proceedings of the 15th International Conferences on Logic for Programming (2008)
  • Author(s): Nao Hirokawa, Aart Middeldorp, Harald Zankl
  • Organizer: Artificial Intelligence and Reasoning, Sydney, Australia, Lecture Notes in Computer Science
  • Place of Presentation: Sydney, Australia
  • Year and Date: 2008-11-27
• [Presentation] Complexity, Graphs, and the Dependency Pair Method (2008)
  • Author(s): Nao Hirokawa, Georg Moser
  • Organizer: In Proceedings of the 15th International Conferences on Logic for Programming, Artificial Intelligence and Reasoning, Sydney, Australia, Lecture Notes in Computer Science
  • Place of Presentation: Sydney, Australia
  • Year and Date: 2008-11-27
• [Presentation] Uncurrying for Termination (2008)
  • Author(s): Nao Hirokawa, Aart Middeldorp, Harald Zankl
  • Organizer: the 15th International Conferences on Logic for Programming, Artificial Intelligence, Reasoning
  • Place of Presentation: カタール国ドーハ
  • Year and Date: 2008-11-27
• [Presentation] Complexity, Graphs, and the Dependency Pair Method (2008)
  • Author(s): Nao Hirokawa, Georg Moser
  • Organizer: the 15th International Conferences on Logic for Programming, Artificial Intelligence, Reasoning
  • Place of Presentation: カタール国ドーハ
  • Year and Date: 2008-11-27
• [Book] 「ソフトウェア基礎」, 「定理証明と検証法」, 「SAT」 (2010)
  • Author(s): 廣川直
  • Publisher: 電子情報通信学会
• [Book] 電子情報通信学会 知識ベース 7群1編「ソフトウェア基礎」2章「定理証明と検証法」3節「SAT」執筆 (2010)
  • Author(s): 廣川直
  • Total Pages: 7
  • Publisher: 社団法人 電子情報通信学会
• [Remarks]
  • URL: http://www.jaist.ac.jp/~hirokawa/
• [Remarks]
  • URL: http://www.jaist.ac.jp/~hirokawa/
• [Remarks]
  • URL: http://www.jalst.ac.ip/~hirokawa/