| 研究課題/領域番号 |
22500025
|
|---|
| 研究機関 | お茶の水女子大学 |
|---|
研究代表者 |
浅井 健一 お茶の水女子大学, 大学院人間文化創成科学研究科, 准教授 (10262156)
|
|---|
| 研究期間 (年度) |
2010-04-01 – 2015-03-31
|
| キーワード | 自己反映言語 / 部分評価 / プログラム変換 |
|---|
| 研究概要 |
本年度は、マルチステージ言語である MetaOCaml を使って自己反映言語のコンパイルを行った。その結果、MetaOCaml を使ったコンパイルは、ある程度、有効だが限界もあることがわかった。自己反映言語のコンパイルには、第１レベルとしてユーザによって変更されたメタレベルインタプリタのコンパイル、さらに第２レベルとしてその変更されたメタレベルインタプリタのもとでのユーザプログラムのコンパイルがある。本年度、行ったコンパイルは第１レベルのもので、変更されたメタレベルインタプリタをコンパイルすることで、変更された言語セマンティクスのもとでのある程度の効率的な実行を実現できた。この内容は、国内のワークショップにて発表した。
しかし、より進んだ第２レベルのコンパイルは、現在の MetaOCaml では難しいことがわかった。第２レベルのコンパイルを行うためには、MetaOCaml によって生成されたメタレベルインタプリタを、さらに部分評価する必要がある。つまり、MetaOCaml が生成したコードをさらにステージ化する必要がある。これの対処が可能かは来年度の課題である。
また、部分継続に関する理論としては、型主導部分評価の正当性の定式化について研究を進めた。その結果、前年度までに行った定式化は、単に型主導部分評価の型レベルの対応を示したのみで、正当性までは示せていないことが判明した。今年度は、この問題を解決し、名前呼び、値呼び、および限定継続命令を含んだ体系に対する型主導部分評価の正当性を Coq で定式化して完全に証明した。このうち、名前呼び、値呼びの体系についてはモナドを使った直感的に理解しやすい証明を得ることができている。しかし、限定継続命令が入った体系については 2CPS では証明できているものの証明は難解で、モナドを使った証明にはまだ成功していない。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
本研究が目指す３つの目標のうち、ひとつ目の「直接実行されるコードと解釈実行されるコードの共存法の確立」はすでに終了している。ふたつ目の「強力かつ高速なプログラム変換技術の開発と発展」については本年度、マルチステージ言語 MetaOCaml を使うことで、ある程度のコンパイルを実現した。また、３つ目の「部分継続に関する理論の発展」については部分継続命令を含む型主導部分評価について（一部、理解のしやすさの面で問題があるものの）その正当性を Coq で定式化することができた。
|
| 今後の研究の推進方策 |
マルチステージ言語である MetaOCaml を使って自己反映言語のある程度のコンパイルができることは示されたが、変更された言語セマンティクスのもとでコンパイルをしようと思うと MetaOCaml 自身を拡張しなくてはならないことがわかってきた。来年度は、これが技術的にどこまで可能か追求する予定である。また、部分継続命令を含む型主導部分評価の定式化については、現在 2CPS での定式化しかできていない。これをモナドを使った定式化に改良することを試みる。
|
