| 研究概要 |
本研究では,論理学における証明論の枠組を用いて,現実のコンピュータの機械語コードに論理学的解釈を与え,それを基に,高水準プログラミング言語の機械語コードへのコンパイルおよびその過程で行なわれる種々の最適化に対する論理学的な基礎を与えることを目的とし研究を行ない,以下の3つの結果を得た.
(1)低レベルの機械の動作は,前提が一つに限定された左規則のみからなるシーケント計算系の証明簡約と解釈できる.この結果に基づき,機械語を表現する論理学の証明体系である逐次シーケント計算系を構築できる.この計算系と直感主義的命題論理学の自然演繹体型は証明能力として同値であり,したがってこれら証明システム間での証明変換が可能である.この洞察に基づき,機械語コードの証明体型を構築した.
(2)これら論理的な成果を,Java言語の抽象機械に適用することにより,Java抽象機械語コードに対応する論理体系を構築し,その論理体系と自然演繹体系間の証明変換を行うアルゴリズムを構築した.
(3)型推論の枠組みにより機械語コードの解析を行っているAlan Mycroftと共同で,本研究における論理学的方法とMycroftによる型推論による方法の関係を分析し,その結果,論理学的方法は機械語コードの制御の流れの分析において型推論より強力かつ一般的であること,しかし,データ型に依存する解析を必要とする場合型推論による方法が必要であることを明らかにし,両者を統合した枠組みの構築が可能であることを示した.
|
