\chapter{Agda における Continuation based C の表現}
\label{chapter:cbc-type}
~\ref{chapter:agda}章では Curry-Howard 同型対応により、型付きラムダ計算を用いて命題が証明できることを示した。
加えて、証明支援系言語 Agda を用いてデータの定義とそれを扱う関数の性質の証明が行なえることを確認した。

この章では CbC の型システムを部分型を利用して定義する。
定義した型システムがきちんと検査されるかを確認するため、Agda 上に DataSegment と CodeSegment の定義、CodeSegment の接続と実行、メタ計算を定義し、型付けされることを確認する。
また、Agda 上で定義した DataSegment とそれに付随する CodeSegment の持つ性質を Agda 証明する。

% {{{ 部分型付け

\section{部分型付け}
単純型付きラムダ計算では、ラムダ計算の項が型付けされることを確認した。
ここで、 単純型の拡張として、レコードを導入する。

レコードとは名前の付いた複数の値を保持するデータである。
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 から定義していく。
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{ノーマルレベル計算の実行}
\label{section:normal-level-exec}
プログラムを実行することは \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 のソースコードは付録に載せる。

% }}}

% {{{ 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{メタレベル計算の実行}
\label{section:meta-level-exec}
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 の検証}
\label{section:cbc-proof}
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=src: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/ にしたまま軽量継続を行なう。

% TODO  null check を入れる
\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 の動作するソースコードは付録に載せる。

% }}}

% {{{ スタックの実装の検証
\section{スタックの実装の検証}
\label{section:stack-proof}
定義した SingleLinkedStack に対して証明を行なっていく。
ここでの証明は SingleLinkedStack の処理が特定の性質を持つことを保証することである。

例えば

\begin{itemize}
    \item スタックに積んだ値は取り出せる
    \item 値は複数積むことができる
    \item スタックから値を取り出すことができる
    \item スタックから取り出す値は積んだ値である
    \item スタックから値を取り出したらその値は無くなる
    \item スタックに値を積んで取り出すとスタックの内容は変わらない
\end{itemize}

といった多くの性質がある。

ここでは、最後に示した「スタックに値を積んで取り出すとスタックの内容は変わらない」ことについて示していく。
この性質を具体的に書き下すと以下のようになる。

\begin{definition}
    任意のスタック s に対して

    \begin{itemize}
        \item 任意の値n
        \item 値xを積む操作 push(x, s)
        \item 値を一つスタックから取り出す操作 pop(s)
    \end{itemize}

    がある時、

    pop . push(n) s = s

    である。
\end{definition}

これを Agda 上で定義するとリスト~\ref{src:agda-push-pop-type-1} のようになる。
Agda 上の定義ではスタックそのものではなく、スタックを含む任意の \verb/Meta/ に対してこの性質を証明する。
この定義が \verb/Meta/ の値によらず成り立つことを、自然数の加算の交換法則と同様に等式変形を用いて証明していく。

\lstinputlisting[label=src:agda-push-pop-type-1, caption=Agda におけるスタックの性質の定義(1)] {src/PushPopType.agda.replaced}

今回注目する条件分けは、スタック本体である \verb/stack/ と、push や pop を行なうための値を格納する \verb/element/ である。
それぞれが持ち得る値を場合分けして考えていく。

\begin{itemize}
    \item スタックが空である場合

        \begin{itemize}
            \item element が存在する場合

                値が存在するため、 push は実行される。
                push が実行されたためスタックに値があるため、pop が成功する。
                pop が成功した結果スタックは空となるため元のスタックと同一となり成り立つ。

            \item element が存在しない場合

                値が存在しないため、 push が実行されない。
                push が実行されなかったため、スタックは空のままであり、pop も実行されない。
                結果スタックは空のままであり、元のスタックと一致する。
        \end{itemize}

    \item スタックが空でない場合

        \begin{itemize}
            \item element が存在する場合

                element に設定された値 n が push され、スタックに一つ値が積まれる。
                スタックの先頭は n であるため、pop が実行されて n は無くなる。
                結果、スタックは実行する前の状態に戻る。

            \item element が存在しない場合

                element に値が存在しないため、push は実行されない。
                スタックは空ではないため、popが実行され、先頭の値が無くなる。
                実行後、スタックは一つ値を失なっているため、これは成りたたない。
        \end{itemize}
\end{itemize}

スタックが空でなく、push する値が存在しないときにこの性質は成り立たないことが分かった。
また、\verb/element/ が空でない制約を仮定に加えることでこの命題は成り立つようになる。

push 操作と pop 操作を連続して行なうとスタックが元に復元されることは分かった。
ここで SingleLinkedStack よりも範囲を広げて \verb/Meta/ も復元されるかを考える。
一見これも自明に成り立ちそうだが、push 操作と pop 操作は操作後に実行される CodeSegment を持っている。
この CodeSegment は任意に設定できるため、\verb/Meta/ 内部の DataSegement が書き換えられる可能性がある。
よってこれも制約無しでは成り立たない。

逆にいえば、CodeSegment を指定してしまえば \verb/Meta/ に関しても push/pop の影響を受けないことを保証できる。
全く値を変更しない CodeSegment \verb/id/ を指定した際には自明にこの性質が導ける。
実際、 Agda 上でも等式変形を明示的に指定せず、定義からの推論でこの証明を導ける(リスト~\ref{src:agda-push-pop-proof})。

なお、今回 SingleLinkedStack に積むことができる値は Agda の標準ライブラリ(\verb/Data.Nat/)における自然数型 $ \mathbb{N} $ としている。
push/pop 操作の後の継続が \verb/Meta/ に影響を与えない制約は \verb/id-meta/ に表れている。
これは \verb/Meta/ を構成する要素を受け取り、継続先の CodeSegment に恒等関数 \verb/id/ を指定している。
加えて、スタックが空で無い制約 where 句の \verb/meta/ に表れている。
必ずスタックの先頭 \verb/top/ には値xが入っており、それ以降の値は任意としている。
よってスタックは必ず一つ以上の値を持ち、空でないという制約を表わせる。
証明は refl によって与えられる。
つまり定義から自明に推論可能となっている。

\lstinputlisting[label=src:agda-push-pop-proof, caption=Agdaにおけるスタックの性質の証明(1)] {src/AgdaPushPopProof.agda.replaced}

ここで興味深い点は、 SingleLinkedStack の実装から証明に仮定が必要なことが証明途中でに分かった点にある。
例えば、CbC の SingleLinkedStack 実装の push/pop 操作は失敗しても成功しても指定された CodeSegment に軽量継続する。
この性質により、指定された CodeSegment によっては、スタックの操作に関係なく \verb/Meta/ の内部の DataSegemnt が書き換えられる可能性があることが分かった。
スタックの操作の際に行なわれる軽量継続の利用方法は複数考えられる。
例えば、スタックが空である際に pop を行なった時はエラー処理用の継続を行なう、といった実装も可能である。
実装が異なれば、同様の性質でも証明は異なるものとなる。
このように、実装そのものを適切に型システムで定義できれば、明示されていない実装依存の仕様も証明時に確定させることができる。

証明した定理をより一般的な「任意の自然数回だけスタックへ値を積み、その後同じ回数スタックから値を取り出すとスタックは操作前と変わらない」という形に拡張する。
この性質を Agda で定義するとリスト~\ref{src:agda-n-push-n-pop}のようになる。
自然数n回だけ push/pop することを記述するために Agda 上に \verb/n-push/ 関数と \verb/n-pop/ 関数を定義している。
それぞれ一度操作を行なった後に再帰的に自身を呼び出す再帰関数である。

\lstinputlisting[label=src:agda-n-push-n-pop, caption=Agda におけるスタックの性質の定義(2)] {src/AgdaNPushNPop.agda.replaced}

この性質の証明は少々複雑である。
結論から先に示すとリスト~\ref{src:agda-n-push-n-pop-proof}のように証明できる。

\lstinputlisting[label=src:agda-n-push-n-pop-proof, caption=Agda におけるスタックの性質の証明(2)] {src/AgdaNPushNPopProof.agda.replaced}

これは以下のような形の証明になっている。

\begin{itemize}
    \item 「n回pushした後にn回popしても同様になる」という定理を \verb/n-push-pop/ とおく。
    \item \verb/n-push-pop/ は自然数nと特定の \verb/Meta/ に対して \verb/exec (n-pop (suc n)) . (n-push (suc n))) m = m/ が成り立つことである
    \item 特定の \verb/Meta/ とは、 push/pop 操作の後の継続が DataSegment を変更しない \verb/Meta/ である。
    \item また、簡略化のために \verb/csComp/ による CodeSegment の合成を二項演算子 \verb/./ とおく
        \begin{itemize}
            \item 例えば \verb/exec (csComp f g) x/ は \verb/exec (f . g) x/ となる。
        \end{itemize}

    \item \verb/n-push-pop/ を証明するための補題 \verb/pop-n-push/ を定義する
    \item \verb/n-push-pop/ とは「n+1回push して1回 pop することは、n回pushすることと等しい」という補題である。
    \item \verb/n-push-pop/ は \verb/exec (pop . n-push (suc n)) m = exec (n-push n) m/ と表現できる。
    \item \verb/n-push-pop/ の n が zero の時は直ちに成り立つ。
    \item \verb/n-push-pop/ の n が zero でない時(suc n である時)は以下のように証明できる。

        \begin{itemize}
            \item \verb/exec (n-push (suc n)) m/ を \verb/X/ とおく
            \item \verb/exec (pop . n-push (suc (suc n))) m = X/
            \item n-push の定義より \verb/exec (pop . (n-push (suc n) . push)) m = X/
            \item 補題 exec-comp より \verb/exec (pop (exec (n-push (suc n) . push) m)) = X/
            \item 補題 exec-comp より \verb/exec (pop (exec (n-push (suc n) (exec push m)))) = X/
            \item 一度pushした結果を \verb/m'/とおくと \verb/exec (pop (exec (n-push (suc n) m'))) = X/
            \item \verb/n-push-pop/ より \verb/exec (exec (n-push n m')) = X/
            \item push の定義より \verb/exec (exec (n-push n (exec push m))) = X/
            \item n-push の定義より \verb/exec (exec (n-push (suc n) m) = X/ となる
            \item 全く同一の項に変更できたので証明終了
        \end{itemize}


    \item 次に \verb/n-push-pop/ の証明を示す。
    \item \verb/n-push-pop/ の n が zero の時は、 \verb/suc zero/ 回の push/pop が行なわれるため、\verb/push-pop/より成り立つ。
    \item \verb/n-push-pop/ の n が zero でない時は以下により証明できる。

        \begin{itemize}
            \item \verb/exec ((n-pop (suc n)) . (n-push (suc n))) m = m / を示せれば良い。
            \item \verb/X/ に注目した時 n-pop の定義より \verb/exec (n-pop n) . pop . (n-push (suc n)) m = m/
            \item exec-comp より \verb/exec (n-pop n) (exec pop (n-push (suc n)) m) = m/
            \item exec-comp より \verb/exec (n-pop n) (exec pop (exec (n-push (suc n)) m)) = m/
            \item exec-comp より \verb/exec (n-pop n) (exec pop . (n-push (suc n)) m) = m/
            \item pop-n-push より \verb/exec (n-pop n) (exec (n-push n) m) = m/
            \item n-push-pop より \verb/m = m/ となり証明終了。
            \item なお、n-push-pop は (suc n) が n に減少するため、確実に停止することから自身を自身の証明に適用している。
        \end{itemize}
\end{itemize}

push-pop を一般化した n-push-pop を証明することができた。
n-push-pop は証明の途中で補題 pop-n-push と push-pop を利用した定理である。
このように、CbC で記述されたプログラムを Agda 上に記述することで、データ構造の性質を定理として証明することができた。
これらの証明機構を CbC のコンパイラやランタイム、モデルチェッカなどに組み込むことにより CbC は CbC で記述されたコードを証明することができるようになる。
なお、本論文で取り扱っている Agda のソースコードは視認性の向上のために暗黙的な引数を省略して記述している。
動作する完全なコードは付録に付す。

% }}}