--- a/paper/type.tex	Sat Jan 28 18:29:15 2017 +0900
+++ b/paper/type.tex	Sun Jan 29 11:56:00 2017 +0900
@@ -792,5 +792,99 @@
 % }}}
 
 \section{単純型付きラムダ計算}
+型無しラムダ計算に対して単純型を適用する場合、ラムダ抽象の型について考える必要がある。
+ラムダ抽象は値を取って値を返すため、関数として考えることもできる。
+差し当たりBool型における関数の型を $ \lambda x . t : \rightarrow $ と定義する。
+この定義においては $ \lambda x . true $ についても  $\lambda x . \lambda y . y $ のような型も同一の型を持つ。
+この二つの項は値を適用すると値を返すという点では同じであるが、前者は $ true $ を返し、後者は $ \lambda y . y $ を返す。
+これでは関数を適用した際に返す値の型は関数の型から予測できず、加えてどの値に対して適用可能かも分からない。
+そのために引数にどのような型を期待しているのか、正しい型の値を適用するとどの型の値を返すのかを型情報に追加する。
+具体的には以下のように $ \rightarrow $ を $  T_1 \rightarrow T_2 $ の形をした無限の型の族に置き換える。
+
+\begin{definition}
+    型 Bool 上の単純型の集合は次の文法により生成される。
+
+    \begin{align*}
+        t ::=           && 型 : \\
+        T \rightarrow T && 関数の型 \\
+        Bool            && ブール値型
+    \end{align*}
+\end{definition}
+
+なお、型構築子 $ \rightarrow $ は右結合である。
+つまり $ T_1 \rightarrow T_2 \rightarrow T_3 $ は$ T_1 \rightarrow (T_2 \rightarrow T_3) $となる。
+
+$ \lambda x . t $ に対して型を割り当てる時、明示的に型付けする方法と暗黙的に型付けする方法がある。
+明示的に型付けを行なう場合はプログラマが項に型の注釈を記述する。
+暗黙的に型付けを行なう場合は型検査器に情報を推論させ、型を再構築させる。
+型推論は $ \lambda $ 計算の文献内では型割り当て体系と呼ぶこともある。
+今回は明示的に型を指定する方法を取る。
+
+$ \lambda $ 抽象の引数の型が分かれば、結果の型は本体 $ t_2 $となる。
+ここで、$ t_2 $内における $ x $ の出現は型 $ T_1 $ の項を表すと仮定する必要がある。
+これは引数に対して正しい型の値が渡されたにも関わらず抽象内で異なる型として振る舞うのを禁止するためである。
+この $ \lambda $ 抽象の型付けは以下の T-ABS によって定義される。
+
+
+\begin{align*}
+    \AxiomC{$x : T_1 \vdash t_2 : T_2$}
+    \UnaryInfC{$ \vdash \lambda x : T_1 . t_2 : T_1 \rightarrow T_2$}
+    \DisplayProof && \text{T-ABS}
+\end{align*}
+
+項は抽象を入れ子で持つ可能性があるため、引数の仮定は複数持ちうる。
+このため型付け関係は二項関係 $ t : T $ から、三項関係 $ \Gamma \vdash t : T $ となる。
+ここで $ \Gamma $ とは $ t $ に表われる自由変数の型の仮定の集合である。
+$ \Gamma $ は型付け文脈や型環境と呼ばれ、$ \Gamma \vdash t : T $ は「型付け文脈 $ \Gamma $ において項 $ t$ は型$T$を持つ」と読む。
+空の文脈は $ \emptyset$ と書かえることもあるが、通常は省略して $ \vdash t : T $ と書く。
+また、型環境に対する $ , $ 演算子は $ \Gamma $ の右に新しい束縛を加えて拡張する。
+
+新しい束縛と既に $ \Gamma $ に表われている束縛は混同しないように名前 $ x$は$\Gamma $に存在しない名前から選ばれるものとする。
+これはアルファ変換により$\lambda$抽象の束縛名は一貫して変更ができるため、常に満たせる。
+
+ラムダ抽象に型を持たせる規則の一般的な形は
+
+\begin{align*}
+    \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{T-ABS}
+\end{align*}
+
+であり、変数の型付け規則は
+
+\begin{align*}
+    \AxiomC{$ x : T \in \Gamma $}
+    \UnaryInfC{$ \Gamma \vdash x : T$}
+    \DisplayProof && \text{T-VAR}
+\end{align*}
+
+である。
+$ x : T \in T $ は 、$ \Gamma$において $x$ に仮定された型は $ T $ である、と読む。
+
+最後に関数適用の型付け規則を定義する。
+
+\begin{align*}
+    \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*}
+
+もし $t_1$ が$ T_{11}$の引数を $ T_{12}$の計算結果に移す関数へ評価され、$ t_2$が型$T_{11}$の計算結果にに評価されるのであれば、$t_1$ を $ t_2$に適用した計算結果は $ T_{12}$の型を持つ。
+ブール定数と条件式の型付け規則は型付き算術式と時と同様である。
+
+最終的な型付きラムダ計算の規則を示す。
+
+\begin{definition}
+    $ \rightarrow $ (型付き)の項
+
+    \begin{align*}
+        t ::=             && \text{項} \\
+        x                 && \text{変数} \\
+        \lambda x : T . t && \text{ラムダ抽象} \\
+        t \; t            && \text{関数適用} \\
+    \end{align*}
+\end{definition}
+
 \section{部分型付け}
 \section{部分型と Continuation based C}