静的再帰構造解析に基づく関数プログラムの停止性自動証明

2015 Fiscal Year Research-status Report

• Project/Area Number: 24500012
• Research Institution: Gifu University
• Principal Investigator: 草刈 圭一朗 岐阜大学, 工学部, 教授 (90323112)
• Co-Investigator(Kenkyū-buntansha): 坂部 俊樹 名古屋大学, 情報科学研究科, 教授 (60111829) [Withdrawn]
• Project Period (FY): 2012-04-01 – 2017-03-31
• Keywords: 情報基礎 / 関数プログラム / 停止性 / 再帰定義

Outline of Annual Research Achievements

本研究の目標は関数プログラム停止性自動証明ツールの構築であり，関数プログラムとしてはSML(Standard Meta Language)系の関数型言語(SML/NJ, SML#等)を採用することに決定した．これは言語の定義が他の関数型言語に比して厳密に与えられているためである．
本研究の核となる静的な再帰構造解析に基づく停止性証明法である静的依存対法は，すでにSML系言語に対応するよう拡張済みであるが，証明において若干のギャップがあったため再証明を行い現在論文を執筆中である．
さらに，静的依存対法が有効に機能するために必要な簡約化順序，引数切り落とし法，実効規則の3つの理論を構築する．簡約化順序に関しては，平成26年度の成果である重み付き経路順序は高階関数への対応が困難であるため，より取り扱いの容易な辞書式経路順序をSML系言語に対応できるように拡張中である．また，簡約化順序を劇的に強化できる引数切り落とし法の理論はパターン付き関数抽象への対応を残すのみとなっている．また，停止性証明の際に解くべき制約を減少させ，証明能力の増大と計算量の減少に多大な貢献が可能な実効規則の理論もパターン付き関数抽象への対応を残すのみとなっている．
これらの理論を元にした停止性自動証明ツールの構築を現在行なっており，高階関数への対応ができていないものの近年飛躍的に能力を向上させているSMTソルバ(Satisfiability Modulo Theories Solver)との連携に基づいた非常に強力な停止性証明ツールを作成済みである．

Current Status of Research Progress

3: Progress in research has been slightly delayed.

Reason

静的依存対法は若干の修正が必要ではあるがすでに完成している．SML系言語に対応した辞書式経路順序は現在設計中である．引数切り落とし法と実効規則はパターン付き関数抽象への対応を残すのみとなっている．また，SMTソルバとの連携法に基づき非常に強力な停止性証明ツールを作成済みではあるが，本ツールは高階関数への対応がまだできていないために全面的な改良が必要である．

Strategy for Future Research Activity

我々の目標である関数プログラム停止性自動証明ツールは静的な再帰構造解析に基づく停止性証明法である静的依存対法に基づき設計する予定である．残りの構築すべき理論として，SML系言語に対応した辞書式経路順序，引数切り落とし法，実効規則の３つの理論の完成が最優先課題となる．また，完成した理論を実装済みの停止性証明ツールに順次反映していく．