--- a/paper/type.tex	Sun Jan 29 12:27:25 2017 +0900
+++ b/paper/type.tex	Sun Jan 29 21:58:35 2017 +0900
@@ -961,4 +961,68 @@
 % }}}
 
 \section{部分型付け}
+単純型付きラムダ計算では、ラムダ計算の項が型付けされることを確認した。
+ここで、 単純型の拡張として、レコードを導入する。
+
+レコードとは名前の付いた複数の値を保持するデータである。
+C 言語における構造体などがレコードに相当する。
+値を保持する各フィールド $ t_1 $ はあらかじめ定められた集合 L からラベル $ l_i$ を名前として持つ。
+例えば $ { x : Nat } $ や $ {no : 100, point 33}$ などがこれに相当する。
+なお、あるレコードの項や値に表れるラベルはすべて相異なるとする。
+レコードから値を取り出す際にはラベルを指定して値を射影する。
+
+レコードの拡張の定義は以下である。
+
+\begin{definition}
+    レコードの拡張に用いる新しい構文形式
+
+    \begin{align*}
+        t :: = ...                    && \text{項 :} \\
+        \{l_i = t_i^{\; i \in 1 .. n}\} && \text{レコード} \\
+        t.l                           && \text{射影} \\
+    \end{align*}
+
+    \begin{align*}
+        v :: = ...                  && \text{値 :} \\
+        {l_i : v_i^{\; i \in 1..n}} && \text{レコードの値}
+    \end{align*}
+
+    \begin{align*}
+        T :: = ...                  && \text{型 :} \\
+        \{l_i : T_i^{\; i \in 1..n}\} && \text{レコードの型}
+    \end{align*}
+\end{definition}
+
+\begin{definition}
+    レコードの拡張に用いる新しい評価規則
+
+    \begin{align*}
+        \{l_i = v_i^{\; i \in 1..n}.l_j \rightarrow v_j\} && \text{E-PROJRCD} \\
+        \AxiomC{$t_1 \rightarrow t_1'$}
+        \UnaryInfC{$t_1.l \rightarrow t_1'.l$}
+        \DisplayProof && \text{E-PROJ} \\
+        \AxiomC{$ t_j \rightarrow t_j'$}
+        \UnaryInfC{$ \{l_i = v_i^{i \in 1..j-1}, l_j = t_j, l_k = t_k^{k \in j+1 .. n}\}
+                     \rightarrow
+                     \{l_i = v_i^{i \in 1..j-1}, l_j = t_j', l_k = t_k^{k \in j+1 .. n}\}
+                   $}
+        \DisplayProof && \text{E-RCD} \\
+    \end{align*}
+\end{definition}
+
+\begin{definition}
+    レコードの拡張に用いる新しい型付け規則
+
+    \begin{align*}
+        \AxiomC{各iに対して$ \Gamma \vdash t_i : T_i$}
+        \UnaryInfC{$ \Gamma \vdash \{ l_i = t_i^{\; i \in 1..n} : \{l_i : T_i^{\; i \in 1..n}\}$}
+        \DisplayProof && \text{T-RCD} \\
+        \AxiomC{$ \Gamma \vdash t_1 : \{ l_i : T_i^{\; i \in 1.. n}\}$}
+        \UnaryInfC{$\Gamma \vdash t_1.lj : T_j$}
+        \DisplayProof && \text{T-PROJ}
+    \end{align*}
+\end{definition}
+
+レコードを用いることで複数の値を一つの値としてまとめて扱うことができる。
+
 \section{部分型と Continuation based C}