--- a/paper/type.tex	Fri Jan 27 17:10:33 2017 +0900
+++ b/paper/type.tex	Sat Jan 28 09:02:15 2017 +0900
@@ -196,7 +196,9 @@
 項 $ s $ 中の自由変数が項 $ t $ に代入されて束縛される現象は変数捕獲と呼ばれる。
 これを避けるためには $ t $ の束縛変数の名前が $ s $ の自由変数の名前と異なることを保証する必要がある。
 変数捕獲を回避した代入操作は捕獲回避代入と呼ばれる。
-
+代入における名前の衝突を回避するために項の束縛変数の名前を一貫して変更することで変数捕獲を回避する方法も存在する。
+束縛変数の名前を一貫して変更することをアルファ変換と呼ばれる。
+これは関数抽象に対する束縛変数は問わないという直感からくるもので、 $ \lambda x . x $ も $ \lambda y . y $ も振舞いとしては同じ関数であるとみなすものである。
 捕獲回避の条件を追加した代入の定義は以下のような定義となる。
 
 \begin{itemize}
@@ -212,12 +214,6 @@
             [ x \mapsto s ] y = y
         \end{equation*}
 
-    \item 抽象内の項への代入($ y = x $ の場合)
-
-        \begin{equation*}
-            [ x \mapsto s ] (\lambda y . t_1) = \lambda y . t_1
-        \end{equation*}
-
     \item 抽象内の項への代入($ y \neq x $ かつ $ y $ が $ s $ の自由変数でない)
 
         \begin{equation*}
@@ -233,14 +229,23 @@
 \end{itemize}
 
 この定義は少なくとも代入が行なわれる際には正しく代入が行なえる。
+さらに、抽象が束縛している変数を名前では無く数字として扱う名無し表現も存在する。
+これは De Brujin 表現と呼ばれ、コンパイラ内部などでの項表現として用いられる。 % TODO: ref and spell check
 
-また、項の束縛変数の名前を一貫して変更することにより正しく代入を行なう方法もあり、名前の変更をアルファ変換と呼ぶ。
-さらし、抽象が束縛している変数を名前では無く数字として扱う名無しで束縛変数を扱う方法もあり、この数字で束縛変数を扱う表現を De Brujin 表現と呼ぶ。 % TODO: ref and spell check
+最終的に形無しラムダ計算 $ \lambda $ の項の定義と評価の要約を示す。
+% TODO: TaPL 54 の図5-3
 
-形無しラムダ計算 $ \lambda $ の項の定義と評価の要約を示す。
+項は変数かラムダ抽象か関数適用の3つにより構成される。
+また、ラムダ抽象値は全て値である。
+加えて評価は関数適用を行なう E-APPABS 計算規則と、適用の項を書き換える E-APP1 と E-APP2 合同規則により定義される。
+
+% TODO: ラムダの再帰とかペアとかの解説
+
+%TODO ラムダの操作的意味論の説明。それとも算術式を前のセクションに入れるか?
 
 % }}}
 
+\section{単純型}
 \section{単純型付きラムダ計算}
 \section{部分型付け}
 \section{部分型と Continuation based C}