--- a/paper/introduction.tex	Mon Jan 30 14:54:01 2017 +0900
+++ b/paper/introduction.tex	Mon Jan 30 16:41:56 2017 +0900
@@ -1,4 +1,4 @@
-\chapter{Continuation based C とメタ計算としての検証手法}
+\chapter{CbC とメタ計算としての検証手法}
 ソフトウェアの規模が大きくなるにつれてバグは発生しやすくなる。
 バグとはソフトウェアが期待される動作以外の動作をすることである。
 ここで期待された動作は仕様と呼ばれ、自然言語や論理によって記述される。
@@ -35,5 +35,5 @@
 型システムの定義とラムダ計算、単純型付きラムダ計算と部分型について述べる。
 第\ref{chapter:agda}章では証明支援系プログラミング言語 Agda についての解説を行なう。
 Agda の構文や使い方、Curry-Howard Isomorphism や Natural Deduction といった証明に関する解説も行なう。
-第\ref{chapter:subtype}章では、部分型を用いて CbC のプログラムを Agda で記述し、証明を行なう。
+第\ref{chapter:cbc-type}章では、部分型を用いて CbC のプログラムを Agda で記述し、証明を行なう。
 CodeSegment や DataSegment の Agda 上での定義や、メタ計算はどのように定義されるかを解説する。

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/src/type-cs.c	Mon Jan 30 16:41:56 2017 +0900
@@ -0,0 +1,9 @@
+__code getMinHeight_stub(struct Context* context) {
+    goto getMinHeight(context, &context->data[Allocate]->allocate, &context->data[AkashaInfo]->akashaInfo);
+}
+
+__code getMinHeight(struct Context* context, struct Allocate* allocate, struct AkashaInfo* akashaInfo) {
+    /* ... */
+    goto getMinHeight_stub(context);
+}
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/src/type-ds.h	Mon Jan 30 16:41:56 2017 +0900
@@ -0,0 +1,5 @@
+struct AkashaInfo {
+    unsigned int minHeight;
+    unsigned int maxHeight;
+    struct AkashaNode* akashaNode;
+};

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/src/type-mds.h	Mon Jan 30 16:41:56 2017 +0900
@@ -0,0 +1,15 @@
+struct Data { /* data segments as types */
+    struct Tree { /* ... */ } tree;
+    struct Node { /* ... */ } node;
+
+    struct IterElem { /* ..  */ } iterElem;
+    struct Iterator { /* ... */ } iterator;
+    struct AkashaInfo { /* ... */} akashaInfo;
+    struct AkashaNode { /* ... */} akashaNode;
+};
+
+
+struct Context { /* meta data segment as subtype */
+    /* ... */
+    struct Data **data;
+};

--- a/paper/type.tex	Mon Jan 30 14:54:01 2017 +0900
+++ b/paper/type.tex	Mon Jan 30 16:41:56 2017 +0900
@@ -1136,5 +1136,98 @@
 
 % }}}
 
+% {{{ 部分型と Continuation based C
 
 \section{部分型と Continuation based C}
+部分型を用いて Conituation based C の型システムを定義していく。
+
+まず、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*\}$ であると見なせる。
+CodeSegment は DataSegment を引数に取るため、DataSegment の型は CodeSegment が要求する最低限の制約をまとめたものと言える。
+
+次に Meta DataSegment について考える。
+Meta DataSegment はプログラムに出現する DataSegment の共用体であった。
+これを DataSegment の構造体に変更する。
+こうすることにより、 Meta DataSegment はプログラム中に出現する DataSegment を必ず持つため、Meta DataSegment は任意の DataSegment の部分型となる。
+もしくは各 DataSegment の全てのフィールドを含むような1つの構造体でも良い。
+第~\ref{chapter:cbc-type}章における Meta 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}
+
+部分型として定義するなら以下のような定義となる。
+
+\begin{definition}
+    Meta DataSegment の定義
+
+    \begin{align*}
+        Meta \; DataSegment <: DataSegment_i^{i \in N} && \text{S-MDS}
+    \end{align*}
+\end{definition}
+
+なお、$N$はあるプログラムに出現するデータセグメントの名前の集合であるとする。
+
+次に CodeSegment の型について考える。
+CodeSegment は DataSegment を DataSegment へと移す関数型とする。
+
+\begin{definition}
+    CodeSegment の定義
+
+    \begin{align*}
+        DataSegment \rightarrow DataSegment && \text{T-CS}
+    \end{align*}
+\end{definition}
+
+そして Meta CodeSegmentは Meta DataSegment を Meta DataSegment へと移す関数となる。
+
+\begin{definition}
+    Meta CodeSegment の定義
+
+    \begin{align*}
+        Meta \; DataSegment \rightarrow Meta \; DataSegment && \text{T-MCS}
+    \end{align*}
+\end{definition}
+
+ここで具体的なコード(リスト~\ref{src:type-cs})と比較してみる。
+
+\lstinputlisting[label=src:type-cs, caption=具体的なCbCにおける CodeSegment] {src/type-cs.c}
+
+CodeSegment \verb/getMinHeight/ は DataSegment \verb/Allocate/ と \verb/AkashaInfo/ を引数に取っている。
+現状は \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 $ とする際の導出木は以下である。
+
+\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}
+
+返り値部分を部分型として定義することにより、軽量継続先が上位型であればどの CodeSegment へと遷移しても良い。
+プログラムによっては遷移先は確定しているために部分型にする必要性は無いが、メタ計算やライブラリなどの遷移先が不定の場合は一度部分型として確定し、その後コンパイル時やランタイム時に包摂関係から具体型を導けば良い。
+例えばコンパイル時に解決すればライブラリの静的リンク時実行コード生成が行なえ、ランタイム時に解決すればネットワークを経由するプログラムとの接続初期化に利用できる。
+例えば、プロトコルがバージョンを持つ場合に接続先のプログラムが利用しているプロトコルと互換性があるかの判断を Context どうしの部分型関係で判断できる。
+
+また、stub のみに注目すると、stub は Context から具体的なDataSegment X を取り出す操作に相当し、S-ARROWの左側の前提のような振舞いをする。
+加えて、軽量継続する際に X の計算結果を Context に格納してから goto する部分を別の Meta CodeSegment として分離すると、S-ARROWの右側の前提のような振舞いを行なう。
+このようにノーマルレベルの CodeSegment の先頭と末尾にメタ計算を接続することによってノーマルレベルの CodeSegment が型付けできる。
+型付けにDataSegment の集合としての Meta DataSegment が必須になるが、これは構造体として定義可能なためコンパイル時に生成することで CbC に組み込むことができる。
+
+なお、メタ計算に利用する Meta DataSegment と Meta DataSegment も同様に型付けできる。
+ここで興味深いのはあるレベルの CodeSegment は同レベルの DataSegment において型付けされるが、一つ上の階層から見ると、下の階層のDataSegmentとして一貫して扱えることにある。
+このようにメタ計算を階層化することにより、メタ計算で拡張された計算に対しても他のメタ計算が容易に適用できる。
+
+% }}}