--- a/paper/agda.tex	Wed Feb 08 17:39:12 2017 +0900
+++ b/paper/agda.tex	Thu Feb 09 12:56:22 2017 +0900
@@ -1,62 +1,10 @@
 \chapter{証明支援系言語 Agda による証明手法}
 \label{chapter:agda}
-\ref{chapter:akasha} 章では CbC のモデル検査的検証アプローチとして、akasha を用いた有限の要素数の挿入時の仕様の検証を行なった。
-しかし、要素数13個分の挿入を検証しても赤黒木の挿入が必ずバランスするとは断言しづらい。
-
-そこで、 CbC の性質をより厳密に定義し、その上で証明を行なうことを考えた。
-CbC のプログラムを証明できる形に変換し、任意の回数の挿入に対しても性質が保証できるよう証明するのである。
-証明を行なう機構として注目したのが型システムである。
+\ref{chapter:type}章ではCbCにおける CodeSegment と DataSegment が部分型で定義できることを示した。
 
 型システムは Curry-Howard 同型対応により命題と型付きラムダ計算が一対一に対応する。
 依存型という型を持つ証明支援系言語 Agda を用いて型システムで証明が行なえることを示す。
 
-% {{{ 型システムとは
-\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 言語は言語仕様として暗黙の型変換を持っている。
-
-型システムを定義することはプログラミング言語がどのような特徴を持つかを決めることにも繋がる。
-
-% }}}
-
 % {{{ 依存型を持つ証明支援系言語 Agda
 
 \section{依存型を持つ証明支援系言語 Agda}