--- a/paper/type.tex	Wed Feb 08 13:50:52 2017 +0900
+++ b/paper/type.tex	Wed Feb 08 14:27:06 2017 +0900
@@ -1,11 +1,19 @@
 \chapter{ラムダ計算と型システム}
 \label{chapter:type}
-\ref{chapter:cbc} では CbC のモデル検査的検証アプローチとして、akasha を用いた有限の要素数の挿入時の仕様の検証を行なった。
+\ref{chapter:akasha} 章では CbC のモデル検査的検証アプローチとして、akasha を用いた有限の要素数の挿入時の仕様の検証を行なった。
+しかし、要素数13個分の挿入を検証しても赤黒木の挿入が必ずバランスするとは断言しづらい。
+
+そこで、 CbC の性質をより厳密に定義し、その上で証明を行なうことを考えた。
+CbC のプログラムを証明できる形に変換し、任意の回数の挿入に対しても性質が保証できるよう証明するのである。
+証明を行なう機構として注目したのが型システムである。
+
+\ref{chapter:type} 章ではCbC の項の形式的な定義の一つとして、部分型を用いて CbC の CodeSegment と DataSegment を定義する。
+また、型システムの別の利用方法として命題が型で表現できる Curry-Howard 対応を利用した証明が存在するが、その利用方法については\ref{chapter:agda}章で述べる。
+
+
 しかし、さらに多くの要素を検証したり無限回の挿入を検証するには状態の抽象化や CbC 側に記号実行の機構を組み込んだり証明を行なう必要がある。
 CbC は直接自身を証明する機構が存在しない。
 プログラムの性質を証明するには CbC の形式的な定義が必須となる。
-\ref{chapter:type} 章ではCbC の項の形式的な定義の一つとして、部分型を用いて CbC の CodeSegment と DataSegment が定義できることを示していく。
-また、型システムの別の利用方法として命題が型で表現できる Curry-Howard 対応を利用した証明が存在するが、その利用方法については\ref{chapter:agda}章で述べる。
 
 % {{{ 型システムとは
 \section{型システムとは}