--- a/paper/type.tex	Sun Jan 29 11:56:00 2017 +0900
+++ b/paper/type.tex	Sun Jan 29 12:27:25 2017 +0900
@@ -791,6 +791,8 @@
 
 % }}}
 
+% {{{ 単純型付きラムダ計算
+
 \section{単純型付きラムダ計算}
 型無しラムダ計算に対して単純型を適用する場合、ラムダ抽象の型について考える必要がある。
 ラムダ抽象は値を取って値を返すため、関数として考えることもできる。
@@ -865,7 +867,7 @@
 
 \begin{align*}
     \AxiomC{$ \Gamma \vdash t_1 : T_{11} \rightarrow T_{12}$}
-    AxiomC{$ \Gamma \vdash t_2 : T_{11}$}
+    \AxiomC{$ \Gamma \vdash t_2 : T_{11}$}
     \BinaryInfC{$ \Gamma \vdash t_1 \; t_2 : T_{12}$}
     \DisplayProof && \text{T-APP}
 \end{align*}
@@ -873,10 +875,12 @@
 もし $t_1$ が$ T_{11}$の引数を $ T_{12}$の計算結果に移す関数へ評価され、$ t_2$が型$T_{11}$の計算結果にに評価されるのであれば、$t_1$ を $ t_2$に適用した計算結果は $ T_{12}$の型を持つ。
 ブール定数と条件式の型付け規則は型付き算術式と時と同様である。
 
-最終的な型付きラムダ計算の規則を示す。
+最終的な純粋単純型付きラムダ計算の規則を示す。
+純粋とは基本型を持たないという意味であり、純粋単純型付きラムダ計算にはブールのような型を持たない。
+この純粋単純型付きラムダ計算でブール値を扱う場合は型環境$\Gamma$を考慮してブール値の規則を追加すれば良い。
 
 \begin{definition}
-    $ \rightarrow $ (型付き)の項
+    $ \rightarrow $ (型付き)の構文
 
     \begin{align*}
         t ::=             && \text{項} \\
@@ -884,7 +888,77 @@
         \lambda x : T . t && \text{ラムダ抽象} \\
         t \; t            && \text{関数適用} \\
     \end{align*}
+
+    \begin{align*}
+       v ::=             && \text{項} \\
+       \lambda x : T . t && \text{ラムダ抽象値} \\
+    \end{align*}
+
+    \begin{align*}
+       T ::=           && \text{型} \\
+       T \rightarrow T && \text{関数型} \\
+    \end{align*}
+
+    \begin{align*}
+       \Gamma ::=     && \text{文脈} \\
+       \emptyset      && \text{空の文脈} \\
+       \Gamma , x : T && \text{項変数の束縛} \\
+    \end{align*}
 \end{definition}
 
+\begin{definition}
+    $ \rightarrow $ (型付き)の評価($ 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_{11} . t_{12}) v_2 \rightarrow [ x \mapsto v_2] t_{12} &&
+        \text{E-APPABS}
+    \end{align*}
+\end{definition}
+
+\begin{definition}
+    $ \rightarrow $ (型付き)の型付け($\Gamma \vdash t : T $)
+
+    \begin{align*}
+        \AxiomC{$ x : T \in \Gamma$}
+        \UnaryInfC{$\Gamma \vdash x : T $}
+        \DisplayProof && \text{T-VAR} \\
+        \AxiomC{$\Gamma , x : T_1 \vdash t_2 : T_2$}
+        \UnaryInfC{$\Gamma \vdash \lambda x : T_1 . t_2 : T_1 \rightarrow T_2$}
+        \DisplayProof && \text{E-ABS} \\
+        \AxiomC{$ \Gamma \vdash t_1 : T_{11} \rightarrow T_{12}$}
+        \AxiomC{$ \Gamma \vdash t_2 : T_{11}$}
+        \BinaryInfC{$\Gamma \vdash t_1 \; t_2 : t_{12}$}
+        \DisplayProof && \text{T-APP}
+    \end{align*}
+\end{definition}
+
+単純型付きラムダ計算の型付け規則のインスタンスも型付き算術式のように導出木をすることで示せる。
+例えば $ (\lambda x : Bool\; x) \; true $ が空の文脈において $ Bool$を持つことは以下の木で表せる。
+
+\begin{prooftree}
+    \AxiomC{$ x : Bool \in x : Bool$}
+    \RightLabel{T-VAR}
+    \UnaryInfC{$x : Bool \vdash x : Bool$}
+    \RightLabel{T-ABS}
+    \UnaryInfC{$\vdash \lambda x : Bool . x : Bool \rightarrow Bool$}
+    \AxiomC{}
+    \RightLabel{T-TRUE}
+    \UnaryInfC{$\vdash true : Bool$}
+    \RightLabel{T-APP}
+    \BinaryInfC{$\vdash (\lambda x : Bool . x) \; true : Bool $}
+\end{prooftree}
+
+純粋型付きラムダ計算の型システムにおいて、閉じた項に対して進行定理と保存定理は成り立つ\ref{Pierce:2002:TPL:509043}\ref{pierce2013型システム入門プログラミング言語と型の理論}。  % FIXME: 進行定理と保存定理の証明。
+閉じた項、という制限が付いているのは $ f \; true $ といった自由変数が存在する項は正規形ではあるが値でないからである。
+しかし、開いた項に関しては評価が行なえないために型システムの検査対象に含まれない。
+
+% }}}
+
 \section{部分型付け}
 \section{部分型と Continuation based C}