--- a/paper/type.tex	Sat Jan 28 15:35:26 2017 +0900
+++ b/paper/type.tex	Sat Jan 28 17:10:51 2017 +0900
@@ -69,7 +69,7 @@
 % {{{ 型無し算術式
 \section{型無し算術式}
 まず、型システムやその性質について述べるためにプログラミング言語そのものの基本的な性質について述べる。
-プログラムの構文と意味論、推論について考えるために整数とブール値のみで構成される小さな言語を扱いながら考察する。
+プログラムの構文と意味論、推論について考えるために自然数とブール値のみで構成される小さな言語を扱いながら考察する。
 この言語は二種類の値しか持たないが、項の帰納的定義や証明、評価、実行時エラーのモデル化を表現することができる。
 
 この言語はブール定数 $ true $ と $ false $ 、条件式、数値定数 0 、算術演算子 $ succ $ と $ pred $ 、判定演算子 $ iszero $ のみからなる。
@@ -275,7 +275,7 @@
 しかし、他の言語における値は一般的に正規形ではない。
 実のところ、値でない正規形は実行時エラーとなって表れる。
 
-実際にこの言語に整数を導入し、値では無い正規形を確認していく。
+実際にこの言語に自然数を導入し、値では無い正規形を確認していく。
 
 
 \begin{definition}
@@ -356,6 +356,90 @@
 
 % }}}
 
+\section{単純型}
+先程定義した算術式には $ pred \; false $ のようなこれ以上評価できない行き詰まり状態が存在する。
+項を実際に評価する前に評価が行き詰まり状態にならないことを保証したい。
+そのために、自然数に評価される項とブール値に評価される項とを区別する必要がある。
+項を分類するために2つの型 Nat と Bool を定義する。
+
+ここで、項$t$が型 $T$を持つ、という表現を用いた場合、$t$を評価した結果が明らかに適切な形の値になることを意味する。
+明らかに、という意味は項を実行することなく静的に分かるという意味である。
+例えば項 $ if \; true \; then \; false \; else \; true $ は Bool 型を持ち、$ pred \; (succ \; (succ \; 0)) $ はNat 型を持つ。
+しかし、項の型の分析は保守的であり、$ if \; true \; then \; 0 \; else \; false $ のような項は実際には行き詰まりにならないが型を持てない。
+
+算術式のための型付け関係は $ t : T $ と書き、項に型を割り当てる推論規則の集合によって定義される。
+具体的な数値とブール値に関する拡張は以下である。
+
+\begin{definition}
+    NB(型付き) の新しい構文形式
+    \begin{align*}
+        T ::= && \text{型 :} \\
+        Bool  && \text{ブール型} \\
+        Nat   && \text{自然数型} \\
+    \end{align*}
+\end{definition}
+
+
+\begin{definition}
+    NB(型付き)の型付け規則
+    \begin{align*}
+        true : Bool  && \text{T-TRUE} \\
+        false : Bool && \text{T-FALSE} \\
+        \AxiomC{$t_1 : Bool$}
+        \AxiomC{$t_2 : T$}
+        \AxiomC{$t_3 : T$}
+        \TrinaryInfC{$if \; t_1 \; then \; t_2 \; else \; t_3 : T$}
+        \DisplayProof && \text{T-IF} \\
+        0 : Nat && \text{T-ZERO} \\
+        \AxiomC{$t_1 : Nat$}
+        \UnaryInfC{$ succ \; t_1 : Nat $}
+        \DisplayProof && \text{T-SUCC} \\
+        \AxiomC{$t_1 : Nat$}
+        \UnaryInfC{$ pred \; t_1 : Nat $}
+        \DisplayProof && \text{T-PRED} \\
+        \AxiomC{$t_1 : Nat$}
+        \UnaryInfC{$ iszero \; t_1 : Bool $}
+        \DisplayProof && \text{T-BOOL}
+    \end{align*}
+\end{definition}
+
+T-TRUE と T-FALSE はブール定数に Bool 型を割り当てている。
+T-IFは条件式の部分にBool型を、部分式に関しては同じ型を要求している。
+これは同じ変数 $ T $ を二回使用することで制約を表している。
+
+また、数に関しては T-ZERO は Nat 型を $ 0 $ に割り当てている。
+T-SUCC と T-PRED は $ t_1 $ が Nat である時に限り Nat 型となる。
+同様に、 T-ISZERO は $ t_1 $ が Nat である時に Bool となる。
+
+\begin{definition}
+算術式のための型付け関係とは、NBにおける規則のすべてのインスタンスを満たす、項と型の二項関係である。
+項$ t $ に対してある型 $ T $ が存在して $ t : T $ である時、 $ t $ は型付け可能である(または正しく型付けされている)という。
+\end{definition}
+
+型無し算術式の評価導出のように型付けも導出可能であり、それも規則のインスタンスの木である。
+型付け関係に含まれる二つ組 $(t, \; T)$は $ t : T $ を結論とする型付け導出により正当化される。
+例えば $ if \; (iszero \; 0) \; then \; 0 \; else \; (pred \; 0) : Nat $ の型付け判断の導出木である。
+
+\begin{prooftree}
+    \AxiomC{}
+    \RightLabel{T-ZERO}
+    \UnaryInfC{$ 0 : Nat$}
+    \RightLabel{T-ISZERO}
+    \UnaryInfC{$ iszero \; 0 : Bool$}
+    \AxiomC{}
+    \RightLabel{T-ZERO}
+    \UnaryInfC{$ 0 : Nat$}
+    \AxiomC{}
+    \RightLabel{T-ZERO}
+    \UnaryInfC{$ 0 : Nat$}
+    \RightLabel{T-PRED}
+    \UnaryInfC{$ pred \; 0 : Bool$}
+    \RightLabel{T-IF}
+    \TrinaryInfC{ if \; (iszero \; 0) \; then \; 0 \; else \; (pred \; 0) : Nat }
+\end{prooftree}
+
+% TODO: 進行と保存
+
 % {{{ 型なしラムダ計算
 \section{型なしラムダ計算}
 計算とは何か、エラーとは何か、を算術式を定義することによって示してきた。
@@ -598,7 +682,6 @@
 
 % }}}
 
-\section{単純型}
 \section{単純型付きラムダ計算}
 \section{部分型付け}
 \section{部分型と Continuation based C}