2011 Fiscal Year Annual Research Report
| Project/Area Number |
21700017
|
|---|
| Research Institution | Shimane University |
|---|
Principal Investigator |
岩見 宗弘 島根大学, 総合理工学部, 講師 (70314614)
|
|---|
| Keywords | 項書換えシステム / 高階項書換えシステム / 無限項書換えシステム / 合流性 / 強頭部正規化可能性 / 強収束性 / 生成性 / 一般生成性 |
|---|
| Research Abstract |
ソフトウェアに対する多様な要求に対して,高機能な関数型プログラミング言語(SML#,Haskell,OCaml等)が提案され,それらのプログラミング言語の基礎理論を与えるものとして高階項書換えシステムが注目されるようになった.
昨年度に引き続き,今年度は合流性を満たす高階(無限)項書換えシステムのクラスの拡張・定式化を目標として,項書換えシステムを拡張した無限項書換えシステムの理論的な解析を行った.無限項書換えシステムは,遅延リストやストリームといった仮想的に無限長としてみなされるデータを扱う関数型プログラミング言語の計算モデルとして知られている.項書換えシステムにおける停止性に対応する基本的な性質として,無限項書換えシステムにおける強頭部正規化可能性(強収束性)があり,その証明法がZantemaやEndrullisらによって報告されている.また,Endrullisらは無限項書換えシステムの部分クラスであるストリーム項書換えシステムを提案し,ある十分条件のもとでのストリームの生成性判定手続きを報告している.今年度の具体的な成果は以下のとおりである.
1.強頭部正規化可能性および一般生成性に対する反証手続きを提案した.提案した手続きの基本的なアイデアは,有限表現を持つ無限項である正則項の反例を構成する点にある.
2.反証手続きの正しさを示ととに,手続きの実装を報告した.実験の結果,自動反証法が従来知られていない例について有効であることを確認した.
本研究の成果は,学術雑誌に掲載済みである.
|
