本論文は、コンパイラ最適化におけるプログラム解析およびコンパイラ最適化の正しさの検証ための新たな型理論を、変数間の依存関係を型として抽象化することにより構築する。特に従来課題となっていたループなどにおける再帰的計算を再帰型により抽象化した型システムを静的単一代入方式中間言語において定義し、健全性定理として最適化前後において返り値の型が適切な順序関係を満たすならばプログラムの意味が保存されることの厳密な証明を与える。また提案する型集合のサブセットを導出する型システムを通常の中間言語上で定義し、そのサブセットが静的単一代入方式中間言語より得られる静的情報を包摂することの厳密な証明を与える。

本研究の背景の一つは静的単一代入形式（Static Single Assignment form（SSA形式））を中心としたコンパイラ最適化の発展である。コンパイラ最適化の目的は高速化であり、そのためにあらゆる高度な技術、テクニックが提案・実装されてきた。しかしながら、そのためのプログラム解析および実装の困難さは、最適化が高度化するにつれ深刻化した。より容易に、効率的に最適化を実装を行なえるための形式化は、実装する現場において強く望まれていたと考える。SSA形式とは変数への代入文をすべて一意にする中間言語の一種であり、CytronらIBMの研究者たちにより1980年代後半に提案された。コンパイラ最適化の基本はuse-def解析であり、最適化の適用の多くの場面において用いられる。中間言語をSSA形式に変換することにより、各プログラムポイントでuseされる変数の代入文は一意に定まり、dead code elimination, common subexpression eliminationなど、多くの最適化の適用が簡略化された。このことからSSA形式はコンパイラ最適化における標準的な中間言語として認識され現在に至っている。さらに、use-def解析はコンパイラ最適化だけでなくアセンブラ言語など低レベル言語におけるあらゆるプログラム解析の基本であり、そのためSSA形式はコンパイラ最適化の適用のみではなく、その正しさの検証など、ソフトウエアシステム検証などにも適用され始めている。コンパイラ最適化の適用を主として、SSA形式は、近年アセンブラ言語など低レベル言語におけるプログラム解析において重要性が増しつつある。

本研究のもう一つの背景は、型理論を中心とした基礎理論に基づく低レベル言語におけるソフトウエア検証研究の発展である。インターネットの普及によりネットワーク上をバイナリコードが飛び交い、不特定多数のコンピュータ上で実行されうる現在、バイナリコードなどの低レベル言語における安全性検証が必須の課題となっている。しかしながらBytecode Verifierなどの先進的な安全性検証機構を備えるJavaなどにおいても、Javaのアプレットの欠陥をついたハッキングによる被害などが発生している。そのため近年より精密な検証を目的とした型理論などの厳密な基礎理論に依拠した低レベル言語におけるソフトウエア検証研究が注目を集めている。代表的な例としてNeculaによるProof Carrying Code（PCC）やMorrisettらによるTyped Assembly Language（TAL）などがある。PCCやTALは主に関数型言語研究における様々な成果を応用することにより、メモリ保全、プログラムの異常停止の実行前の検出などの低レベルコードの安全性の検証を試みた。このような方向性はHoareが型理論や数理論理学に基づく検証つきコンパイラ（Verifying Compiler）の構築を21世紀の計算機科学におけるグランドチャレンジとして提唱するなど、計算機科学において大きな潮流となりつつある。

しかしながら、コンパイラ最適化研究においてはSSA形式の登場などを契機として、最適化をより効率よく容易に適用可能にするため、さらには低レベル言語における安全性・正しさの検証のための見通しのよい理論的形式化に関する研究が活発に行なわれているが、残念ながらコントロールフローグラフ上における古典的な形式化の域をこえる従来研究はいまだ存在しない。一方型理論などプログラミング基礎理論に基づく低レベル言語解析は、関数型言語分野における成果を応用することにより行なわれているが、関数型言語と低レベル言語は本質的に異なるため、その試みは容易ではない。

我々は、上記2つの研究背景における課題を解決するためには、従来低レベル言語レベルにおける解析を包摂し、かつ関数型言語における成果に表面的に依拠しない、低レベル言語のための新たな形式的理論体系の構築が必要であると考える。その構築のため本研究は具体的な対象としてコンパイラ最適化の正しさを検証するための理論体系の構築を目指す。その手段として、我々は低レベル言語の解析において最も本質的なものを抽象化し、それらを導出する形式的な体系を構築することを試みる。形式的体系として型理論を用いる。我々のアプローチは型理論に基づき、プログラムの様々な概念を抽象化することにより新たなプログラム解析理論の構築を目指す近年の研究動向に沿うものであるが、コンパイラ最適化などのプログラム変換に対して本格的に型を導入する研究は少ない。抽象化すべき低レベル言語の本質は、前述のように、変数間のuse-def関係などのプログラムに現れる様々なオブジェクトの依存関係である洞察する。

本研究は上記目的・洞察に基づき、コンパイラ最適化における最も基本的な概念であるデータ依存関係（use-def chain）を変数の代入型として抽象化することにより型システムをSSA形式中間言語上において構築し、健全性定理として、もしreturn valueの型が最適化前後において適切な順序関係をみたすならば、プログラムの意味が保存されることの厳密な証明を与えた。さらに、最適化前後の型の変化により、様々な最適化の形式的な定義を与えた。

本論文の貢献は以下の通りである。型システムの構築に当たって、我々は従来研究において低レベル言語レベル言語において形式化困難であった以下の2点:

破壊的代入（ある変数に対して複数のプログラムポイントにおいて代入文が存在しうること）

ループにおける再帰的計算

に対して、

SSA形式を対象言語とし、

再帰的に値が計算される変数に対して、再帰型を与える型システムを構築

することにより理論的形式化を行なうことを試みた。変数の値の計算過程を抽象化した代入型は以下のBNFで定義される。（T1,T2）aopは各算術命令に対応し、 {l1:T1,l2:T2}はSSA形式におるφ関数に対応するものである。さらに、{l1:T1,l2:T2}に対して再帰型を導入する。

T::=α|int（i）|（T1,T2）aop|{l1:T1,l2:T2}|μα.{l1:T1,l2:T2}.

上記の2点は低レベル言語の最も基本的な性質であるが、従来研究においては明確な形式化がなされてこなかったものである。SSA形式に対して型システムなど形式的な体系を導入する研究は我々が知る限り存在せず、また、再帰的計算に対して明示的に再帰型などの抽象化に成功した既存研究は、特に低レベル言語レベルにおいていまだ存在しない。さらに我々はSSA形式自体に対する理論的形式化を試みた。提案する型の内、SSA形式におけるφ関数に対応する型より定義されるサブセットを導出する型システムを通常の中間言語において定義し、その型情報がSSA形式が持つ静的情報と等価であることを証明した。

本研究はアセンブラレベルの低レベル言語の基礎的・本質的な性質に焦点を当て形式化を行った。本論文における成果は、アセンブラ言語などの低レベル言語に対する理論的形式化のための、本質的な第一歩になると考える。

本論文は「AType Theory for Optimizing Compilers」と題し,最適化コンパイラにおけるコンパイラ最適化の正当性検証を取り上げ,型理論を用いた理論的な解析のための枠組を提案し,その理論の強さについて解析を与えたものである。コンパイラ最適化の複雑度が飛躍的に増す中で,最適化変換の正当性検証がますます困難になっている。本論分はその問題を解決するための型体系を構築し,さらにカット除去性,健全性,完全性などの理論解析のための標準的な基準に従って解析を加え,構築した体系が非常に良い性質を持っていることを示している。さらにこの理論を用いて,代表的なコンパイラ最適化のうちのいくつかについて正当性検証の式を導出している。対象としているのはアセンブリ言語を静的単一代入形式（SSA）化したもの,およびSSA化を行わないものである。それぞれに対して非常によい性質を持つ型体系を与えている。

第1章は,序論である。本論文の背景となるプログラミング言語理論を概観し,さらに本論文でとった研究方式の概要を述べている。

第2章は,関連研究について述べている。本論文が位置づけられるべきコンパイラ最適化検証,型理論,より一般にプログラム解析について述べ,その問題点を指摘している。

第3章は,本論文で用いる理論の諸概念,特にSSAに関係する定義を行っている。

第4章は,コンパイラ最適化の正当性検証のための型体系を提案している。対象として,SSA化されたアセンブリ言語を固定し,それに対して代入型と呼ばれる,変数への代入を抽象した型,さらに再帰代入型と呼ばれる,ループなどで複数回行われる代入を表現する型を与えた。さらにそれに対する型推論規則を与えている。この型体系は,カット除去定理を持つことを証明した。さらに,同一の変数に対して複数の型推論が与えられるものの,それらはすべて同等であることを証明した。この結果は型体系の一貫性を示す重要な定理である。さらに,構造同等性を持つ2つのプログラムが同等の型を持つならば,それらは実行結果が同一であることを証明した。これは型体系の健全性を証明する非常に重要な定理である。また,一般的な場合は原理的に不可能なプログラムの同一性について,それがある合理的な条件下では証明可能であることを示した点でも重要である。この型体系を用いることで,定数繰り込みや不要コード除去の最適化が自明なものとして証明されている。本章では,さらにこの体系を拡張して,最適化順序を導入し,同様の方法でさらに広い最適化の正当性検証ができることを示している。

第5章は,アセンブリ言語のSSA化を必要としない前提で,4章と同等の理論の構築ができることを示している。型体系を一段抽象化して再帰代入型と同等の型を定義可能にしている。この型体系のもとで変数が再帰代入型と同等の型に型づけ可能ならば,代表的なSSA化アルゴリズムにより,その変数にφ擬似関数による代入が発生すること（健全性）,さらに変数がSSA化によりφ擬似関数による代入が発生するならば,もとのプログラムが再帰代入型と同等の型に型付け可能であること（完全性）を同時に示している。これらはこの型体系がプログラム解析のためによい性質を持っていることをあらわしており,非常に重要な結果である。

第6章は,結論であり,本論文の成果をまとめているものである。

以上,これを要するに,本論文はコンパイラ最適化の正当性検証を取り上げ,型理論を用いた理論的な解析のための枠組を提案し,その理論の強さについて解析を与えたものである。コンパイラ最適化という非常に複雑なシステムの正当性検証のための型体系の構築は,理論的,実践的に非常に意義のあることであり,情報科学上寄与するところ大である。

したがって,博士（科学）の学位を授与できると認める。