| 研究概要 |
本研究の目的は,論理学における証明論の枠組を用いて,現実のコンピュータの機械語コードに論理学的解釈を与え,それを基に,高水準プログラミング言語の機械語コードへのコンパイルおよびその過程で行なわれる種々の最適化に対する論理学的な基礎を与えることである.
本年度は,機械語コードに対応するシーケントスタイルの証明論の確立とその証明論からの抽象機械の抽出のアルゴリズムの確立の研究を行い,以下の結果を得た.(1)低レベルの機械の動作は,前提が一つに限定された左規則のみからなるシーケント計算系の証明簡約と解釈できる.この結果に基づき,機械語を表現する論理学の証明体系である逐次シーケント計算系を構築できる.この計算系と直感主義的命題論理学の自然演繹体型は証明能力として同値であり,したがってこれら証明システム間での証明変換が可能である.(2)これら論理的な成果を,Java言語の抽象機械に適用することにより,Java抽象機械語コードに対応する論理体系を構築し,その論理体系と自然演繹体系間の証明変換を行うアルゴリズムを構築した.
(1)の成果については国際論文誌に発表すべく準備中である.(2)の成果の概要は,2001年度のESOP国際会議にて発表予定である.さらに,本研究で示された論理学による機械語コードの表現というアプローチは,研究の初期の段階であるにもかかわらず,一部の研究者を得,2000年のProof Carrying Code国際ワークショップや第16回京都賞記念ワークショップにての招待講演に招かれ,本研究の成果についての発表を行った.
|
