2006 Fiscal Year Annual Research Report
| Project/Area Number |
16500004
|
|---|
| Research Institution | University of Tsukuba |
|---|
Principal Investigator |
亀山 幸義 筑波大学, 大学院システム情報工学研究科, 助教授 (10195000)
|
|---|
| Keywords | メタ・プログラミング / オブジェクト・プログラム / 定理証明 / 限定継続 / 型システム / コントロール・オペレータ |
|---|
| Research Abstract |
メタ・プログラミング言語の処理系は、メタレベル実行によってオブジェクト・プログラムを生成し、次に、そのプログラムを通常の処理系で実行するという2段階の処理を行う。第1段階の処理においては、メタ・プログラムの実行を表す継続(Continuation)と、オブジェクト・プログラムの実行を表す継続の2つの継続を適切に取り扱うことが必要である。我々は、階層化したshift/resetを用いることにより、これら2種類の継続を適切に表現できるという観測に基づき、今年度は特に、階層化されたshift/resetをもつメタ・プログラム自身に対する型システムの構築を精力的に行った。
まず、階層化shift/resetに対する数学的に厳密な意味論としてCPS変換に基づく意味論を採用した。単純な型システムでは、shift/resetの副作用(side effect)を表現するために、階層化レベルNの指数関数に比例する型変数が必要になってしまい、取り扱いが極めて困難である。我々は、型システムの判断の表記を抜本的にあらためて、木の形の型を簡潔に表現するための「型スキーム」を考案し、任意の階層化レベルをもつshift/resetに対する型システムを構築することに成功した。また、得られた型システムの性質を調べ、健全性、CPS変換との整合性などが成立することを証明した。さらに、shiftをabortオペレータの代用として使っている場合を除き、CPS変換で意味のあるプログラムに変換される任意のプログラムに対して、我々の型システムでは型がつけられることを示した。最後に、この型システムにおける型推論アルゴリズムを設計し、objective caml言語を用いて実装を行った。
来年度は最終年度であるため、研究のまとめとして、階層化shift/resetに基づくメタ・プログラミング言語を設計し、効率的なコード生成を行う多数の例題に対して、信頼性を保証する仕組みを研究する予定である。
|
