@article{oai:nagoya.repo.nii.ac.jp:00019059,
 author = {濱口, 毅 and 酒井, 正彦 and 馬場, 正貴 and 阿草, 清滋 and Hamaguchi, Takeshi and Sakai, Masahiko and Baba, Masataka and Agusa, Kiyoshi},
 issue = {2},
 journal = {情報処理学会論文誌, プログラミング},
 month = {Mar},
 note = {本論文では,例外処理を持つ先行評価に基づく関数型プログラムの停止性・非停止性証明法を提案する.停止性と非停止性を保存する関数型プログラムの文脈依存項書き換え系 (CS-TRS) への変換法を与える.これにより,近年開発が進んでいる既存の CS-TRS の停止性証明ツールを用いることが可能になる.先行評価での実行においては,関数の引数を先頭から順に評価してから関数の値を計算するため,生成される書き換え系においては,この評価は基本的には最内評価に対応する.しかし,停止性を持たない引数と例外を発生させる引数の順序によって停止性に影響を与えるため,引数の評価順を厳密に考慮する必要がある.そのため,文脈依存の機能を用いて引数の評価順を制御する.また,例外が発生した場合には,それ以降の評価を止めて,例外が処理されるまで例外値を戻す必要がある.これを行えるように書き換え規則を生成する.また,この変換の健全性,すなわち変換後の CS-TRS が最内停止性を持てばプログラムも停止性を持つことと,完全性,すなわちプログラムが停止性を持つならば変換後の CS-TRS も最内停止性を持つことを示す.これにより,変換後の CS-TRS の最内 (非) 停止性が示すことができれば,プログラムの (非) 停止性が証明されることが保証される., We present a proving method of termination/non-termination for functional programs based on eager-evaluation with exception handling. We give a transformation of functional programs into Context-Sensitive Term Rewriting Systems (CS-TRSs). This enables us to use recent-developed termination provers for CS-TRSs as termination provers for functional programs. Since eager-evaluation computes a return value of a function after all values of its arguments are computed in right-to-left order, this evaluation corresponds to the innermost reduction on generated TRSs. The termination property is affected by the occurrences of non-terminating argument and exception-raising argument. This means that we have to handle the evaluation order strictly. Thus we used context sensitiveness for this purpose and design the transformation producing rewrite rules, that repeatedly pass back an exception to the caller until it is handled when exception occurs. We prove the soundness and completeness of the transformation, that is, the innermost termination of the CS-TRS implies the termination of the program and vise versa. This allows us to prove (non-)termination of programs by proving (non-)termination of CS-TRSs.},
 pages = {13--30},
 title = {例外処理を持つ関数型プログラムの停止性・非停止性証明法},
 volume = {4},
 year = {2011}
}