Binary file paper/atton-master.pdf has changed

Binary file paper/fig/cbc-subtype.graffle has changed

Binary file paper/fig/cbc-subtype.pdf has changed

Binary file paper/fig/subtype-arg.graffle has changed

Binary file paper/fig/subtype-arg.pdf has changed

Binary file paper/fig/subtype-return.graffle has changed

Binary file paper/fig/subtype-return.pdf has changed

--- a/paper/type.tex	Thu Feb 09 16:34:07 2017 +0900
+++ b/paper/type.tex	Thu Feb 09 17:50:50 2017 +0900
@@ -131,23 +131,39 @@
     \BinaryInfC{$ S_1 \rightarrow S_2 <: T_1 \rightarrow T_2 $}
 \end{prooftree}
 
-これは「仮定{$ T_1 <: S_1$ と$ S_2 <: T_2$ が成り立つ時、$ S_1 \rightarrow S_2 <: T_1 \rightarrow T_2 $ が成り立つ」と読む。
+これは「仮定$ T_1 <: S_1$ と$ S_2 <: T_2$ が成り立つ時、$ S_1 \rightarrow S_2 <: T_1 \rightarrow T_2 $ が成り立つ」と読む。
 この部分型は引数の型と返り値の部分型について述べているために少々複雑である。
 
 まず、引数部分に注目する。
 上位型の関数の引数は $ T_1 $ である。
 引数に対する仮定は部分型関係$ T_1 <: S_1$である。
-これは上位型関数の方が部分型となっており、大きい。
+これは上位型関数の引数が部分型となっており、大きい。
 そして導かれる部分型の引数の型は $ S_1$ である。
-つまり、「大きい型 $T_1$を要求する関数は小さい型 $S_1$ を要求する関数として使って良い」ということである。
-具体的には $ T_1 $ のレコードをいくつか削って $S_1$まで小さくすれば良い。
+つまり、「小さい型 $S_1$を要求する関数は大きな型 $S_1$ を受けつける」と言える。
+具体的には $ T_1 $ のレコードをいくつか削って $S_1$まで小さくすれば良いのである(図~\ref{fig:subtype-arg})。
+
+\begin{figure}[htbp]
+    \begin{center}
+        \includegraphics[width=450pt]{fig/subtype-arg.pdf}
+        \caption{部分型の関数型と引数の型}
+        \label{fig:subtype-arg}
+    \end{center}
+\end{figure}
 
 次に返り値部分に注目する。
 上位型の関数の返り値は $T_2$ である。
 返り値に対する仮定は部分型関係$ S_2 <: T_2$であり、引数と逆になっている。
 これは上位型関数の方が上位型となっており、小さい。
-つまり、「小さい型 $ T_2 $ を返す関数は、大きい型 $S_2$ を返す関数として使っても良い」ということである。
-具体的には $ T_2 $ のレコードが $S_2$ に全て格納できることを意味する。
+つまり、「大きい型 $ S_2 $ を返す関数は、小さい型 $T_2$ を返す関数として使っても良い」ということである。
+具体的にはこちらも $ S_2 $ のレコードを削って $T_2$ と同じになるまで小さくなるようにすれば良い(図~\ref{fig:subtype-return})。
+
+\begin{figure}[htbp]
+    \begin{center}
+        \includegraphics[width=450pt]{fig/subtype-return.pdf}
+        \caption{部分型の関数型と返り値の型}
+        \label{fig:subtype-return}
+    \end{center}
+\end{figure}
 
 % }}}
 
@@ -181,7 +197,7 @@
     Meta DataSegment の定義
 
     \begin{align*}
-        Meta \; DataSegment <: プログラム中の任意のDataSegment
+        \text{Meta DataSegment} <: \text{プログラム中の任意のDataSegment}
     \end{align*}
 \end{definition}
 
@@ -192,7 +208,7 @@
     CodeSegment の定義
 
     \begin{align*}
-        DataSegment \rightarrow DataSegment
+        \text{DataSegment} \rightarrow \text{DataSegment}
     \end{align*}
 \end{definition}
 
@@ -202,7 +218,7 @@
     Meta CodeSegment の定義
 
     \begin{align*}
-        Meta \; DataSegment \rightarrow Meta \; DataSegment
+        \text{Meta DataSegment} \rightarrow \text{Meta DataSegment}
     \end{align*}
 \end{definition}
 
@@ -215,9 +231,15 @@
 その場合、引数の型は $ \{ allocate : Allocate , akashaInfo : AkahsaInfo\}  $ となる。
 また、返り値は構文的には存在していないが、軽量継続で渡す値は $ Context $ である。
 よって \verb/getMinHeight/ の型は $ \{ allocate : Allocate , akashaInfo : AkahsaInfo\} \rightarrow Context $ となる。
-$ Context $ の型は Meta DataSegment なので、部分型の定義より $Context $の上位型への変更ができる。
+$ Context $ の型は Meta DataSegment なので、部分型の定義より $Context $の上位型への変更ができる(図~\ref{fig:cbc-subtype})。
 
-% TODO: 図
+\begin{figure}[htbp]
+    \begin{center}
+        \includegraphics[width=450pt]{fig/cbc-subtype.pdf}
+        \caption{CodeSegment の部分型付け}
+        \label{fig:cbc-subtype}
+    \end{center}
+\end{figure}
 
 返り値部分を部分型として定義することにより、軽量継続先が上位型であればどの CodeSegment へと遷移しても良い。
 プログラムによっては遷移先は確定しているために部分型にせず具体的なものでも良い。