On Proving Termination of Functional Programs by Static Recursion Analysis

2016 Fiscal Year Final Research Report

• 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(Renkei-kenkyūsha): SAKAI Masahiko 名古屋大学, 情報科学研究科, 教授 (50215597) ; NISHIDA Naoki 名古屋大学, 情報科学研究科, 准教授 (00397449)
• Project Period (FY): 2012-04-01 – 2017-03-31
• 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.

Free Research Field

情報基礎