Confluence Analysis for Term Rewriting and Its Applications

• Project/Area Number: 25730004
• Research Category: Grant-in-Aid for Young Scientists (B)
• Allocation Type: Multi-year Fund
• Research Field: Theory of informatics
• Research Institution: Japan Advanced Institute of Science and Technology
• Principal Investigator: Hirokawa Nao 北陸先端科学技術大学院大学, 情報科学研究科, 准教授 (50467122)
• Project Period (FY): 2013-04-01 – 2016-03-31
• Project Status: Completed (Fiscal Year 2015)
• Budget Amount: ¥3,900,000 (Direct Cost: ¥3,000,000、Indirect Cost: ¥900,000); Fiscal Year 2015: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000); Fiscal Year 2014: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000); Fiscal Year 2013: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000)
• Keywords: 項書換え / 合流性 / 国際研究者交流 / オーストリア / 可換性 / 形式言語

Outline of Final Research Achievements

Term rewriting is a fundamental computational model that underlies automated theorem proving and algebraic specification languages. In applications, deduction or computation is usually performed as an exhaustive search of normal forms. Therefore, for efficient computation, confluence that guarantees uniqueness of normal forms is considered as one of the most important properties in the area of rewriting. The main outcomes of our project are three: (1) We developed effective confluence analysis based on commutative decomposition, critical pair analysis, and E-unification. As applications of confluence analysis, (2) we obtained a simple proof for correctness of abstract completion which is a theoretical foundation of automated theorem proving, and also (3) a basic normalization theorem that enables us to effectively compute a normal form of basic terms.

Research Products

• [Int'l Joint Research] インスブルック大学(オーストリア)
• [Journal Article] AC-KBO Revisited (2015)
  • Author(s): Akihisa Yamada, Sarah Winkler, Nao Hirokawa, and Aart Middeldorp
  • Journal Title: Theory and Practice of Logic Programming Volume: 未定
  • NAID: 120005611453
  • Peer Reviewed / Open Access / Acknowledgement Compliant
• [Presentation] CoLL: A Confluence Tool for Left-Linear Term Rewrite Systems (2015)
  • Author(s): Kiraku Shintani and Nao Hirokawa
  • Organizer: 25th International Conference on Automated Deduction
  • Place of Presentation: ベルリン、ドイツ
  • Year and Date: 2015-08-04 – 2015-08-07
• [Presentation] Commutation and Signature Extensions (2015)
  • Author(s): Nao Hirokawa
  • Organizer: 4th International Workshop on Confluence
  • Place of Presentation: ドイツ・ベルリン
  • Year and Date: 2015-08-02
  • Int'l Joint Research
• [Presentation] Leftmost Outermost Revisited (2015)
  • Author(s): Nao Hirokawa, Aart Middeldorp and Georg Moser
  • Organizer: 26th International Conference on Rewriting Techniques and Applications
  • Place of Presentation: ワルシャワ、ポーランド
  • Year and Date: 2015-06-29 – 2015-07-01
• [Presentation] Basic Normalization (2014)
  • Author(s): Nao Hirokawa
  • Organizer: International Federation for Information Processing (IFIP) Working Group 1.6: Term Rewriting
  • Place of Presentation: ウィーン、オーストリア
  • Year and Date: 2014-07-13
  • Invited
• [Presentation] AC-KBO Revisited (2014)
  • Author(s): Akihisa Yamada, Sarah Winkler, Nao Hirokawa, and Aart Middeldorp
  • Organizer: 12th International Symposium on Functional and Logic Programming
  • Place of Presentation: 金沢市石川県立美術館
• [Presentation] A New and Formalized Proof of Abstract Completion (2014)
  • Author(s): Nao Hirokawa, Aart Middeldorp, and Christian Sternagel
  • Organizer: 5th International Conference on Interactive Theorem Proving
  • Place of Presentation: オーストリア・ウィーン
• [Presentation] Automated Complexity Analysis Based on Context-Sensitive Rewriting (2014)
  • Author(s): Nao Hirokawa and Georg Moser
  • Organizer: Joint 25th International Conference on Rewriting Techniques and Applications and 12th International Conference on Typed Lambda Calculi and Applications
  • Place of Presentation: オーストリア・ウィーン
• [Remarks] 項書換えの合流性解析とその応用
  • URL: http://www.jaist.ac.jp/~hirokawa/kaken12.html
• [Remarks] Confluence Competition
  • URL: http://coco.nue.riec.tohoku.ac.jp/
• [Remarks] 研究代表のホームページ
  • URL: http://www.jaist.ac.jp/~hirokawa/
• [Remarks] 合流性ツール Saigawa
  • URL: http://www.jaist.ac.jp/project/saigawa/
• [Remarks] 合流性コンペティション CoCo
  • URL: http://coco.nue.riec.tohoku.ac.jp/
• [Remarks] 合流性問題のデータベース
  • URL: http://cops.uibk.ac.at/
• [Remarks] 研究代表のホームページ
  • URL: http://www.jaist.ac.jp/~hirokawa/
• [Remarks] 合流性ツール Saigawa
  • URL: http://www.jaist.ac.jp/project/saigawa/