2011 Fiscal Year Annual Research Report
高階再帰スキームのモデル検査とそのプログラム検証への応用
| Project/Area Number |
10J03842
|
|---|
| Research Institution | Tohoku University |
|---|
Principal Investigator |
塚田 武志 東北大学, 大学院・情報科学研究科, 特別研究員(DC1)
|
|---|
| Keywords | 高階再帰スキーム / モデル検査 / プログラム検証 / 型理論 / ゲーム意味論 |
|---|
| Research Abstract |
本年度も、前年度に引き続いて、理論的な側面の研究を行った。引き続き高階再帰スキームと正規言語の包含判定の決定可能性という結果を拡張するとともに、決定可能性を示すための基礎となっている共通型システムそのものについても研究を行った。具体的には次の通り。
1.高階再起スキームと超決定性言語の包含判定の決定可能性の理論の拡張
前年度に得られた結果の一般化を行った。まず、前年度の研究である文脈自由言語と超決定性言語の包含判定であったが、これの右辺を超決定性言語から一般の文脈自由言語へと拡張した。一般には文脈自由言語同士の包含判定問題は決定不能であることが知られているが,包含判定が決定可能となる十分条件を与え、これが前年度の結果がこの枠組みから与えられることを示した。
2.共通型システムとゲーム意味論の対応関係
プログラムの意味を解析するためのアプローチに共通型システムとゲーム意味論というものがあるが、この2つのアプローチの対応関係をはじめて与えた。形式的な対応関係が知られる前から2つのアプローチを組み合わせることの有効性が示されており(例えば[Kobayashi FoSSaCS 2011]ではゲーム意味論の直感を使うことで共通型システムの型付け可能性判定器の高速化が行われている)、本研究はこの統合的アプローチを強力に進めるための鍵となる重要な結果である。
この研究を進めるために、Oxford大学のC.-H.Luke Ong氏の下に3ヶ月間滞在し、研究遂行および意見交換を行った。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
交付申請書に記載した研究目標はすべて達成され、さらに実績2に関しては予想されてしたよりも広い応用先が見えるなど、当初の期待を超える成果が得られた。この点においては「(1)当初の計画以上に進展している」と評価することもできるが、実績1の成果の対外発表が当初計画よりも遅れており、これをもって総合的には「(2)おおむね順調に進展している」と評価できる。
|
| Strategy for Future Research Activity |
研究計画の通り、これまでに得られた基礎的結果の応用的な研究を行う。その際に特に鍵となるのは、今年度の研究実績(2)の「共通型システムとゲーム意味論の対応関係」である。具体的な課題としては、(a)高階再帰スキームのモデル検査器のアルゴリズムの解析やその高速化、(b)プログラム検証を高階再帰スキームのモデル検査に帰着するプログラム変換がモデル検査の困難さに与える影響の調査、などが挙げられる。
|
Research Products
(1 results)
