例外処理を持つ関数型プログラムの停止性・非停止性証明法

概要

論文の詳細を見る
本論文では,例外処理を持つ先行評価に基づく関数型プログラムの停止性・非停止性証明法を提案する.停止性と非停止性を保存する関数型プログラムの文脈依存項書き換え系 (CS-TRS) への変換法を与える.これにより,近年開発が進んでいる既存の CS-TRS の停止性証明ツールを用いることが可能になる.先行評価での実行においては,関数の引数を先頭から順に評価してから関数の値を計算するため,生成される書き換え系においては,この評価は基本的には最内評価に対応する.しかし,停止性を持たない引数と例外を発生させる引数の順序によって停止性に影響を与えるため,引数の評価順を厳密に考慮する必要がある.そのため,文脈依存の機能を用いて引数の評価順を制御する.また,例外が発生した場合には,それ以降の評価を止めて,例外が処理されるまで例外値を戻す必要がある.これを行えるように書き換え規則を生成する.また,この変換の健全性,すなわち変換後の CS-TRS が最内停止性を持てばプログラムも停止性を持つことと,完全性,すなわちプログラムが停止性を持つならば変換後の CS-TRS も最内停止性を持つことを示す.これにより,変換後の CS-TRS の最内 (非) 停止性が示すことができれば,プログラムの (非) 停止性が証明されることが保証される.
2011-03-25

例外処理を持つ関数型プログラムの停止性・非停止性証明法

スポンサーリンク

概要

著者

関連論文

スポンサーリンク