--- a/paper/cbc-type.tex	Wed Feb 08 17:39:12 2017 +0900
+++ b/paper/cbc-type.tex	Thu Feb 09 12:56:22 2017 +0900
@@ -6,285 +6,10 @@
 CbC で自身を証明するために依存型を利用したいが、CbC には専用の型システムが存在しない。
 依存型をCbCコンパイラで扱うためにもまず現状の CbC を型付けする必要がある。
 
-~\ref{chapter:cbc-type}では CbC の型システムを部分型を利用して定義する。
+~\ref{chapter:cbc-type}では CbC の項が部分型で型付けできることを示す。
 定義した型システムを用いて、Agda 上に DataSegment と CodeSegment の定義、CodeSegment の接続と実行、メタ計算を定義し、それらが型付けされることを確認する。
 また、Agda 上で定義した DataSegment とそれに付随する CodeSegment の持つ性質を Agda で証明する。
 
-% {{{ 部分型付け
-
-\section{部分型付け}
-TODO: なおす
-単純型付きラムダ計算では、ラムダ計算の項が型付けされることを確認した。
-ここで、 単純型の拡張として、レコードを導入する。
-
-レコードとは名前の付いた複数の値を保持するデータである。
-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}
-
-レコードを用いることで複数の値を一つの値としてまとめて扱うことができる。
-しかし、引数にレコードを取る場合、その型と完全に一致させる必要がある。
-例えば $ \{ 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 \}$ を導ける。
-
-部分型関係は $ S <: T $ という形式の部分型付け式を導入するための推論規則の集まりとして定式化される。
-始めに、部分型付けの一般的な規定から考える。
-部分型は反射的であり、推移的である。
-
-\begin{align*}
-    S <: S && \text{S-REFL} \\
-    \AxiomC{$S <: U$}
-    \AxiomC{$U <: T$}
-    \BinaryInfC{$ S <: T $}
-    \DisplayProof && \text{S-TRANS}
-\end{align*}
-
-これらの規則は安全代入に対する直感より正しい。
-次に、基本型や関数型、レコード型などの型それぞれに対して、その形の型の要素が期待される部分に対して上位型の要素を利用しても安全である、という規則を導入していく。
-
-レコード型については型 $ T = \{ l_i : T_1 ... l_n : T_n\} $が持つフィールドが型 $ S = \{ k_1 : S_1 ... k_n : T_n\} $のものよりも少なければ $S$ を $T$の部分型とする。
-つまりレコードの終端フィールドのいくつかを忘れてしまっても安全である、ということを意味する。
-この直感は幅部分型付け規則となる。
-
-\begin{align*}
-    \{l_i : T_i^{\; i \in 1..n+k} \} <: \{l_i : T_i^{\; i \in 1..n}\}
-    && \text{S-RCDWIDTH}
-\end{align*}
-
-フィールドの多い方が部分型となるのは名前に反するように思える。
-しかし、フィールドが多いレコードほど制約が多くなり表すことのできる集合の範囲は小さくなる。
-集合の大きさで見ると明かにフィールドの多い方が小さいのである。
-
-幅部分型付け規則が適用可能なのは、共通のフィールドの型が全く同じな場合のみである。
-しかし、その場合フィールドの型に部分型を導入できず、フィールドの型の扱いで同じ問題を抱えることとなる。
-そのために導入するのが深さ部分型付けである。
-二つのレコードの中で対応するフィールドの型が部分型付け関係にある時に個々のフィールドの型が異なることを許す。
-これは具体的には以下の規則となる。
-
-\begin{align*}
-    \AxiomC{各iに対して $S_i <: T_i$}
-    \UnaryInfC{$\{ l_i : S_i^{\; i \in 1..n}\} <: \{l_i : T_i^{\; i \in 1..n}\}$}
-    \DisplayProof && \text{S-RCDDEPTH}
-\end{align*}
-
-これらを用いて $ \{ x : \{a : Nat , b : Nat\}, y : \{m : Nat\}\}$ が $ \{x : \{ a : Nat\}, y : \{\}\}$の部分型であることは以下のように導出できる。
-
-\begin{prooftree}
-    \AxiomC{}
-    \RightLabel{S-RCDWIDTH}
-    \UnaryInfC{$ \{a : Nat, b : Nat\} <: \{a : Nat\}$}
-    \AxiomC{}
-    \RightLabel{S-RCDWIDTH}
-    \UnaryInfC{$ \{m : Nat\} <: \{\}$}
-    \RightLabel{S-RCDDEPTH}
-    \BinaryInfC{$ \{ x : \{a : Nat , b : Nat\}, y : \{m : Nat\}\} <:  \{x : \{ a : Nat\}, y : \{\}\}$}
-\end{prooftree}
-
-最後に、レコードを利用する際はフィールドさえ揃っていれば順序は異なっても良いという規則を示す。
-
-\begin{align*}
-    \AxiomC{$ \{ k_j : S_j^{\; i \in 1 .. n} \}$ は $ \{ l_i : T_i^{\; i \in 1 ..n}\} $ の並べ替えである}
-    \UnaryInfC{$ \{k_j : S_j^{\; j \in 1..n} \} <: \{l_i : T_i^{\; i \in 1..n }\}$}
-    \DisplayProof && \text{S-RCDPERM}
-\end{align*}
-
-S-RCDPERM を用いることで、終端フィールドだけではなく任意の位置のフィールドを削ることができる。
-
-レコードの部分型は定義できたので、次は関数の部分型を定義していく。
-関数の部分型は以下 S-ARROW として定義できる。
-
-\begin{align*}
-    \AxiomC{$ T_1 <: S_1$}
-    \AxiomC{$ S_2 <: T_2$}
-    \BinaryInfC{$ S_1 \rightarrow S_2 <: T_1 \rightarrow T_2 $}
-    \DisplayProof && \text{S-ARROW}
-\end{align*}
-
-前提の条件二つを見ると部分型の関係が逆転している。
-左側の条件は関数型自身の型と逆になっているため反変と言い、返り値の型は同じ向きであるため共変と言う。
-引数について考えた時、求める型よりも大きい型であれば明らかに安全に呼ぶことができるために関数の引数の型の方が上位型になる。
-返り値については関数が返す型が部分型であれば上位型を返すことができるため、関数の返り値の方が部分型になる。
-
-別の見方をすると、型 $ S_1 \rightarrow S_2 $ の関数を別の型 $ T_1 \rightarrow T_2 $が期待される文脈で用いることが安全な時とは
-
-\begin{itemize}
-    \item 関数に渡される引数がその関数にとって想定外でない($ T_1 <: S_1$)
-    \item 関数が返す値も文脈にとって想定外でない($ S_2 <: T_2 $)
-\end{itemize}
-
-という場合に限る。
-
-% }}}
-
-% {{{ 部分型と 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 はそのように定義している。
-なお、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}
-
-部分型として定義するなら以下のような定義となる。
-
-\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として一貫して扱えることにある。
-このようにメタ計算を階層化することにより、メタ計算で拡張された計算に対しても他のメタ計算が容易に適用できる。
-
-% }}}
-
 % {{{ DataSegment の定義
 \section{DataSegment の定義}
 まず DataSegment から定義していく。