2002 Fiscal Year Annual Research Report
宣言型プログラミング言語のためのAC記号のあるナローイングの計算理論
| Project/Area Number |
14780187
|
|---|
| Research Institution | Tohoku University |
|---|
Principal Investigator |
青戸 等人 東北大学, 電気通信研究所, 講師 (00293390)
|
|---|
| Keywords | 宣言型プログラミング言語 / AC記号 / ナローイング / 項書換え系 / 停止性 / 合流性 |
|---|
| Research Abstract |
まず,本研究の開始にさきだって考案した制約条件を分離したナローイング計算系を実際に宣言型プログラミング言語の計算機構として用いるために必要となる基礎理論についての考察をすすめた.その結果,AC記号を導入した場合を含め,一般的に制約条件の計算が重要であるという認識に至った.本研究の計算系において用いる制約条件の計算は,従来,研究が活発に行われている,単一化のバリエーションとして考えられる.そこで,単一化やそのバリエーション,単一化のモジュラ性等についての調査をすすめることにした.また,高階記号を含む場合の拡張については,考察をすすめた結果,山田(RTA'01,2001)により提案された単純型付き項書換え系が,高階記号への拡張が比較的容易に行えるため,本研究に活用するのに適しているとの結論に至った.しかしながら,単純型付き項書換え系については,基本的な性質についての基盤理論の確立が不十分であることも判明した.特に,完備性について,その一方の条件である合流性については,基本的な結果が報告されていたものの,もう一方の条件である停止性については,自動化の困難な停止性証明技術しか得られていないという,きわめて不十分な状態であることがわかった.そこで,単純型付き項書換え系の停止性証明を行う技法について考察をすすめ,従来手法とは対照的に,停止性証明の自動化が容易に行える手法を考案した.また本手法について,情報処理学会プログラミング研究会において報告を行った.
|
