--- a/paper/type.tex	Thu Feb 09 12:56:22 2017 +0900
+++ b/paper/type.tex	Thu Feb 09 13:57:35 2017 +0900
@@ -88,7 +88,10 @@
 
 ここでレコード型という型を導入する。
 レコード型は複数の型を持ちえる型であり、内部に持っている値にはユニークな名前がラベルとして付いている。
+例えば「Intの変数x とIntの変数yを持つレコード型」は$ \{ x : Int , y : Bool\}$のように記述する。
+C における構造体ではリストに対応する。
 % TODO C の構造体
+
 レコード型の値を構成する際には、内部に格納する値を全て与えることで構成できる。
 % TODO C の構造体の初期化
 レコード型から値を取り出す際にはラベル名を用いた射影を利用する。
@@ -102,8 +105,8 @@
 \section{部分型付け}
 レコードを用いることで複数の値を一つの値としてまとめて扱うことができる。
 しかし、関数が引数にレコードを取る場合、その型と完全に一致させる必要がある。
-例えば $ \{ x : Nat \} $ を引数に取る関数に対して $ \{ x : Nat , y : Bool\}$ といった値を適用することができない。
-しかし、直感的には関数の要求はフィールド $x $ が型 $Nat$を持つことのみであり、その部分にのみ注目すると$ \{ x : Nat , y : Bool\}$ も要求に沿っている。
+例えば $ \{ x : Int \} $ を引数に取る関数に対して $ \{ x : Int , y : Bool\}$ といった値を適用することができない。
+しかし、直感的には関数の要求はフィールド $x $ が型 $Int$を持つことのみであり、その部分にのみ注目すると$ \{ x : Nat , y : Bool\}$ も要求に沿っている。
 
 ここで、部分型という型を導入する。
 部分型は上記のような場合の項を許すように型付けを緩めることである。
@@ -151,15 +154,14 @@
 % {{{ 部分型と Continuation based C
 
 \section{部分型と Continuation based C}
-TODO なおす
 部分型を用いて Conituation based C の型システムを定義していく。
 
-まず、DataSegment の型から定義してく。
+まず、DataSegment の型を定義する。
 DataSegment 自体はCの構造体によって定義されているため、レコード型として考えることができる。
 例えばリスト~\ref{src:akasha-context}に示していた DataSegment の一つに注目する(リスト~\ref{src:type-ds})。
 
 \lstinputlisting[label=src:type-ds, caption=akashaContext の DataSegment である AkashaInfo] {src/type-ds.h}
-この AkashaInfo は $ \{ minHeight : unsigned\; int , maxHeight : unsigned \; int, akashaNode : AkashaNode*\}$ であると見なせる。
+この AkashaInfo は $ \{ minHeight : unsigned\; int , maxHeight : unsigned \; int, akashaNode : AkashaNode*\}$ 型を持つ。
 CodeSegment は DataSegment を引数に取るため、DataSegment の型は CodeSegment が要求する最低限の制約をまとめたものと言える。
 
 次に Meta DataSegment について考える。
@@ -168,7 +170,7 @@
 こうすることにより、 Meta DataSegment はプログラム中に出現する DataSegment を必ず持つため、Meta DataSegment は任意の DataSegment の部分型となる。
 もしくは各 DataSegment の全てのフィールドを含むような1つの構造体でも良い。
 第~\ref{chapter:cbc-type}章における Meta DataSegment はそのように定義している。
-なお、GearsOSでは DataSegment の共用体をプログラムで必要な数だか持つ実装になっている。
+なお、GearsOSでは DataSegment の共用体をプログラムで必要な数だけ持つ実装になっている。
 
 具体的な CbC における Meta DataSegment であるContext (リスト~\ref{src:type-mds})は、 DataSegment の集合を値として持っているために明らかに DataSegment よりも多くの情報を持っている。
 \lstinputlisting[label=src:type-mds, caption=CbC の Meta DataSegment である Context] {src/type-mds.h}
@@ -179,12 +181,10 @@
     Meta DataSegment の定義
 
     \begin{align*}
-        Meta \; DataSegment <: DataSegment_i^{i \in N} && \text{S-MDS}
+        Meta \; DataSegment <: プログラム中の任意のDataSegment
     \end{align*}
 \end{definition}
 
-なお、$N$はあるプログラムに出現するデータセグメントの名前の集合であるとする。
-
 次に CodeSegment の型について考える。
 CodeSegment は DataSegment を DataSegment へと移す関数型とする。
 
@@ -192,7 +192,7 @@
     CodeSegment の定義
 
     \begin{align*}
-        DataSegment \rightarrow DataSegment && \text{T-CS}
+        DataSegment \rightarrow DataSegment
     \end{align*}
 \end{definition}
 
@@ -202,7 +202,7 @@
     Meta CodeSegment の定義
 
     \begin{align*}
-        Meta \; DataSegment \rightarrow Meta \; DataSegment && \text{T-MCS}
+        Meta \; DataSegment \rightarrow Meta \; DataSegment
     \end{align*}
 \end{definition}
 
@@ -211,36 +211,25 @@
 \lstinputlisting[label=src:type-cs, caption=具体的なCbCにおける CodeSegment] {src/type-cs.c}
 
 CodeSegment \verb/getMinHeight/ は DataSegment \verb/Allocate/ と \verb/AkashaInfo/ を引数に取っている。
-現状は \verb/Context/ も継続のために渡しているが、本来ノーマルレベルからはアクセスできないために隠れているとする。
+現状は \verb/Context/ も軽量継続のために渡しているが、本来ノーマルレベルからはアクセスできないために隠れているとする。
 その場合、引数の型は $ \{ allocate : Allocate , akashaInfo : AkahsaInfo\}  $ となる。
 また、返り値は構文的には存在していないが、軽量継続で渡す値は $ Context $ である。
 よって \verb/getMinHeight/ の型は $ \{ allocate : Allocate , akashaInfo : AkahsaInfo\} \rightarrow Context $ となる。
-$ Context $ の型は Meta DataSegment なので、 subtype の S-ARROW より $Context $の上位型への変更ができる。
-
-$ \{ allocat; : Allocate , akashaInfo : AkahsaInfo\}  $ を $X$と置いて、\verb/getMinHeignt/ を $ X \rightarrow X $ とする際の導出木は以下である。
+$ Context $ の型は Meta DataSegment なので、部分型の定義より $Context $の上位型への変更ができる。
 
-\begin{prooftree}
-    \AxiomC{}
-    \RightLabel{S-REFL}
-    \UnaryInfC{$ X <: X $}
-    \AxiomC{}
-    \RightLabel{S-MDS}
-    \UnaryInfC{$ Conttext <: X$}
-    \RightLabel{S-ARROW}
-    \BinaryInfC{$ X \rightarrow Context <: X \rightarrow X$}
-\end{prooftree}
+% TODO: 図
 
 返り値部分を部分型として定義することにより、軽量継続先が上位型であればどの CodeSegment へと遷移しても良い。
-プログラムによっては遷移先は確定しているために部分型にする必要性は無いが、メタ計算やライブラリなどの遷移先が不定の場合は一度部分型として確定し、その後コンパイル時やランタイム時に包摂関係から具体型を導けば良い。
-例えばコンパイル時に解決すればライブラリの静的リンク時実行コード生成が行なえ、ランタイム時に解決すればネットワークを経由するプログラムとの接続初期化に利用できる。
-例えば、プロトコルがバージョンを持つ場合に接続先のプログラムが利用しているプロトコルと互換性があるかの判断を Context どうしの部分型関係で判断できる。
+プログラムによっては遷移先は確定しているために部分型にせず具体的なものでも良い。
+しかし、メタ計算やライブラリなどの遷移先が不定の場合は一度部分型として確定し、その後コンパイル時やランタイム時に具体的な型を導けば良い。
 
-また、stub のみに注目すると、stub は Context から具体的なDataSegment X を取り出す操作に相当し、S-ARROWの左側の前提のような振舞いをする。
-加えて、軽量継続する際に X の計算結果を Context に格納してから goto する部分を別の Meta CodeSegment として分離すると、S-ARROWの右側の前提のような振舞いを行なう。
+また、stub のみに注目すると、stub は Context から具体的な DataSegment X を取り出す操作に相当し、部分型の関数の引数の仮定のような振舞いをする。
+加えて、軽量継続する際に X の計算結果を Context に格納してから goto する部分を別の Meta CodeSegment として分離すると、部分型の返り値の仮定のような振舞いを行なう。
 このようにノーマルレベルの CodeSegment の先頭と末尾にメタ計算を接続することによってノーマルレベルの CodeSegment が型付けできる。
-型付けにDataSegment の集合としての Meta DataSegment が必須になるが、これは構造体として定義可能なためコンパイル時に生成することで CbC に組み込むことができる。
+型付けを行なう際には DataSegment の集合としての Meta DataSegment が必須になるが、構造体としてコンパイル時に生成することで CbC に組み込むことができる。
 
 なお、メタ計算に利用する Meta DataSegment と Meta DataSegment も同様に型付けできる。
+Meta DataSegment の部分型に相当する Meta Meta DataSegment を定義してやれば良い。
 ここで興味深いのはあるレベルの CodeSegment は同レベルの DataSegment において型付けされるが、一つ上の階層から見ると、下の階層のDataSegmentとして一貫して扱えることにある。
 このようにメタ計算を階層化することにより、メタ計算で拡張された計算に対しても他のメタ計算が容易に適用できる。