\chapter{RedBlackTreeとInvariantの実装}
本章では，RedBlackTreeとそのInvariantをGearsAgdaを用いて実装していく．

\section{RedBlackTreeの基本的な実装}
第３章１節で説明した通り，BinarySearchTreeをもとにRedBlackTreeの基本的な部分を実装していく．BinarySearchTreeはleafとnodeの二つの要素から構成されており，nodeには以下の４つの要素を持つ．
\begin{enumerate}
\item key : 自然数であり，この値によって木構造を決定する．
\item value : nodeに格納する値である．型は任意で決めることができる．
\item left-child : 該当ノードから見た左側に持つ子供ノード．制約により，親のKeyの値よりも小さいKeyを持つ．
\item right-child : 該当ノードから見た右側に持つ子供ノード．制約により，親のKeyの値よりも大きいKeyを持つ．
\end{enumerate}
これらの要素を含むData型をGearsAgdaで記述することで，基本的なBinarySearchTreeの構造を示すことができる．

\begin{lstlisting}[caption=BinarySearchTreeの基本的な実装 , label=bt.agda]
data bt {n : Level} (A : Set n) : Set n where
  leaf : bt A
  node :  (key : @$\mathbb{N}$@) → (value : A) →
    (left : bt A ) → (right : bt A ) → bt A
  
\end{lstlisting}
ソースコード\ref{bt.agda}について解説する．

1行目ではData型の実装に基づき，bt型を定義している．ここに書かれている(A : Set n)とは，任意の型を1つ受け取るという意味になり，valueの持つ型を指定することができる．
前述した通り，BinarySearchTreeはleafとnodeの二つの要素からなるので，直下に要素ごとの処理を記述する必要がある．

2行目では，leafを定義している．leafはKeyもValueも持たないため，ただbt Aを返すだけ と記述するだけになることが確認できる．

3行目と４行目ではnodeについて定義している．nodeは必要な４つの要素を入力に受け取り，bt型を返すという実装になっていることが確認できる．

BinarySearchTreeの基本的な実装を元に色の概念を付け加えることで，RedBlackTreeの基本的な実装を行うことができる．ここでは，Valueに色を組で渡すことで色の概念を付け加える．
\begin{lstlisting}[caption=RedBlackTreeの基本的な実装 , label=rbt.agda]
data Color  : Set where
    Red : Color
    Black : Color
 
RBTreeTest : bt (Color ∧ @$\mathbb{N}$@)
RBTreeTest = node 8  @$\llangle$@  Black , 200 @$\rrangle$@  (node 5  @$\llangle$@  Red , 100 @$\rrangle$@  (_) (_)) (node 10  @$\llangle$@  Red , 300 @$\rrangle$@  (_) (_))
\end{lstlisting}
ソースコード\ref{rbt.agda}について解説する．

１行目から３行目では，色の概念を追加するためにColorという名前のData型を定義している．要素にはRedとBlackの二つがあり，二つともただColorを返すだけになっている．

５行目では，実際に簡単なRedBlackTreeを記述している．前述した通り，btに与えるValueの値の部分を色と自然数の組にして渡している．今回は例として自然数を用いているが，ここの型は任意に決めることができる．

６行目では，RBtreeTestの処理内容を記述している．ここでは例として，第２章４節で説明した図\ref{RedBlackTree.png}のルートノードから見た木構造を実装している．BinarySearchTreeでのvalueに相当する部分が，色と自然数の組として記述されていることが確認できる．また，左の子にKeyが5で赤の子，右の子にKeyが10で赤の子が記述されており，これは第２章４節で説明した図\ref{RedBlackTree.png}の木構造と一致する．Agdaでは，\_ (アンダースコア)を使用することでコンパイラが推論し，記述を省略できる．本来，親ノードから見た孫ノードが入るが，木構造全体を記述すると冗長になるため省略している．

以上により，GearsAgdaにてRedBlackTreeを記述し木構造を実装できることが確認できた．

\section{Invariantの実装}
第３章２節で説明した通り，本研究ではInvariantを中心に証明を進めていく．本節では，特に重要になる以下のInvariantについての実装を解説していく．
\begin{enumerate}
\item RBtreeInvariant : 対象の木がRedBlackTreeであることを示す
\item stackInvariant : 辿った木を積むstackが辿った順に構成されていることを示す
%\item replacedRBTree : 木を置き換えた際に，木が置き換わっていることを示す
\end{enumerate}
これらのInvariantは，RedBlackTreeにおける操作の正当性を示すのに重要なInvariantとなっている．

\subsection{RBtreeInvariantの実装}
RBtreeInvariantは，対象の木がRedBlackTreeであることを示すInvariantである．これは，RedBlackTreeの可能な値全部の集合であり，RedBlackTreeの表示的意味論そのものになっている．つまり，全体の集合を型として用意し，この型に該当することを示すことで，対象の木はRedBlackTreeであるということを証明することができる．RedBlackTreeの取る可能な値は８種類あり，それぞれについての実装を記述する必要がある．

\begin{lstlisting}[caption=RBtreeInvariantの実装 , label=RBtreeInvariant.agda]
data RBtreeInvariant {n : Level} {A : Set n} : (tree : bt (Color ∧ A)) → Set n where
    rb-leaf : RBtreeInvariant leaf
    rb-single :  {c : Color} → (key : @$\mathbb{N}$@) → (value : A) →  RBtreeInvariant (node key  @$\llangle$@ c , value @$\rrangle$@ leaf leaf)
    rb-right-red : {key key@$_1$@ : @$\mathbb{N}$@} → {value value@$_1$@ : A} 
       → {t t@$_1$@ : bt (Color ∧ A)} → key < key@$_1$@
       → black-depth t ≡ black-depth t@$_1$@
       → RBtreeInvariant (node key@$_1$@ @$\llangle$@ Black , value@$_1$@ @$\rrangle$@ t t@$_1$@)
       → RBtreeInvariant (node key  @$\llangle$@ Red ,   value  @$\rrangle$@ leaf (node key@$_1$@ @$\llangle$@ Black , value@$_1$@ @$\rrangle$@ t t@$_1$@))
    rb-right-black : ? 
    rb-left-red : ?
    rb-left-black : {key key@$_1$@ : @$\mathbb{N}$@} → {value value@$_1$@ : A} 
       → {t t@$_1$@ : bt (Color ∧ A)} → key < key@$_1$@ → {c : Color}
       → black-depth t ≡ black-depth t@$_1$@
       → RBtreeInvariant (node key@$_1$@ @$\llangle$@ c     , value@$_1$@ @$\rrangle$@ t t@$_1$@)
       → RBtreeInvariant (node key  @$\llangle$@ Black , value  @$\rrangle$@ (node key@$_1$@ @$\llangle$@ c , value@$_1$@ @$\rrangle$@ t t@$_1$@) leaf)
    rb-node-red  : {key key@$_1$@ key@$_2$@ : @$\mathbb{N}$@} → {value value@$_1$@ value@$_2$@ : A} → {t@$_1$@ t@$_2$@ t@$_3$@ t@$_4$@ : bt (Color ∧ A)} 
       → key < key@$_1$@ → key@$_1$@ < key@$_2$@
       → black-depth (node key  @$\llangle$@  Black  , value  @$\rrangle$@  t@$_1$@ t@$_2$@) ≡ black-depth (node key@$_2$@ @$\llangle$@  Black , value@$_2$@ @$\rrangle$@  t@$_3$@ t@$_4$@)
       → RBtreeInvariant (node key @$\llangle$@ Black , value @$\rrangle$@ t@$_1$@ t@$_2$@)
       → RBtreeInvariant (node key@$_2$@ @$\llangle$@ Black , value@$_2$@ @$\rrangle$@ t@$_3$@ t@$_4$@)
       → RBtreeInvariant (node key@$_1$@ @$\llangle$@ Red , value@$_1$@ @$\rrangle$@ (node key @$\llangle$@ Black , value @$\rrangle$@ t@$_1$@ t@$_2$@) (node key@$_2$@ @$\llangle$@ Black , value@$_2$@ @$\rrangle$@ t@$_3$@ t@$_4$@))
    rb-node-black  : ?
\end{lstlisting}
ソースコード\ref{RBtreeInvariant.agda}を解説していく．

agdaでは「？」と記述することで，該当箇所の記述を省略することができる．ここでは，全体を記述すると冗長になってしまうため，最低限の説明が必要な部分を除き，記述を省略している．

1行目では，RBtreeIvariant型を定義している．入力として，RedBlackTreeを受け取る．

2行目ではrb-leafを定義しており，これはleafのInvariantを示している．RBtreeInvariantの引数にleafを渡すことで実装している．

3行目ではrb-singleを定義しており，これはノードの左右にleafがついている木の最小単位のようなノードを示している．RBtreeInvaritantの引数に (node key$\llangle$c , value $\rrangle$ leaf leaf)を渡すことで実装している．

4行目から8行目までは，rb-right-redを定義しており，これはノードの右側に子ノード，左側にはleafがあるようなノードのInvariantを示している．
また，親ノードは赤と黒の2パターン存在するので，それぞれ別に定義する必要があり，4行目から8行目は赤の親ノード，9行目は黒の親ノードを定義している．

5行目では，$key  \textless key_1$ を入力として受けるように記述されている．これは，このInvariantを示すためには，親子間のKeyの大小関係を必ず明示しなければいけないという意味になり，Keyの制約を満たす場合のみを通すことから，このInvariantを示すことで，Keyの正当性を示すことが可能になる．

６行目では，親ノードからみた孫ノードの黒の深さが同じであることを入力として受けている．これはKeyの大小関係と同じように，このInvariantを示すことで，黒の深さの正当性を示すことが可能になる．

7行目では，子ノードの色が黒であるInvariantを入力として受けている．rb-right-redでは，親は赤ノードであるため，必ず子ノードは黒であるという条件を含めていることが確認できる．

11行目から15行目では，rb-left-blackを定義しており，これはノードの右側にleaf，左側には子ノードがあるようなノードのInvariantを示している．
これは，前述したrb-right-red,rb-right-blackの左右の子を入れ替えたものであり，本質的な構造は似ているため，説明を省略する．
ただし，親ノードが黒のとき，子ノードは赤と黒の2パターンが存在し，どちらの色でも可能という意味で$\llangle$c     , value $\rrangle$と記述されている．

16行目から21行目では，rb-node-redを定義しており，これは左右それぞれに子ノードを持つようなノードのInvariantを示している．
また，親ノードは赤と黒の2パターン存在するので，それぞれ別に定義する必要があり，16行目から21行目は赤の親ノード，22行目からは黒の親ノードを定義している．

以上のように，RedBlackTreeの制約をInvariantの入力に含めることで，これを示した際にRedBlackTreeの正当性を証明することができる．

\subsection{stackInvariantの実装}
GearsOSのファイルシステムとデータベースでは，非破壊的なRedBlackTreeを採用することが予定されている．非破壊的とは，操作を行う際に木を上書きせず，コピーして木を構築することを意味し，読み込みと書き込みを同時に行うことができるなどの利点がある．非破壊的なRedBlackTreeを構築するためにはstackを使う必要がある．

stackInvariantとは，木の操作を行う際に辿った木を積むstackが，辿った順に構成されていることを示すInvariantである．つまり，このInvariantを示すことで，対象のstackが積んできた木の履歴を見れるような形になっている．これを実装することにより，木をバランスさせる際などにstackを見て，ひとつ前の木に戻り操作を行うなどの実装が可能になる．

\begin{lstlisting}[caption=stackInvariantの実装 , label=stackInvariant.agda]
data stackInvariant {n : Level} {A : Set n}  (key : @$\mathbb{N}$@) : (top orig : bt A) → (stack  : List (bt A)) → Set n where
    s-nil :  {tree0 : bt A} → stackInvariant key tree0 tree0 (tree0 :: [])
    s-right :  (tree tree0 tree@$_1$@ : bt A) → {key@$_1$@ : @$\mathbb{N}$@ } → {v1 : A } → {st : List (bt A)}
        → key@$_1$@ < key  
        →  stackInvariant key (node key@$_1$@ v1 tree@$_1$@ tree) tree0 st
        → stackInvariant key tree tree0 (tree :: st)
    s-left :  (tree@$_1$@ tree0 tree : bt A) → {key@$_1$@ : @$\mathbb{N}$@ } → {v1 : A } → {st : List (bt A)}
        → key  < key@$_1$@
        →  stackInvariant key (node key@$_1$@ v1 tree@$_1$@ tree) tree0 st 
        → stackInvariant key tree@$_1$@ tree0 (tree@$_1$@ :: st)
\end{lstlisting}
ソースコード\ref{stackInvariant.agda}について解説する．

1行目では，stackInvariantの型を定義している．入力は，key,top,orig,stackの4つを受け取る．topとorigは両方ともbt型であり，topはstackの一番上にある木，origは一番下にある木を意味する．GearsAgdaにおいて，stackはList型を用いて定義する．List型は，任意の型を中に持ち，List (bt A)の書くことで木をListの中に持たせることができる．List型は， (tree0 :: [])のように記述することができ，「::」で要素同士を並べていく．「[]」は空であることを意味し，Listの終わりであることを示す．

２行目では，stackの最小単位であるs-nilを定義している．これは，topとorigに受け取る木が同じであるといった特徴がある．

３行目から６行目では，s-rightを定義している．
５行目を見ると，入力でstackInvariantを受け取っている．これは，一個前の木で示されたstackInvariantであり，s-rightでは，この木の右側の子をstackに積んだことを示す．
４行目を見ると，keyの大小関係を入力として受け取っており，対象のKeyよりも一個前のkey$_1$が小さく，木の順序性を保っていることが確認できる．
６行目では，一個前のstackInvariantが示しているstackのstに，新たな木を積んだことを示すstackを(tree :: st)と表していることが確認できる．

7行目から10行目では，s-leftを定義している．s-leftでは右側ではなく左側の子をstackに積んだことを示すInvariantになっている．その他の大まかな実装はs-rightと同じであるため，説明を省略する．

以上により，一番下の木origから，対象の木topまでを辿った木を積むstackの正当性を示すInvariantを定義することができた．
%\subsection{replacedRBTreeの実装}