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

機関リポジトリ HANDLE Web Site Web Site オープンアクセス

書誌事項

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

この論文をさがす

抄録

先に提案した文脈依存項書換え系(CS-TRS)への変換による例外処理を持つ先行評価に基づく関数型プログラムの停止性・非停止性証明法では,変換で得られるCS-TRSの停止性・非停止性証明に汎用の停止性証明ツールを利用すると非常に短いプログラムしか証明に成功しない.そこで,本論文では例外処理を持つ関数型プログラムから変換されたCS-TRSの停止性証明のための新しい手法を提案する.まず,項書換え系(TRS)の停止性証明に用いられる依存対を拡張し,文脈を条件として記述する条件付き依存対を定義する.次に,条件付き依存対から構成される条件付き依存対鎖の存在とCS-TRSの最内停止性が一致することを証明する.さらに,依存グラフを用いた既存の手法を拡張し,条件付き依存対グラフによるCS-TRSの停止性判定手法を提案する.本手法によりこれまで証明ができなかった多くのプログラムの停止性・非停止性が証明可能となる.

収録刊行物

詳細情報

問題の指摘

ページトップへ