--- a/paper/type.tex	Sat Jan 28 12:10:35 2017 +0900
+++ b/paper/type.tex	Sat Jan 28 15:35:26 2017 +0900
@@ -446,6 +446,36 @@
 例えば $ (\lambda x . \lambda y . s) \; v \; w $ は $ (\lambda y . [x \mapsto v] s) w $ に簡約され、 $ [y \mapsto w][x \mapsto v]s $ に簡約される。
 なお、複数の引数を取る関数を高階関数に変換することはカリー化と呼ばれる。
 
+% TODO: ラムダの再帰とかペアとかの解説
+
+ラムダ計算の帰納的な項は以下のように定義される。
+
+\begin{definition}
+    $ V $ を変数名の加算集合とする。項の集合は以下を満たす最小の集合 $ T $ である。
+
+    \begin{eqnarray*}
+        任意の x \in V について x \in T \\
+        t_1 \in T かつ x in V ならば \lambda x . t \in T \\
+        t_1 \in T かつ t_2 \in T ならば t_1 \; t_2 \in T
+    \end{eqnarray*}
+\end{definition}
+
+また、形式的な自由変数の定義を与える。
+
+\begin{definition}
+    項 $ t $ の自由変数の集合は $ FV(t)$と書き、以下のように定義される。
+
+    \begin{eqnarray*}
+        FV(x) = \{ x \} \\
+        FV(\lambda  . t_1 x) = FV(t_1) \setminus \{ x \} \\
+        FV(t_1 \; t_2) = FV(t_1) \cup FV(t_2)
+    \end{eqnarray*}
+\end{definition}
+
+記号 $ \setminus $ は集合に対する二項演算子であり、$ S \setminus T := {x \in S : x \notin T}$ である。
+つまり、$ t_1 $の内部の自由変数の集合から $ x $ を抜いた集合である。
+
+最後に代入について定義する。
 代入の操作は直感的には置換であるが、変数の束縛に注意しなくてはならない。
 例えば抽象への代入を以下のように定義する。
 
@@ -523,16 +553,48 @@
 さらに、抽象が束縛している変数を名前では無く数字として扱う名無し表現も存在する。
 これは De Brujin 表現と呼ばれ、コンパイラ内部などでの項表現として用いられる。 % TODO: ref and spell check
 
-最終的に形無しラムダ計算 $ \lambda $ の項の定義と評価の要約を示す。
-% TODO: TaPL 54 の図5-3
+最終的な型無しラムダ計算 $ \lambda $ の項の定義と評価の要約を示す。
+
+\begin{definition}
+    $ \rightarrow $ (型無し)
+
+    項
+    \begin{align*}
+        t ::=         && \text{項} \\
+        \lambda x . t && \text{ラムダ抽象} \\
+        t \; t        && \text{関数適用}
+    \end{align*}
+
+    値
+    \begin{align*}
+        v ::=         && \text{値} \\
+        \lambda x . t && \text{ラムダ抽象値}
+    \end{align*}
+
+    評価( $ t \rightarrow t' $)
+
+    \begin{align*}
+        \AxiomC{$ t_1 \rightarrow t_1'$}
+        \UnaryInfC{$t_1 \; t_2 \rightarrow t_1' t_2$}
+        \DisplayProof && \text{E-APP1} \\
+        \AxiomC{$ t_2 \rightarrow t_2'$}
+        \UnaryInfC{$v_1 \; t_2 \rightarrow v_1 t_2'$}
+        \DisplayProof && \text{E-APP2} \\
+        (\lambda x . t_{12}) \; v_2 \rightarrow [ x \mapsto v_2] t_{12}
+        && \text{E-APPABS}
+    \end{align*}
+\end{definition}
 
 項は変数かラムダ抽象か関数適用の3つにより構成される。
 また、ラムダ抽象値は全て値である。
 加えて評価は関数適用を行なう E-APPABS 計算規則と、適用の項を書き換える E-APP1 と E-APP2 合同規則により定義される。
 
-% TODO: ラムダの再帰とかペアとかの解説
+この定義からも評価戦略と評価順序が分かる。
+関数を適用する E-APPABS は左側が抽象であり、右側が値である $v_2$ の時にしか適用されない。
+逆に、規則 E-APP1 の$t_1$は任意の項にマッチするため関数部分が値でない関数適用に用いる。
+一方、E-APP2 は左辺が値であるようになるまで評価されない。
+よって、関数適用 $ t_1 \; t_2 $ の評価順は、まずE-APP1を用いて$t_1$が値となった後にE-APP2を用いて$t_2$を値とし、最後にE-APPABSで関数を適用を行なう。
 
-%TODO ラムダの操作的意味論の説明。それとも算術式を前のセクションに入れるか?
 
 % }}}