例外処理を含む関数型プログラム停止性証明のための条件付き依存対法

IR HANDLE Web Site Web Site Open Access

Bibliographic Information

Other Title
  • レイガイ ショリ オ フクム カンスウガタ プログラム テイシセイ ショウメイ ノ タメ ノ ジョウケン ツキ イソン タイホウ
  • Conditional Dependency Pair Method for Proving Termination of Functional Programs with Exception Handling

Search this article

Abstract

We have recently proposed a method for proving termination/non-termination properties of eager-evaluation-based functional programs with exception handling. The method transforms them into Context-Sensitive Term Rewriting Systems (CS-TRSs) in preserving the properties. However we encounter a problem that the existing termination provers for CS-TRSs fail even if a very short program is given. In this paper, we present a dependency method specialized for CS-TRSs transformed from functional programs with exception handling. We introduce conditions that represent context information into the dependency pairs, and define conditional dependency chains. We prove that the target CS-TRS is inner-most terminating if and only if there exists no infinite conditional dependency chain. Moreover, we augment graph notion into the framework of the dependency pair problems, and propose some new processors. The new method works effectively for CS-TRSs produced by the transformation.

IEICE Technical Report;SS2013-23,IEICE Technical Report;KBSE2013-23

Journal

Keywords

Details 詳細情報について

Report a problem

Back to top