On Proving Termination of Functional Programs by Static Recursion Analysis

• Project/Area Number: 24500012
• Research Category: Grant-in-Aid for Scientific Research (C)
• Allocation Type: Multi-year Fund
• Section: 一般
• Research Field: Fundamental theory of informatics
• Research Institution: Gifu University (2013-2016); Nagoya University (2012)
• Principal Investigator: Kusakari Keiichirou 岐阜大学, 工学部, 教授 (90323112)
• Co-Investigator(Kenkyū-buntansha): 坂部 俊樹 名古屋大学, 情報科学研究科, 教授 (60111829)
• Co-Investigator(Renkei-kenkyūsha): SAKAI Masahiko 名古屋大学, 情報科学研究科, 教授 (50215597) ; NISHIDA Naoki 名古屋大学, 情報科学研究科, 准教授 (00397449)
• Project Period (FY): 2012-04-01 – 2017-03-31
• Project Status: Completed (Fiscal Year 2016)
• Budget Amount: ¥5,070,000 (Direct Cost: ¥3,900,000、Indirect Cost: ¥1,170,000); Fiscal Year 2016: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000); Fiscal Year 2015: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000); Fiscal Year 2014: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000); Fiscal Year 2013: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000); Fiscal Year 2012: ¥780,000 (Direct Cost: ¥600,000、Indirect Cost: ¥180,000)
• Keywords: 関数型プログラム / 停止性 / 再帰定義 / 情報基礎 / 関数プログラム

Outline of Final Research Achievements

We formalize a rewriting model for functional programs, which can represent the notions of higher-order function, polymorphic type, algebraic data type, and functional abstraction with pattern. We extend the static dependency pair method, which proves the termination by analyzing a static recursive structure, onto this rewriting model. In order that this method gives full play to its ability, we also extend reduction orders, the argument filtering method, and the notion of usable rules, although present results do not handle functional abstraction with pattern. Since the syntax of our rewriting model is very close to SML-like functional programs, our result can expect the effective applicability to verification for existing functional programs.

Research Products

• [Journal Article] A Unified Ordering for Termination Proving (2014)
  • Author(s): YAMADA Akihisa, KUSAKARI Keiichirou, SAKABE Toshiki
  • Journal Title: Science of Computer Programming Volume: In Press, Corrected Proof Pages: 1-38
  • Peer Reviewed / Open Access / Acknowledgement Compliant
• [Journal Article] Static Dependecy Pair Method in Rewriting Systems for Functional Programs with Product, Algebraic Data, and ML-Polymorphic Types (2013)
  • Author(s): KUSAKARI Keiichirou
  • Journal Title: IEICE Transactions on Information and Systems Volume: E96-D Pages: 472-480
  • NAID: 110009569242
  • Peer Reviewed
• [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
  • Int'l Joint Research
• [Presentation] Nagoya Termination Tool (2014)
  • Author(s): YAMADA Akihisa, KUSAKARI Keiichirou, SAKABE Toshiki
  • Organizer: n Proc. Joint 25th International Conference on Rewriting Techniques and Applications and 12th International Conference on Typed Lambda Calculi and Applications
  • Place of Presentation: Vienna (Austria)
  • Year and Date: 2014-07-15
• [Presentation] Size Complexity of BDD Construction of Pseudo-Boolean Constraints in binary/mixed-radix Base Form (2014)
  • Author(s): Naoki Nagatsuka, Masahiko Sakai, Zankl Harald, Keiichirou Kusakari
  • Organizer: The 28th Annual Conference of the Japan Society of Artifical Intelligence
  • Place of Presentation: 松山
  • Year and Date: 2014-05-12
• [Presentation] Partial Status for KBO (2013)
  • Author(s): YAMADA Akihisa, KUSAKARI Keiichirou, SAKABE Toshiki
  • Organizer: In Proc. of the 13th International Workshop on Termination (WST2013)
  • Place of Presentation: Bertinoro, Italy
• [Presentation] Unifying the Knuth-Bendix, Recursive Path and Polynomial Orders (2013)
  • Author(s): YAMADA Akihisa, KUSAKARI Keiichirou, SAKABE Toshiki
  • Organizer: In Proc. of the 15th International Symposium on Principles and Practice of Declarative Programming (PPDP2013)
  • Place of Presentation: Madrid, Spain
• [Presentation] 手続き型プログラムから書換え系への変換における停止性をより保存するためのループ不変式の利用 (2013)
  • Author(s): 片岡巧, 西田直樹, 酒井正彦, 坂部俊樹, 草刈圭一朗
  • Organizer: 平成25年度電気関係学会東海支部連合大会
  • Place of Presentation: 静岡大学 浜松キャンパス
• [Presentation] 単純型付き項書換え系における帰納的定理自動証明の局所戦略について (2013)
  • Author(s): 神谷尚史, 草刈圭一朗, 酒井正彦, 坂部俊樹, 西田直樹
  • Organizer: 平成25年度電気関係学会東海支部連合大会
  • Place of Presentation: 静岡大学 浜松キャンパス
• [Presentation] カリー化を組み込んだ高階辞書式経路順序の設計 (2013)
  • Author(s): 松原穂波, 草刈圭一朗, 酒井正彦, 坂部俊樹, 西田直樹
  • Organizer: 平成25年度電気関係学会東海支部連合大会講演論文集
  • Place of Presentation: 静岡大学 浜松キャンパス
• [Presentation] 静的依存対法 －再帰定義は定義か？－ (2013)
  • Author(s): 草刈圭一朗
  • Organizer: 第15回プログラミングおよび言語ワークショップ(PPL2013)
  • Place of Presentation: 会津若松
• [Presentation] 単純型付き項書換え系の停止性証明におけるカリー化の利用 (2012)
  • Author(s): 倉田佳佑, 草刈圭一朗, 酒井正彦, 坂部俊樹, 西田直樹
  • Organizer: 平成24年度電気関係学会東海支部連合大会
  • Place of Presentation: 豊橋技術科学大学
• [Presentation] Static Dependecy Pair Method in Rewriting Systems for Functional Programs with Product, Algebraic Data, and ML-Polymorphic Types (2012)
  • Author(s): KUSAKARI Keiichirou
  • Organizer: 電子情報通信学会ソフトウェアサイエンス研究会
  • Place of Presentation: 愛媛大学