--- a/paper/cbc-type.tex	Fri Feb 03 10:29:28 2017 +0900
+++ b/paper/cbc-type.tex	Fri Feb 03 11:59:41 2017 +0900
@@ -138,6 +138,46 @@
 
 % }}}
 
+% {{{ メタレベル計算の実行
+
 \section{メタレベル計算の実行}
+Meta DataSegment と Meta CodeSegment の定義を行なったので、残るは実行である。
+
+実行はノーマルレベルにおいては軽量継続 \verb/goto/ を定義することによって表せた。
+メタレベル実行ではそれを Meta CodeSegment と Meta DataSegment を扱えるように拡張する。
+Meta DataSegment は Parameterized Module の引数 \verb/Context/ に相当するため、Meta CodeSegment は Context を取って Context を返す CodeSegment となる。
+軽量継続 \verb/goto/ と区別するために名前を \verb/exec/ とするリスト~\ref{src:agda-exec}のように定義できる。
+行なっていることは Meta CodeSegment の本体部分に Meta DataSegment を渡す、という \verb/goto/ と変わらないが、\verb/set/ と \verb/get/ を用いることで上位型である任意の DataSegment を実行する CodeSegment も Meta CodeSegment として一様に実行できる。
+
+\lstinputlisting[label=src:agda-exec, caption=Agda におけるメタレベル実行の定義] {src/Exec.agda.replaced}
+
+実行例として、リスト~\ref{src:goto} に示していた a と b の値を加算して c に代入するプログラムを考える。
+実行する際に c の値を \verb/c'/ に保存してから加算ようなメタ計算を考える。
+c の値を \verb/c'/ に保存するタイミングは軽量継続時にユーザが指定する。
+よって軽量継続を行なうのと同等の情報を保持してなくてはならない。
+そのために Meta Meta DataSegment \verb/Meta/ には制御を移す対象であるノーマルレベル CodeSegment を持つ。
+値を格納する \verb/c'/ の位置は Meta DataSegment でも Meta Meta DataSegment でも構わないが、今回は Meta Meta DataSegemnt に格納するものとする。
+それらを踏まえた上での Meta Meta DataSegment の Agda 上での定義は~\ref{src:agda-mmds}のようになる。
+なお、\verb/goto/ などの名前の衝突を避けるためにノーマルレベルの定義は \verb/N/ に、メタレベルの定義は \verb/M/ へと名前を付けかえている。
+
+\lstinputlisting[label=src:agda-mmds, caption=Agda における Meta Meta DataSegment の定義例] {src/MetaMetaDataSegment.agda}
+
+定義した \verb/Meta/ を利用して、c を \verb/c'/に保存するメタ計算 \verb/push/ を定義する。
+より構文が CbC に似るように \verb/gotoMeta/ を糖衣構文的に定義する。
+\verb/gotoMeta/ や \verb/push/ で利用している \verb/liftContext/ や \verb/liftMeta/ はノーマルレベル計算をメタ計算レベルとするように型を明示的に変更するものである。
+結果的に \verb/main/ の \verb/goto/ を \verb/gotoMeta/ に置き換えることにより、c の値を計算しながら保存できる。
+リスト~\ref{src:agda-mmcs} に示したプログラムでは、通常レベルのコードセグメントを全く変更せずにメタ計算を含む形に拡張している。
+加算を行なう前の \verb/c/ の値が \verb/70/ であったとした時、計算結果 \verb/150/ は \verb/c/ に格納されるが、\verb/c'/には\verb/70/に保存されている。
+
+\lstinputlisting[label=src:agda-mmcs, caption=Agda における Meta Meta CodeSegment の定義と実行例] {src/MetaMetaCodeSegment.agda}
+
+メタの階層構造を表すと図のようになる。
+Meta DataSegment を含む任意の DataSegment は Meta DataSegment になりえるので、この階層構造は任意の段数定義することが可能である。
+
+
+% TODO: メタの階層構造の図
+
+% }}}
+
 \section{Agda を用いたContinuation based C の検証}
 \section{スタックの実装の検証}