2002 Fiscal Year Annual Research Report
Project/Area Number |
14019007
|
Research Institution | University of Tsukuba |
Principal Investigator |
MIDDELDORP Aart 筑波大学, 電子・情報工学系, 助教授 (30251044)
|
Keywords | 項書換え系 / 記号計算 / 停止性 / 自動化 |
Research Abstract |
停止性を保証する問題は計算機科学の多くの分野で生じる。様々なプログラミング言語においてプログラムが停止することを証明するために、多くの研究がなされてきた。ソフトウェア解析のテクニックであるプログラムの特殊化,部分評価,プログラム変換は、いずれも基盤技術として停止性が必須である。またセーフティクリティカルなシステムでは、正しい動作を保証する必要があるが、このような問題の多くは項書換え系の停止性問題へと帰着させることが可能である。項書換え系の停止性証明の自動化は、従来、単純化順序をベースにしたテクニックを用いていたが、この数年間においては、単純化順序の持つ限界を打破する自動化手法の研究が盛んに行われるようになった。ArtsとGieslの依存対法は、現在注目されている新手法の1つである。依存対法に基づく停止性証明ツールの実現する際には、(1)依存グラフの近似,(2)循環解析,(3)引数フィルタリングの3つの困難がある。最初の2つにより、停止性を証明するために解かなければならない順序制約の集合(連立不等式の一種)の数とサイズが決まる。3つ目により、順序制約の集合を解く際の探索空間のサイズが決まる。これらのサイズと停止性証明の計算コストは比例するが、私たちは新たなアルゴリズムを開発し、そのサイズを劇的に削減することに成功した。このアルゴリズムを停止性自動証明ツールTsukuba Termination Tool上で実装し、数多くの実験を行った。その実験データによりアルゴリズムの有効性が確認された。
|
-
[Publications] Aart Middeldorp: "Approximations for Strategies and Termination"Proceedings of the 2nd International Workshop on Reduction Strategies in Rewriting and Programming, Electronic Notes in Computer Science. 70(6). (2002)
-
[Publications] Jurgen Giesl, Aart Middeldorp: "Innermost Termination of Context-Sensitive Rewriting"Proceedings of the 6th International Conference on Developments in Language Theory, Lecture Notes in Computer Science. (印刷中). (2003)
-
[Publications] Alfons Geser, Aart Middeldorp, Enno Ohlebusch, Hans Zantema: "Relative Undecidability in Term Rewriting, Part 1 : The Termination Hierarchy"Information and Computation. 178(1). 101-131 (2002)
-
[Publications] Alfons Geser, Aart Middeldorp, Enno Ohlebusch, Hans Zantema: "Relative Undecidability in Term Rewriting, Part 2 : The Confluence Hierarchy"Information and Computation. 178(1). 132-148 (2002)