| 研究課題/領域番号 |
22500023
|
|---|
| 研究機関 | 東北大学 |
|---|
研究代表者 |
大堀 淳 東北大学, 電気通信研究所, 教授 (60252532)
|
|---|
| 研究分担者 |
森畑 明昌 東北大学, 電気通信研究所, 助教 (10582257)
上野 雄大 東北大学, 電気通信研究所, 助教 (60551554)
|
|---|
| 研究期間 (年度) |
2010-04-01 – 2013-03-31
|
| キーワード | コンパイラ / プログラミング言語処理系 / 最適化 / 証明論 |
|---|
| 研究概要 |
最終年度である平成24年度の研究計画の主なものは以下の３点であった．（A）コンパイルの各中間言語の操作的意味に正確に対応するカット除去システムの定義．具体的には，自然演繹システム及びシーケント計算それぞれが，証明系逐次シーケント計算系と対応す構造を持つ証明系として再定義し，逐次シーケント計算に対して定義したものと同型のカット除去定理を証明することを試みる．（B）各証明変換の再定義及びその正しさの証明自然演繹システムからシーケント計算への証明変換がカット除去に関する性質を保存することを示し，証明変換によって抽出されるコンパイルアルゴリズムの正しさを確立することを目指す．（C) さらに，今後の証明論に基づくコンパイルの総合的な研究への展望を開くことを一般的な目的として，最適化理論の研究やアプリケーションに特化したコンパイルのための証明論的拡張の各点に関する萌芽的な探求のさらなる探求を行う．
（A)に関しては，自然演繹およびシーケント計算のそれぞれのに対してコード証明，値証明，環境証明，トップレベル証明の各概念を導入した証明系の厳密な定義を含むカット除去システムの形式的な定義を完成した．さらにそれらに関してカット除去性の保存性に関する証明を完成させ，（B)で目標とした証明変換によって得られたアルゴリズムの正しさの一側面を確立した．（C)に関しては，データベースやシステムライブラリなどの領域に特化した言語の埋め込み等を系統的に表現するための萌芽的な探求を行なった．
|
| 現在までの達成度 (区分) |
理由
24年度が最終年度であるため、記入しない。
|
| 今後の研究の推進方策 |
24年度が最終年度であるため、記入しない。
|
