On Proving Termination of Functional Programs by Static Recursion Analysis

2016 Fiscal Year Annual Research 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

本研究の目標は，関数型プログラム停止性証明のための理論構築と，得られた成果に基づく停止性証明ツールの作成である．具体的には，静的な再帰構造解析に基づく停止性証明法である静的依存対法と，その補助理論となる簡約化順序，引数切り落とし法，実効規則の3つの理論構築であり，得られた理論成果とSMTソルバとの連携に基づいた関数型プログラム停止性証明ツールの作成である．
我々は，項書換え系と呼ばれる計算モデルを拡張し，SML系の関数型言語そのものと呼んでもよい構文を持つ書換えモデルを定式化した．理論的には，高階関数，多相型，代数的データ型，パターンを用いた関数抽象の４つの拡張を行っている．これらの拡張により提案理論の実用性は劇的に向上し，実在のプログラム検証へ多大な貢献が期待できることになる．
一方，この書換えモデル上での静的依存対法の健全性証明が予想以上に困難であり，研究期間内の完全な目標達成ができなかった．なお，パターンを用いた関数抽象への対応を除き，他の3つの補助理論の構築やSMTソルバとの連携に基づいた停止性証明ツールは作成は完了している．静的依存対法の健全性証明のために強計算性の概念を用いた単純型付きラムダ計算の停止性証明を拡張した．これを一般には停止性を持たない我々の書換えモデル上へ適用し，証明が破綻する極小の状況を定式化し，この極小破綻点を巧妙に繋ぐことにより再帰定義を浮かび上がらせる，すなわち，「停止性が破綻するならばプログラマが与えた再帰定義関数が原因となる」という証明を予定より時間がかかったとはいえ与えた．
だが，どうしても技巧的かつ長大なものにならざるをえず，最終年度に投稿した論文は，成果は認めるものの証明が追いきれない，という理由により受理されなかった．現在，再投稿論文のための証明の簡単化を試みているところであり，目標達成までは後３年ほどかかると思われる．

Research Products

• [Presentation] AC Dependency Pairs Revisited (2016)
  • Author(s): YAMADA Akihisa, Christian Sternagel, Rene Thiemann, KUSAKARI Keiichirou
  • Organizer: 25th EACSL Annual Conference on Computer Science Logic (CSL 2016)
  • Place of Presentation: Marseille, France
  • Year and Date: 2016-08-29 – 2016-09-01
  • Int'l Joint Research