Normalization Analysis for Term Rewriting

• Project/Area Number: 17K00011
• Research Category: Grant-in-Aid for Scientific Research (C)
• Allocation Type: Multi-year Fund
• Section: 一般
• Research Field: Theory of informatics
• Research Institution: Japan Advanced Institute of Science and Technology
• Principal Investigator: Hirokawa Nao 北陸先端科学技術大学院大学, 先端科学技術研究科, 准教授 (50467122)
• Project Period (FY): 2017-04-01 – 2021-03-31
• Project Status: Completed (Fiscal Year 2020)
• Budget Amount: ¥4,550,000 (Direct Cost: ¥3,500,000、Indirect Cost: ¥1,050,000); Fiscal Year 2020: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000); Fiscal Year 2019: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000); Fiscal Year 2018: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000); Fiscal Year 2017: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000)
• Keywords: 項書換え / 正規化性 / 正規化戦略 / 定理自動証明 / 完備化 / 合流性 / 自動定理証明 / 情報基礎

Outline of Final Research Achievements

We studied foundational techniques for dealing with infinite data structures such as real numbers and infinite lists. Programs that operate on such infinite data often employ potentially non-terminating functions. Therefore, their evaluation requires a special computation method called lazy evaluation. In this research project we showed that in many cases a program can be turned into another form of a program so that a simple calculation by the leftmost outermost strategy achieves lazy evaluation. We also developed an automatic method for verifying termination of lazy evaluation, which is a crucial property for running programs safely.

Academic Significance and Societal Importance of the Research Achievements

本研究において遅延評価の実現方法とその停止性（正規化性）を解析する枠組み・手法を構築した。遅延評価は関数型プログラミング言語のみならず、数学的な定理を証明する定理証明支援システムにおいても採用されている。実数や無限列などの数学的構造を扱う上で必須の技術であり、本研究はそれらをより良く扱うための計算・演繹機構の理論基盤、より良い自動化の枠組みを与えるための技術基盤の確立に貢献する。

Research Products

• [Int'l Joint Research] University of Innsbruck(オーストリア)
• [Int'l Joint Research] Queen Mary University of London(英国)
• [Int'l Joint Research] University of Innsbruck(オーストリア)
• [Int'l Joint Research] Queen Mary University of London(英国)
• [Int'l Joint Research] University of Innsbruck(オーストリア)
• [Int'l Joint Research] Queen Mary University of London(英国)
• [Journal Article] Abstract Completion, Formalized (2019)
  • Author(s): Nao Hirokawa, Aart Middeldorp, Christian Sternagel, and Sarah Winkler.
  • Journal Title: Journal of Logical Methods in Computer Science Volume: 15(3)
  • Peer Reviewed / Open Access / Int'l Joint Research
• [Presentation] Parallel Closedness Revisited (2020)
  • Author(s): Kiraku Shintani and Nao Hirokawa
  • Organizer: 9th International Workshop on Confluence (IWC 2020)
  • Int'l Joint Research
• [Presentation] Confluence by Critical Pair Analysis Revisited (2019)
  • Author(s): Nao Hirokawa, Julian Nagele, Vincent van Oostrom, and Michio Oyamaguchi
  • Organizer: Proceedings of the 27th International Conference on Automated Deduction
  • Int'l Joint Research
• [Presentation] Cops and CoCoWeb: Infrastructure for Confluence Tools (2018)
  • Author(s): Nao Hirokawa, Julian Nagele, and Aart Middeldorp
  • Organizer: Proceedings of the 9th International Joint Conference on Automated Reasoning, Lecture Notes in Artificial Intelligence 10900, pp. 346-353, 2018
  • Int'l Joint Research
• [Presentation] Confluence Competition 2018 (2018)
  • Author(s): Takahito Aoto, Makoto Hamana, Nao Hirokawa, Aart Middeldorp, Julian Nagele, Naoki Nishida, Kiraku Shintani, and Harald Zankl
  • Organizer: Proceedings of the 3rd International Conference on Formal Structures for Computation and Deduction, Leibnitz International Proceedings in Informatics, pp. 32:1-32:5, 2018
  • Int'l Joint Research / Invited
• [Presentation] Infinite Runs in Abstract Completion (2017)
  • Author(s): Nao Hirokawa, Aart Middeldorp, Christian Sternagel, and Sarah Winkler
  • Organizer: Proceedings of the 2nd International Conference on Formal Structures for Computation and Deduction, Leibnitz International Proceedings in Informatics 84, pp. 19:1-19:16, 2017.
  • Int'l Joint Research
• [Remarks] 研究代表のホームページ
  • URL: http://www.jaist.ac.jp/~hirokawa/
• [Remarks] 合流性ツール Saigawa と CoLL のウェブサイト
  • URL: https://www.jaist.ac.jp/project/saigawa/
• [Remarks] ホームページ
  • URL: https://www.jaist.ac.jp/~hirokawa/
• [Remarks] 合流性ツール Saigawa
  • URL: https://www.jaist.ac.jp/project/saigawa/
• [Remarks] 研究者代表のホームページ
  • URL: https://www.jaist.ac.jp/~hirokawa/