書誌事項
- タイトル別名
-
- レイガイ ショリ オ フクム カンスウガタ プログラム テイシセイ ショウメイ ノ タメ ノ ジョウケン ツキ イソン タイホウ
- Conditional Dependency Pair Method for Proving Termination of Functional Programs with Exception Handling
この論文をさがす
抄録
先に提案した文脈依存項書換え系(CS-TRS)への変換による例外処理を持つ先行評価に基づく関数型プログラムの停止性・非停止性証明法では,変換で得られるCS-TRSの停止性・非停止性証明に汎用の停止性証明ツールを利用すると非常に短いプログラムしか証明に成功しない.そこで,本論文では例外処理を持つ関数型プログラムから変換されたCS-TRSの停止性証明のための新しい手法を提案する.まず,項書換え系(TRS)の停止性証明に用いられる依存対を拡張し,文脈を条件として記述する条件付き依存対を定義する.次に,条件付き依存対から構成される条件付き依存対鎖の存在とCS-TRSの最内停止性が一致することを証明する.さらに,依存グラフを用いた既存の手法を拡張し,条件付き依存対グラフによるCS-TRSの停止性判定手法を提案する.本手法によりこれまで証明ができなかった多くのプログラムの停止性・非停止性が証明可能となる.
収録刊行物
-
- 電子情報通信学会技術研究報告. KBSE, 知能ソフトウェア工学
-
電子情報通信学会技術研究報告. KBSE, 知能ソフトウェア工学 113 (160), 61-66, 2013-07
一般社団法人電子情報通信学会
- Tweet
キーワード
詳細情報
-
- CRID
- 1050845763734814848
-
- NII論文ID
- 110009778534
- 110009778382
-
- NII書誌ID
- AA1123312X
-
- HANDLE
- 2237/23566
-
- ISSN
- 09135685
-
- 本文言語コード
- ja
-
- 資料種別
- journal article
-
- データソース種別
-
- IRDB
- NDL
- CiNii Articles