--- a/paper/type.tex	Sun Jan 29 21:58:35 2017 +0900
+++ b/paper/type.tex	Sun Jan 29 22:13:47 2017 +0900
@@ -1024,5 +1024,26 @@
 \end{definition}
 
 レコードを用いることで複数の値を一つの値としてまとめて扱うことができる。
+しかし、引数にレコードを取る場合、その型と完全に一致させる必要がある。
+例えば $ \{ x : Nat \} $ を引数に取る関数に対して $ \{ x : Nat , y : Bool\}$ といった値を適用することができない。
+しかし、直感的には関数の要求はフィールド $x $ が型 $Nat$を持つことのみであり、その部分にのみ注目すると$ \{ x : Nat , y : Bool\}$ も要求に沿っている。
+
+部分型付けの目標は上記のような場合の項を許すように型付けを改良することにある。
+つまり型 $ S $ の任意の項が、型 $ T $ の項が期待される文脈において安全に利用できることを示す。
+この時、$ S $ を $ T $ の部分型と呼び、 $ S <: T $ と書く。
+これは型 $ S $ が型 $ T $よりも情報を多く持っていることを示しており、$S$は$T$の部分型である、と読む。
+$ S <: T $ の別の読み方として、型 $ T $ は型 $ S $ の上位型である、という読み方も存在する。
+
+型付け関係と部分型関係をつなぐための新しい型付け規則を考える。
+
+\begin{align*}
+    \AxiomC{$\Gamma \vdash t : S $}
+    \AxiomC{$ S <: T $}
+    \BinaryInfC{$ \Gamma \vdash t : T$}
+    \DisplayProof && \text { T-SUB}
+\end{align*}
+
+この規則は $ S <: T $ ならば $ S $ 型の要素 $ t$はすべて $ T $の要素であると言っている。
+例えば、先程の $ \{ x : Nat \} $ と $ \{ x : Nat , y : Bool\}$ が $ \{ x : Nat , y : Bool\} <: \{ x : Nat \}$ となるように部分型関係を定義した時に $ \Gamma \vdash \{x=0, y=1\} : \{ x : Nat \}$ を導ける。
 
 \section{部分型と Continuation based C}