2008 Fiscal Year Annual Research Report
コード言語の最適化技術と検証技術を統合する証明システムの研究
| Project/Area Number |
19500021
|
|---|
| Research Institution | Tohoku University |
|---|
Principal Investigator |
大堀 淳 Tohoku University, 電気通信研究所, 教授 (60252532)
|
|---|
| Keywords | プログラミング言語 / コード最適化 / コード検証 / 証明論 |
|---|
| Research Abstract |
本研究の最終的な目的は, 機械語コードの論理学的解釈を基礎とし, コードの利用や, 最適化, 検証などを統一的に行うことを可能にする系統的な枠組みを構築することである. 特に, コードの最適化と検証を統一的に扱う論理学的枠組みの確立とそれに基づく最適化と検証技術の構築し, それによって, ラムダ計算の型理論が果たしたと同様に, 低レベルコードに対しても, その安全性の検証やより効率的なコードへの最適化などを系統的に行うことを可能にする基礎理論の確立である. 本年度は, 昨年度に完成させた機械語コードの証明論及び以前の研究成果であるコンパイルの論理学的基礎を, コード生成システムに応用する研究を行い, 制御フローの合流を取り扱うための計算系と, その計算系から導出される中間表現を構築した. 従来の関数型言語の中間表現として使用される継続渡し形式やA-正規形などでは, 条件分岐後に制御フローを合流する機構が含まれていないため, 条件式などを機械的に翻訳すると, 分岐の後に続く計算が各分岐に複製されてしまう. この問題は, それら中間表現に対応する計算系に, 分岐後の制御フローの合流に相当する規則を追加することで解決できるはずである. 本研究では, この洞察に基づき, 論理和に関する規則を左規則が唯一の上式を持つように変更したシーケント計算を構築し, その結果から, 制御フローの合流を取り扱うことができるコンパイラの中間表現とその型システム, およびラムダ計算からこの中間表現への効率の良いコンパイルアルゴリズムを導いた. この成果は関数型言語の実用的なコンパイラのより系統的な実現を可能にするものである.
|
