# HG changeset patch
# User atton <atton@cr.ie.u-ryukyu.ac.jp>
# Date 1486085006 -32400
# Node ID 3981580ece72d4cea8e99f3224a6e4b50da75860
# Parent  ecd3a1e4092101e0c659d72c710284d5d5bdf8fd
Add Meta DataSegment description

diff -r ecd3a1e40921 -r 3981580ece72 paper/atton-master.pdf
Binary file paper/atton-master.pdf has changed
diff -r ecd3a1e40921 -r 3981580ece72 paper/cbc-type.tex
--- a/paper/cbc-type.tex	Wed Feb 01 15:37:11 2017 +0900
+++ b/paper/cbc-type.tex	Fri Feb 03 10:23:26 2017 +0900
@@ -63,7 +63,7 @@
 \begin{itemize}
     \item 次に実行する CodeSegment を指定する
     \item CodeSegment に渡すべき DataSegment を指定する
-    \item 現在実行している CodeSegment から制御を指定されて CodeSegment へと移動させる
+    \item 現在実行している CodeSegment から制御を指定された CodeSegment へと移動させる
 \end{itemize}
 
 がある。
@@ -82,7 +82,51 @@
 
 % }}}
 
-\section{MetaDataSegment の定義}
+% {{{ Meta DataSegment の定義
+
+\section{Meta DataSegment の定義}
+ノーマルレベルの CbC を Agda 上で記述し、実行することができた。
+次にメタレベルの計算を Agda 上で記述していく。
+
+Meta DataSegment はノーマルレベルの DataSegment の集合として定義できるものであり、全ての DataSegment の部分型であった。
+ノーマルレベルの DataSegment はプログラムによって変更されるので、事前に定義できるものではない。
+ここで、Agda の Parameterized Module を利用して、「Meta DataSegment の上位型は DataSegment である」のように DataSegment を定義する。
+こうすることにより、全てのプログラムは一つ以上の Meta DataSegment を持ち、任意の個数の DataSegment を持つ。
+また、Meta DataSegment をメタレベルの DataSegment として扱うことにより、「Meta DataSegment の部分型である Meta Meta DataSegment」を定義できるようになる。
+階層構造でメタレベルを表現することにより、計算の拡張を自在に行なうことができる。
+
+具体的な Meta DataSegment の定義はリスト~\ref{src:agda-mds}のようになる。
+型システム \verb/subtype/ は、Meta DataSegment である \verb/Context/ を受けとることにより構築される。
+Context を Meta DataSegment とするプログラム上では DataSegment は Meta CodeSegment の上位型となる。
+その制約を \verb/DataSegment/ 型は表わしている。
+
+\lstinputlisting[label=src:agda-mds, caption=Agda における Meta DataSegment の定義] {src/MetaDataSegment.agda}
+
+
+ここで、関数を部分型に拡張する 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-ARROW は、前提である部分型関係 $ T_1 <: S_1 $ と $ S_2 <: T_2 $ が成り立つ時に、 上位型 $ S_1 \rightarrow S_2 $ の関数を、部分型 $ T_1 \rightarrow T_2 $ に拡張できた。
+ここでの上位型は DataSegment であり、部分型は Meta DataSegment である。
+制約\verb/DataSegment/ の \verb/get/ は、 Meta DataSegment から DataSegment が生成できることを表す。
+これは前提 $ T_1 <: S_1 $ に相当する。
+そして、\verb/set/ は $ S_2 <: T_2 $ に相当する。
+しかし、任意の DataSegment が Meta DataSegment の部分型となるには、 DataSegment が Meta DataSegment よりも多くの情報を必ず持たなくてはならないが、これは通常では成り立たない。
+だが、メタ計算を行なう際には常に Meta DataSegment を一つ以上持っていると仮定するならば成り立つ。
+実際、GearsOS における赤黒木では Meta DataSegment に相当する \verb/Context/ を常に持ち歩いている。
+GearsOS における計算結果はその持ち歩いている Meta DataSegment の更新に相当するため、常に Meta DataSegment を引き連れていることを無視すれば DataSegment から Meta DataSegment を導出できる。
+よって $ S_2 <: T_2 $ が成り立つ。
+
+なお、 $ S_2 <: T_2 $ は Output DataSegment を Meta DataSegment を格納する作業に相当し、 $ T_1 <: S_1 $ は Meta DataSegment から Input DataSegment を取り出す作業であるため、これは明らかに \verb/stub/ である。
+
+% }}}
+
 \section{MetaCodeSegment の定義}
 \section{メタレベル計算の実行}
 \section{Agda を用いたContinuation based C の検証}
diff -r ecd3a1e40921 -r 3981580ece72 paper/src/MetaDataSegment.agda
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/src/MetaDataSegment.agda	Fri Feb 03 10:23:26 2017 +0900
@@ -0,0 +1,7 @@
+module subtype {l : Level} (Context : Set l) where
+
+record DataSegment {ll : Level} (A : Set ll) : Set (l ⊔ ll) where
+  field
+    get : Context -> A
+    set : Context -> A -> Context
+