\chapter{Agda における Continuation based C の表現}
\label{chapter:cbc-type}
CbC の項を部分型を用いて Agda 上に記述していく。
DataSegment と CodeSegment の定義、CodeSegment の接続と実行、メタ計算を定義し、 Agda 上で実行できることを確認する。
また、Agda上で定義した DataSegment とそれに付随する CodeSegment の持つ性質を Agda 上で証明していく。

% {{{ DataSegment の定義
\section{DataSegment の定義}
まず DataSegment から定義していく。
DataSegment はレコード型で表現できるため、Agda のレコードをそのまま利用できる。
例えは~\ref{src:goto} に示していた a と b を加算して c を出力するプログラムに必要な DataSegment を記述すると~\ref{src:agda-ds}のようになる。
cs0 は a と b の二つの Int 型の変数を利用するため、対応する ds0 は a と b のフィールドを持つ。
cs1 は計算結果を格納する c という名前の変数のみを持つので、同様にds1もcのみを持つ。

\lstinputlisting[label=src:agda-ds, caption=Agda における DataSegment の定義] {src/DataSegment.agda}
% }}}

% {{{ CodeSegment の定義
\section{CodeSegment の定義}
次に CodeSegment を定義する。
CodeSegment は DataSegment を取って DataSegment を返すものである。
よって $ I \rightarrow O $ を内包するデータ型を定義する。

レコード型の型は Set なので、Set 型を持つ変数 I と O を型変数に持ったデータ型 CodeSegment を定義する。
I は Input DataSegment の型であり、 O は  Output DataSegment である。

CodeSegment 型のコンストラクタには \verb/cs/ があり、Input DataSegment を取って Output DataSegment を返す関数を取る。
具体的なデータ型の定義はリスト ~\ref{src:agda-cs} のようになる。

\lstinputlisting[label=src:agda-cs, caption= Agda における CodeSegment 型の定義] {src/CodeSegment.agda.replaced}

この CodeSegment 型を用いて CodeSegment の処理本体を記述する。

まず計算の本体となる cs0 に注目する。
cs0 は二つのInt型変数を持つ ds0 を取り、一つのInt型変数を作った上で cs1 に軽量継続を行なう。
DataSegment はレコードなので、a と b のフィールドから値を取り出した上で加算を行ない、cを持つレコードを生成する。
そのレコードを引き連れたまま cs1 へと goto する。

次に cs1 に注目する。
cs1 は値に触れず cs2 へと goto するだけである。
よって何もせずにそのまま goto する関数をコンストラクタ\verb/cs/ に渡すだけで良い。

最後に cs2 である。
cs2 はリスト~\ref{src:goto}では省略していたが、今回は計算を終了させる CodeSegment として定義する。
どの CodeSegment にも軽量継続せずに値を持ったまま計算を終了させる。
コンストラクタ \verb/cs/ には関数を与えなくては値を構成できないため、何もしない関数である id を渡している。

最後に計算をする cs0 へと軽量継続する main を定義する。
例として、 a の値を 100 とし、 b の値を50としている。

cs0, cs1, cs2, main をAgda で定義するとリスト~\ref{src:agda-css}のようになる。

\lstinputlisting[label=src:agda-css, caption= Agda における CodeSegment の定義] {src/CodeSegments.agda}

正しく計算が行なえたなら値150が得られるはずである。
% }}}

% {{{ ノーマルレベル計算の実行
\section{ノーマルレベル計算の実行}
プログラムを実行することは \verb/goto/ を定義することと同義である。
軽量継続\verb/goto/ の性質としては

\begin{itemize}
    \item 次に実行する CodeSegment を指定する
    \item CodeSegment に渡すべき DataSegment を指定する
    \item 現在実行している CodeSegment から制御を指定された CodeSegment へと移動させる
\end{itemize}

がある。
Agda における CodeSegment の本体は関数である。
関数をそのまま使用すると再帰を許してしまうために CbC との対応が失われてしまう。
よって、\verb/goto/を利用できるのは関数の末尾のみである、という制約を関数に付け加える必要がある。

この制約さえ満たせば、CodeSegment の実行は CodeSegment 型から関数本体を取り出し、レコード型を持つ値を適用することに相当する。
具体的に \verb/goto/ を関数として適用するとリスト~\ref{src:agda-goto}のようになる。

\lstinputlisting[label=src:agda-goto, caption=Agdaにおける goto の定義] {src/Goto.agda}

この \verb/goto/ の定義を用いることで main などの関数が評価できるようになり、値150が得られる。
本文中での CodeSegment の定義は一部を抜粋している。
実行可能な Agda のソースコードは付録に載せる。% TODO: Appendix

% }}}

% {{{ 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.replaced}


ここで、関数を部分型に拡張する 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/ である。

% }}}

% {{{ Meta CodeSegment の定義

\section{Meta CodeSegment の定義}
Meta DataSegment が定義できたので Meta CodeSegment を定義する。
実際、DataSegment が Meta DataSegment に拡張できたため、Meta CodeSegment の定義には比較的変更は無い。
ノーマルレベルの \verb/CodeSegment/ 型に、DataSegment を取って DataSegment を返す、という制約を明示的に付けるだけである(リスト~\ref{src:agda-mcs})

\lstinputlisting[label=src:agda-mcs, caption=Agda における Meta CodeSegment の定義] {src/MetaCodeSegment.agda.replaced}

% }}}

% {{{ メタレベル計算の実行

\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}

なお、CbC におけるメタ計算を含む軽量継続\verb/goto meta/とAgda におけるメタ計算実行の比較はリスト~\ref{src:goto-meta}のようになる
% TODO: cbc と agda の diff

CodeSegment や Meta CodeSegment などの定義が多かっため、どの処理やデータがどのレベルに属するか複雑になったため、一度図にてまとめる。
Meta DataSegment を含む任意の DataSegment は Meta DataSegment になりえるので、この階層構造は任意の段数定義することが可能である。


% TODO: メタの階層構造の図

% }}}

% {{{ Agda を用いた Continuation based C の検証

\section{Agda を用いた Continuation based C の検証}
Agda において CbC の CodeSegment と DataSegment を定義することができた。
実際の CbC のコードを Agda に変換し、それらの性質を証明していく。

ここではGearsOS が持つ DataSegment \verb/SingleLinkedStack/ を証明していく。
この\verb/SingleLinkedStack/はポインタを利用した片方向リストを用いて実装されている。

CbC における DataSegment \verb/SingleLinkedStack/ の定義はリスト~\ref{src:cbc-stack}のようになっている。

\lstinputlisting[label=src:cbc-stack, caption=CbC における構造体 stack の定義] {src/stack.h}

次に Agda における \verb/SingleLinkedStack/の定義について触れるが、Agda にはポインタが無いため、メモリ確保や\verb/NULL/の定義は存在しない。
CbC におけるメモリ確保部分はノーマルレベルには出現しないと仮定し、\verb/NULL/の表現にはAgda の標準ライブラリに存在する \verb/Data.Maybe/ を用いる。

\verb/Data.Maybe/ の \verb/maybe/ 型は、コンストラクタを二つ持つ。
片方のコンストラクタ \verb/just/ は値を持ったデータであり、ポインタの先に値があることに対応している。
一方のコンストラクタ \verb/nothing/ は値を持たない。
これは値が存在せず、ポインタの先が確保されていない(\verb/NULL/ ポインタである)ことを表現できる。

\lstinputlisting[label=src:agda-maybe, caption=Agda における Maybe の定義] {src/Maybe.agda.replaced}

Maybe を用いて片方向リストを Agda 上に定義するとリスト~\ref{src:agda-stack}のようになる。
CbC とほぼ同様の定義ができている。
CbC、 Agda 共に\verb/SingleLinkedStack/ は \verb/Element/ 型の \verb/top/ を持っている。
\verb/Element/ 型は値と次の \verb/Element/ を持つ。
CbC ではポインタで表現していた部分が Agda では Maybe で表現されているが、\verb/Element/ 型の持つ情報は変わっていない。

\lstinputlisting[label=src:agda-stack, caption=Agda における片方向リストを用いたスタックの定義] {src/AgdaStack.agda}

Agda で片方向リストを利用する DataSegment の定義をリスト~\ref{src:agda-stack-ds}に示す。
ノーマルレベルからアクセス可能な場所として \verb/Context/ に \verb/element/ フィールドを追加する。
そしてノーマルレベルからアクセスできないよう分離した Meta Meta DataSegment である \verb/Meta/ にスタックの本体を格納する。
CbC における実装では \verb/.../ で不定であった \verb/next/ も、agda ではメタレベルのコードセグメント \verb/nextCS/ となり、きちんと型付けされている。

\lstinputlisting[label=agda-stack-ds, caption=スタックを利用するための DataSegment の定義] {src/AgdaStackDS.agda}

次にスタックへの操作に注目する。
スタックへと値を積む \verb/pushSingleLinkedStack/ と値を取り出す \verb/popSingleLinkedStack/ の CbC 実装をリスト~\ref{src:cbc-push-pop}に示す。
\verb/SingleLinkedStack/ は Meta CodeSegment であり、メタ計算を実行した後には通常の CodeSegment へと操作を移す。
そのために \verb/next/ という名前で次のコードセグメントを保持している。
具体的な \verb/next/ はコンパイル時にしか分からないため、\verb/.../ 構文を用いて不定としている。

\verb/pushSingleLinkedStack/ は \verb/element/ を新しく確保し、値を入れた後に \verb/next/ へと繋げ、 \verb/top/ を更新して軽量継続する。
\verb/popSingleLinkedStack/ は先頭が空でなければ先頭の値を \verb/top/ から取得し、\verb/element/を一つ進める。
値が空であれば \verb/data/ を \verb/NULL/ にしたまま軽量継続を行なう。

\lstinputlisting[label=src:cbc-push-pop, caption= CbC における SingleLinkedStack を操作する Meta CodeSegment] {src/singleLinkedStack.c}

次に Agda における定義をリスト~\ref{src:agda-push-pop}に示す。
同様に \verb/pushSingleLinkedStack/ と \verb/popSingleLinkedStack/ を定義している。
\verb/pushsinglelinkedstack/ では、スタックの値を更新したのちにノーマルレベルの CodeSegment である \verb/n/ を \verb/exec/ している。
なお、 \verb/liftMeta/ はノーマルレベルの計算をメタレベルとする関数である。

実際に値を追加する部分は where 句に定義された関数 \verb/push/ である。
これはスタックへと積む値が空であれば追加を行なわず、値がある時は新たに element を作成して top を更新している。
本来の CbC の実装では空かチェックはしていないが、値が空であるかに関わらずにスタックに積んでいるために挙動は同じである。

次に \verb/popSingleLinkedStack/ に注目する。
こちらも操作後に \verb/nextCS/ へと継続を移すようになっている。

実際に値を取り出す操作はノーマルレベルからアクセスできる \verb/element/ の値の確定と、アクセスできない \verb/stack/ の更新である。

\verb/element/については、 \verb/top/ が空なら取り出した後の値は無いので \verb/element/ は \verb/nothing/ である。
\verb/top/ が空でなければ \verb/element/ は \verb/top/ の値となる。

\verb/stack/ は空なら空のままであり、\verb/top/ に値があればその先頭を捨てる。
ここで、\verb/pop/ の実装はスタックが空であっても、例外を送出したり停止したりせずに処理を続行できることが分かる。

\lstinputlisting[label=src:agda-push-pop, caption=Agda における片方向リストを用いたスタックの定義] {src/AgdaPushPop.agda}

また、この章で取り上げた CbC と Agda の動作するソースコードは付録に載せる。 % TODO

% }}}


\section{スタックの実装の検証}