| 研究課題/領域番号 |
23220001
|
|---|
| 研究機関 | 東京大学 |
|---|
研究代表者 |
小林 直樹 東京大学, 情報理工学(系)研究科, 教授 (00262155)
|
|---|
| 研究分担者 |
篠原 歩 東北大学, 情報科学研究科, 教授 (00226151)
五十嵐 淳 京都大学, 情報学研究科, 教授 (40323456)
海野 広志 筑波大学, システム情報工学研究科(系), 助教 (80569575)
|
|---|
| 研究期間 (年度) |
2011-04-01 – 2016-03-31
|
| キーワード | 高階モデル検査 / プログラム検証 / 関数型プログラム / 高階文法 / データ圧縮 |
|---|
| 研究実績の概要 |
本課題では、高階モデル検査とその応用について、（１）高階モデル検査の理論とその高階モデル検査器の構築への応用、（２）プログラム検証への応用、（３）データ圧縮への応用、を３つの柱として研究している。以下、それぞれについて25年度（ただし24年度の繰り越し期間分として報告済みの内容は除く）から繰越期間中の26年度の実績を述べる。
（１）高階モデル検査の理論：高階モデル検査の検証対象のモデルである高階文法の性質について研究を行い、オーダー２の高階文法によって生成される木言語が文脈依存であることを証明した。また、値呼び高階プログラムのモデル検査問題の計算量が型の「深さ」に関して多重指数時間であることを示した。この結果により、これまでは関数型プログラムを検証するのに、継続渡し変換(CPS変換）を介して名前呼びプログラムに変換してからモデル検査を行っていたのに対し、値呼びプログラムに対して直接モデル検査を行った方がよい可能性があることがわかった。
（２）プログラム検証への応用：高階モデル検査の新たな応用として、高階関数型プログラムの停止性検証、高階並行プログラムの同時到達可能性検証の手法を示し、実装・実験を通してその有効性を示した。これらの検証は、いずれも高階モデル検査を用いて初めて実現できたものである。また、高階モデル検査のモデルに再帰型を許した拡張高階モデル検査のための新しいアルゴリズムとして、オートマトンによる抽象化を用いる手法を考案し、実装・実験を通して有効性を示した。
（３）データ圧縮への応用：木構造データを、それを生成する関数型プログラム（ラムダ式）の形で圧縮する方式について、圧縮アルゴリズムの改良を行った。具体的には、通常の文法圧縮で用いられているRePairアルゴリズムの考え方を用いた高速化、ラムダ式をビット表現に変換する際の型情報を用いた最適化などを行った。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
高階モデル検査の理論については、高階文法の性質に関する論文がETAPS 2014でEATCS Best Paper Award を受賞するなど、国際的に極めて高く評価されており、当初の計画以上に成果がでている。
プログラム検証への応用についても、LICS 2015, ESOP 2014, CONCUR 2014などの一流の国際会議に論文が採択され、従来手法ではできなかった検証を高階モデル検査により実現しており、順調に進展している。
データ圧縮への応用については、もともと萌芽的なテーマであることもあり、圧縮率の向上に関して若干難航し、いろいろなアイデアを試しているところであるが、データ圧縮に関する国際会議DCCでポスター発表をするなど、概ね順調に進展している。
以上から、全体としては、おおむね順調に進展していると判断する。
|
| 今後の研究の推進方策 |
引き続き計画に従って研究を遂行する。
データ圧縮への応用に関しては、圧縮効率の改善の点で若干難航しているが、圧縮対象として用いているデータに詳しいゲノムデータ処理や自然言語処理などの専門家とも連携をとって、さまざまな改良案を試す。
|
