2011 Fiscal Year Annual Research Report
| Project/Area Number |
21300005
|
|---|
| Research Institution | University of Tsukuba |
|---|
Principal Investigator |
亀山 幸義 筑波大学, システム情報系, 教授 (10195000)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
浅井 健一 お茶の水女子大学, 大学院・人間文化創成科学研究科, 准教授 (10262156)
五十嵐 淳 京都大学, 大学院・情報学研究科, 准教授 (40323456)
|
|---|
| Keywords | コード生成 / マルチステージプログラミング / 型システム / 様相論理 / コントールオペレータ / 型推論 / 多相型 / 融合変換 |
|---|
| Research Abstract |
本研究の目的は、コード生成のためのプログラミング言語であるマルチステージ言語の基礎となる計算体系の確立である。
今年度の研究では、まず、昨年度設計した、計算エフェクトを利用するための機構を持つ型付きマルチステージ言語の型システムに対して、型推論アルゴリズムを設計・実装した。この言語では、計算エフェクトを表す型システムを採用しているため、型がかなり複雑になることが多く、型推論の自動化は、現実的なプログラム言語とするための必要条件であったが、本年度の研究により、プログラマは、個々のプログラムの型を明示する必要がなくなり、負担が大幅に軽減した。ただし、現段階では限定継続の「タグ」に対する型を指定する必要がある点など、若干の問題点があるため、さらなる改善が必要である。また、コード生成を行う際にしばしば利用するライブラリ関数の多くは、多相型を持つため、体系の型システムを多相型に拡張する研究を行った。多相型の境界を超える計算エフェクトを禁止することにより、安全性を失わずに多相型を導入できる、という結果を得た。
マルチステージプログラム言語の基礎研究として、2段階のステージを持つ体系を定式化した「メタラムダ計算」に関する研究を行い、その意味論の定式化、ベータ簡約の健全性の証明などを行った。
MetaOCamlなど多くのマルチステージ言語では、コードとしてソースプログラムを生成するため、生成後にコンパイルする必要がある。そこで、コード生成と抽象機械のコードへのコンパイルの2つの操作を融合し、機械語を直接生成するマルチステージプログラム言語を設計し、その正当性を融合変換により厳密に証明した。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
本年度の研究目的は、(1)計算エフェクトを操作する機構を持つマルチステージプログラミング言語の設計、その基礎理論の整備、(2)この言語の実用化(多相型など型システムの拡張、計算エフェクトの拡張などによる表現力の向上)の2点であった。このうち(1)については、昨年度の段階で設計済みであった体系の型推論アルゴリズムを設計・実装し、ほぼ目的を達成した。(2)については、多相型を導入した体系を新たに設計し、型システムの健全性を示すことに成功した。計算エフェクトの拡張については、すでに設計した体系の範囲内で、(局所的な)「状態」を表現できるため、体系を拡張するのではなく、既存体系で多数の例を作る方針に切り替え、実際にプログラム例を作成した。
|
| Strategy for Future Research Activity |
来年度は、最終年度にあたるため、まとめとなる研究を行う。本研究で設計したマルチステージプログラム言語の表現力をさらに高め、多くの有用なコード生成例を与えることを目的とする。また、これまで行ってきた論理学的基礎付けや機械語コードの直接生成、部分計算などの既存成果と有機的に組み合わせて、まとまりのある成果を出すことを目的とする。
|
Research Products
(10 results)
