\section{Gears Agda における木構造の設計}

本研究では、Gears Agda にて Red Black Tree の検証を行うにあたり、
Agda が変数に対して再代入を許していないことが問題になってくる。

そのため下図のように、木構造の root から leaf　に 辿る際に見ているnodeから
下の　tree をそのまま stack に持つようにする。

そして insert や delete を行った後に stack から tree を取り出し、
元の木構造を再構築 していきながら　rootへ戻る。

このようにして Gears Agda にて Red Black Tree を実装していく。

\section{Gears Agda における Binary Tree の実装}

Red Black Tree を実装しそれを検証する前段階として、
実装が簡単な Binary Tree の実装から行う。

まず Binary Tree と 遷移させる Data Gear となる Env の定義は Code \ref{bt_env} のようになる。

\lstinputlisting[label=bt_env, caption=Binary Tree の Data Gear] {src/bt_impl/bt_env.agda.replaced}

bt は、木での順序としての意味を持つ key とその中身 value はどのような型でも入れられるように
「A : Set n」となっている。
そして left, right には bt A を持つようにし、木構造を構築している。

Env では、 find, insert, delete の対象となる値を保存し、 Code Gear に与えられるようにするために
varn, varv を持っている。
加えて変更を加える bt を持つ vart と、章Nで前述した木構造を持っておくための List である
varl を Env に設定している。

7章で述べた Gears Agda での木構造を保ったまま root から目的のnodeまで辿る Code Gear が
Code \ref{bt_find_impl} になる。

\lstinputlisting[label=bt_find_impl, caption=root から目的のnodeまで辿る Code Gear] {src/bt_impl/find.agda.replaced}

まず、関数の実装が始まってすぐに Env の vartを指定したものと引数をそのまま find-c の関数に遷移している。
ここで展開しているのは Env の vart で、そのまま Env から展開した vart をパターンマッチすると
Agda が追えなくなってしまい、\{-$\#$ TERMINATING $\#$-\} を使用することになってしまう。

そのため関数を新たに定義し、展開したものを受け取り、パターンマッチすることで
\{-$\#$ TERMINATING $\#$-\} を使用せずに loopを定義できるようになる

木を stack に入れるのは単純で、操作の対象の key となる varn と
node のkeyを比較を行う。
そこからは本来の木構造と同じで、操作の対象の key が小さいなら
left の tree を次の node として遷移する。
大きいなら right の tree を次の node として遷移していく。

操作の対象となる node に辿り着き、操作を行った後、
Stack に持っている tree から再構築を行う。

そのコードが Code \ref{bt_replace_impl} となる

\lstinputlisting[label=bt_replace_impl, caption=Stack から tree を再構築する Code Gear] {src/bt_impl/replace.agda.replaced}

これも Code \ref{bt_find_impl} と同じように構成されており、
varn と node の key を比較し、 vart を List から持ってきた node の どこに加えるかを決めるようになっている。

以上の流れを繋げることで、 Binary Tree の insert と find を実装できた。
delete は insert の値を消すようにすると実装ができる。

\section{Gears Agda における Binary Tree の検証}

検証も前述した While Loop の 検証と同じようにしていく。
しかし、 Binary Tree の不変条件は2つ以上あるため、これを関数定義の際に全て書くと
煩雑になってしまうため、事前に記述して関数化しておく。
それが Code \ref{bt_invariant} になる。

\lstinputlisting[label=bt_invariant, caption=Binary Tree の 不変条件] {src/bt_verif/invariant.agda.replaced}

この不変条件は、 treeInvariant が　tree の 左にある node の key が小さく、
右にある node の方が大きいことを条件としている。

stackInvariant は Stack にある tree が、次に取り出す Tree の一部であることを
条件としている。

これを先ほど実装した Code Gear に対して加えることで検証していく。
先ほど実装した Code \ref{bt_find_impl} に対して加えると Code ref のようになる。


\lstinputlisting[label=bt_invariant, caption=Binary Tree の 不変条件] {src/bt_verif/find.agda.replaced}

現時点では条件を満たしていることの証明まで行っていないが
コード中の {!!} に記述を行い、前述した While Loop と同じように中身を記述することで検証を行える。