Normalization Analysis for Term Rewriting

2020 Fiscal Year Final Research Report

• 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
• 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.

Free Research Field

計算モデル

Academic Significance and Societal Importance of the Research Achievements

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