文献

J-GLOBAL ID：201102257678534413   整理番号：11A1900657

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

Proving Method of Termination/Non-Termination for Functional Programs with Exception Handling

著者 (4件)： 濱口毅 (名古屋大) ,  酒井正彦 (名古屋大) ,  馬場正貴 (名古屋大) ,  阿草清滋 (名古屋大)
資料名： 情報処理学会論文誌トランザクション(CD-ROM)  (情報処理学会論文誌 Computer Vision and Applications(CD-ROM))
巻： 2010  号： 2  ページ： ROMBUNNO.PUROGURAMINGU,VOL.4,NO.2,13-30  発行年： 2011年04月15日 
JST資料番号： L7379A  ISSN： 1882-7772  資料種別： 逐次刊行物 (A)
記事区分： 原著論文  発行国： 日本 (JPN)  言語： 日本語 (JA)

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

シソーラス用語： *関数プログラミング ,  *停止問題 ,  *項書換え系 ,  依存性 ,  定理証明 ,  支援プログラム ,  変数 ,  健全性 ,  完全性 ,  文脈依存性
準シソーラス用語： 関数型プログラム ,  ソフトウェアツール ,  引数

分類 (2件)： 計算機システム開発  (JD02010R) ,  計算理論  (JB02000A)

引用文献 (7件)：

• 1) 住井英二郎,大根田裕一,米澤明憲:例外処理機構を備えた命令型言語のCPS変換とその定式化,情報処理学会論文誌プログラミング,Vo1.45, No,SIG 12(PRO 23).
• 2) Benton, N. and Kennedy, A.: Exception Syntax, Journal of Functional Program-ming, Vol.4, No.11, pp.395-410 (2001).
• 3) SchrOder, L. and Mossakowski, T.: Generic Exception Handling and the Java Monad, Proc. Algebraic Methodology and Software Technology 10th International Conference AMAST 2004, Lecture Notes in Computer Science 3116, Stirling, UK,pp.443-459 (2004).
• 4) 馬場正貴,酒井正彦,濱口毅,西田直樹,坂部俊樹,草刈圭一朗:例外処理を持つ関数型プログラムの停止性証明法,第12回プログラミングおよびプログラミング言語ワークショップPPL2010論文集, p.81(2010).
• 5) Giesl, J., Thiemann, R., Schneider-Kamp, P. and Falke, S.: Automated Termi-nation Proofs with AProVE, Proc. 15th International Conference on Rewriting Techniques and Applications (RTA-04), Lecture Notes in Computer Science 3091, Aachen, Germany, pp.210-220 (2004).

タイトルに関連する用語 (4件)： 例外処理 ,  関数 ,  停止性 ,  証明