--- a/paper/agda.tex	Wed Feb 08 14:27:06 2017 +0900
+++ b/paper/agda.tex	Wed Feb 08 14:49:51 2017 +0900
@@ -1,8 +1,72 @@
 \chapter{証明支援系言語 Agda による証明手法}
 \label{chapter:agda}
-第~\ref{chapter:type}章では形無し算術式と型付き算術式による型システムの定義、ラムダ計算によるプログラミング言語の抽象化、部分型の導入とCbCの型が部分型で示せることを確認した。
-部分型を用いて具体的なCbCの型システムを定義する前に、型システムの一方のメリットである証明について触れる。
-依存型という型を持つ証明支援系言語 Agda を用いて証明が行なえることを示す。
+\ref{chapter:akasha} 章では CbC のモデル検査的検証アプローチとして、akasha を用いた有限の要素数の挿入時の仕様の検証を行なった。
+しかし、要素数13個分の挿入を検証しても赤黒木の挿入が必ずバランスするとは断言しづらい。
+
+そこで、 CbC の性質をより厳密に定義し、その上で証明を行なうことを考えた。
+CbC のプログラムを証明できる形に変換し、任意の回数の挿入に対しても性質が保証できるよう証明するのである。
+証明を行なう機構として注目したのが型システムである。
+
+型システムは Curry-Howard 同型対応により命題と型付きラムダ計算が一対一に対応する。
+依存型という型を持つ証明支援系言語 Agda を用いて型システムで証明が行なえることを示す。
+
+% {{{ 型システムとは TODO: もう少し大ざっぱに説明
+\section{型システムとは}
+型システムとは、計算する値を分類することにでプログラムがある種の振舞いを行なわないことを保証する機構の事である\cite{Pierce:2002:TPL:509043}\cite{pierce2013型システム入門プログラミング言語と型の理論}。
+ある種の振舞いとはプログラム中の評価不可能な式や、言語として未定義な式などが当て嵌まる。
+例えば、gcc や clang といったコンパイラは関数定義時に指定された引数の型と呼び出し時の値の型が異なる時に警告を出す。
+この警告は関数が受けつける範囲以外の値をプログラマが渡してしまった場合などに有効に働く。
+加えて、関数を定義する側も受け付ける値の範囲を限定できるため関数内部の処理を記述しやすい。
+
+型システムで行なえることには以下のようなものが存在する。
+
+\begin{itemize}
+    \item エラーの検出
+
+        文字列演算を行なう関数に整数を渡してしまったり、データの単位を間違えてしまったり、複雑な場合分けで境界条件を見落すなど、プログラマの不注意が型の不整合となって早期に指摘できる。
+        この指摘できる詳細さは、型システムの表現力とプログラムの内容に依存する。
+        多用なデータ構造を扱うプログラム(コンパイラのような記号処理アプリケーションなど)は数値計算のような数種類の単純な型しか使わないプログラムよりも型検査器から受けられる恩恵が大きい。
+        他にも、ある種のプログラムにとっては型は保守のためのツールともなる。
+        複雑なデータ構造を変更する時、その構造に関連するソースコードを型検査器は明らかにしてくれる。
+
+    \item 抽象化
+
+        型は大規模プログラムの抽象化の単位にもなる。
+        例えば特定のデータ構造に対する処理をモジュール化し、パッケージングすることができる。
+        モジュール化されたデータ構造は厳格に定義されたインターフェースを経由して呼び出すことになる。
+        このインターフェースは利用する側に取っては呼び出しの規約となり、実装する側にとってはモジュールの要約となる。
+
+    \item ドキュメント化
+
+        型はプログラムを理解する際にも有用である。
+        関数やモジュールの型を確認することにより、どのデータを対象としているのかといった情報が手に入る。
+        また、型はコンパイラが実行されるために検査されるため、コメントに埋め込まれた情報と異なり常に正しい情報を提供する。
+
+    \item 言語の安全性
+
+        安全性のの定義は言語によって異なるが、型はデータの抽象化によってある種の安全性を確保できる。
+        例えば、プログラマは配列をソートする関数があった場合、与えられた配列のみがソートされ、他のデータには影響が無いことを期待するだろう。
+        しかし、低水準言語ではメモリを直接扱えるため、予想された処理の範囲を越えてデータを破壊する可能性がある。
+        より安全な言語ではメモリアクセスが抽象化し、データを破壊する可能性をプログラマに提供しないという選択肢がある。
+
+    \item 効率性
+
+        そもそも、科学計算機における最初の型システムは Fortran~\ref{Backus:1978:HFI:960118.808380} などにおける式の区別であった。
+        整数の算術式と実数の算術式を区別し、数値計算の効率化を測るために導入されたのである。
+        型の導入により、コンパイラはプリミティブな演算とは異なる表現を用い、実行コードを生成する時に適切な機械語表現を行なえるようになった。
+        昨今の高性能コンパイラでは最適化とコード生成のフェーズにおいて型検査器が収集する情報を多く利用している。
+
+\end{itemize}
+
+型システムの定義には多くの定義が存在する。
+型の表現能力には単純型や総称型、部分型などが存在し、動的型付けや静的型付けなど、言語によってどの型システムを採用するかは言語の設計に依存する。
+例えば C言語では数値と文字を二項演算子 \verb/+/ で加算できるが、Haskell では加算することができない。
+これは Haskell が C言語よりも厳密な型システムを採用しているからである。
+具体的には Haskell は暗黙的な型変換を許さず、 C 言語は言語仕様として暗黙の型変換を持っている。
+
+型システムを定義することはプログラミング言語がどのような特徴を持つか決めることにも繋がる。
+
+% }}}
 
 % {{{ Natural Deduction
 \section{Natural Deduction}
@@ -219,7 +283,7 @@
 
 % }}}
 
-% {{{ Curry-Howard Isomorphism
+% {{{ Curry-Howard Isomorphism TODO: もっと増やす(Agda でラムダ計算を説明する)
 \section{Curry-Howard Isomorphism}
 \label{section:curry_howard_isomorphism}
 \ref{section:natural_deduction}節では natural deduction における証明手法について述べた。