| 研究概要 |
平成22年度の研究計画の主なものは以下の3点であった.
(A)コンパイルの各中間言語の操作的意味に正確に対応するカット除去システムの定義
具体的には,「コード証明」,「値証明」,「環境証明」,「トップレベル証明」の各概念を,自然演繹システム及びシーケント計算それぞれに導入し,各証明システムを再定義し,さらに,その証明系に対し,カット除去定理を証明することを試みることを計画した.
(B)各証明変換の再定義及びその正しさの証明
具体的には,前項の操作的意味論に正確に対応するカット除去定理の結果を用いて,自然演繹システムからシーケント計算への証明変換がカット除去に関する性質を保存することを示し,証明変換によって抽出されるコンパイルアルゴリズムの正しさ(total correctness)を確立することの2点であった.
(C)実装技術および、最適化理論の研究
(A)に関しては,コンパイラの主要なコンポーネントの一つであるA正規形変換に対してこの目標をほぼ完全に達成し,さらにそれに対して(B)のカット除去の性質の保存定理を証明しることに成功した.(C)に関しては,本研究等の成果を基礎として開発を行っているSML#コンパイラのA-正規化変換の実装に,本研究の一部の結果を試験的に応用し,コンパイラの開発に応用可能であるとの知見を得た.さらに,SML#でのプログラム開発の過程で,本研究における証明論的な考え方に基づき,アプリケーションに特化したコンパイルのための証明論的拡張が可能であること,さらにそれら拡張はゲームプログラムの構築に有望であるとの萌芽的な洞察を得た.
|
