|
0
|
1 \chapter{RedBlackTreeとInvariantの実装}
|
|
|
2 本章では，RedBlackTreeとそのInvariantをGearsAgdaを用いて実装していく．
|
|
|
3
|
|
|
4 \section{RedBlackTreeの基本的な実装}
|
|
|
5 第３章１節で説明した通り，BinarySearchTreeをもとにRedBlackTreeの基本的な部分を実装していく．BinarySearchTreeはleafとnodeの二つの要素から構成されており，nodeには以下の４つの要素を持つ．
|
|
|
6 \begin{enumerate}
|
|
|
7 \item key : 自然数であり，この値によって木構造を決定する．
|
|
|
8 \item value : nodeに格納する値である．型は任意で決めることができる．
|
|
|
9 \item left-child : 該当ノードから見た左側に持つ子供ノード．制約により，親のKeyの値よりも小さいKeyを持つ．
|
|
|
10 \item right-child : 該当ノードから見た右側に持つ子供ノード．制約により，親のKeyの値よりも大きいKeyを持つ．
|
|
|
11 \end{enumerate}
|
|
|
12 これらの要素を含むData型をGearsAgdaで記述することで，基本的なBinarySearchTreeの構造を示すことができる．
|
|
|
13
|
|
|
14 \begin{lstlisting}[caption=BinarySearchTreeの基本的な実装 , label=bt.agda]
|
|
|
15 data bt {n : Level} (A : Set n) : Set n where
|
|
|
16 leaf : bt A
|
|
|
17 node : (key : @$\mathbb{N}$@) → (value : A) →
|
|
|
18 (left : bt A ) → (right : bt A ) → bt A
|
|
|
19
|
|
|
20 \end{lstlisting}
|
|
|
21 ソースコード\ref{bt.agda}について解説する．
|
|
|
22
|
|
|
23 1行目ではData型の実装に基づき，bt型を定義している．ここに書かれている(A : Set n)とは，任意の型を1つ受け取るという意味になり，valueの持つ型を指定することができる．
|
|
|
24 前述した通り，BinarySearchTreeはleafとnodeの二つの要素からなるので，直下に要素ごとの処理を記述する必要がある．
|
|
|
25
|
|
|
26 2行目では，leafを定義している．leafはKeyもValueも持たないため，ただbt Aを返すだけ と記述するだけになることが確認できる．
|
|
|
27
|
|
|
28 3行目と４行目ではnodeについて定義している．nodeは必要な４つの要素を入力に受け取り，bt型を返すという実装になっていることが確認できる．
|
|
|
29
|
|
|
30 BinarySearchTreeの基本的な実装を元に色の概念を付け加えることで，RedBlackTreeの基本的な実装を行うことができる．ここでは，Valueに色を組で渡すことで色の概念を付け加える．
|
|
|
31 \begin{lstlisting}[caption=RedBlackTreeの基本的な実装 , label=rbt.agda]
|
|
|
32 data Color : Set where
|
|
|
33 Red : Color
|
|
|
34 Black : Color
|
|
|
35
|
|
|
36 RBTreeTest : bt (Color ∧ @$\mathbb{N}$@)
|
|
|
37 RBTreeTest = node 8 @$\llangle$@ Black , 200 @$\rrangle$@ (node 5 @$\llangle$@ Red , 100 @$\rrangle$@ (_) (_)) (node 10 @$\llangle$@ Red , 300 @$\rrangle$@ (_) (_))
|
|
|
38 \end{lstlisting}
|
|
|
39 ソースコード\ref{rbt.agda}について解説する．
|
|
|
40
|
|
|
41 １行目から３行目では，色の概念を追加するためにColorという名前のData型を定義している．要素にはRedとBlackの二つがあり，二つともただColorを返すだけになっている．
|
|
|
42
|
|
|
43 ５行目では，実際に簡単なRedBlackTreeを記述している．前述した通り，btに与えるValueの値の部分を色と自然数の組にして渡している．今回は例として自然数を用いているが，ここの型は任意に決めることができる．
|
|
|
44
|
|
|
45 ６行目では，RBtreeTestの処理内容を記述している．ここでは例として，第２章４節で説明した図\ref{RedBlackTree.png}のルートノードから見た木構造を実装している．BinarySearchTreeでのvalueに相当する部分が，色と自然数の組として記述されていることが確認できる．また，左の子にKeyが5で赤の子，右の子にKeyが10で赤の子が記述されており，これは第２章４節で説明した図\ref{RedBlackTree.png}の木構造と一致する．Agdaでは，\_ (アンダースコア)を使用することでコンパイラが推論し，記述を省略できる．本来，親ノードから見た孫ノードが入るが，木構造全体を記述すると冗長になるため省略している．
|
|
|
46
|
|
|
47 以上により，GearsAgdaにてRedBlackTreeを記述し木構造を実装できることが確認できた．
|
|
|
48
|
|
|
49 \section{Invariantの実装}
|
|
|
50 第３章２節で説明した通り，本研究ではInvariantを中心に証明を進めていく．本節では，特に重要になる以下のInvariantについての実装を解説していく．
|
|
|
51 \begin{enumerate}
|
|
|
52 \item RBtreeInvariant : 対象の木がRedBlackTreeであることを示す
|
|
|
53 \item stackInvariant : 辿った木を積むstackが辿った順に構成されていることを示す
|
|
|
54 %\item replacedRBTree : 木を置き換えた際に，木が置き換わっていることを示す
|
|
|
55 \end{enumerate}
|
|
|
56 これらのInvariantは，RedBlackTreeにおける操作の正当性を示すのに重要なInvariantとなっている．
|
|
|
57
|
|
|
58 \subsection{RBtreeInvariantの実装}
|
|
|
59 RBtreeInvariantは，対象の木がRedBlackTreeであることを示すInvariantである．これは，RedBlackTreeの可能な値全部の集合であり，RedBlackTreeの表示的意味論そのものになっている．つまり，全体の集合を型として用意し，この型に該当することを示すことで，対象の木はRedBlackTreeであるということを証明することができる．RedBlackTreeの取る可能な値は８種類あり，それぞれについての実装を記述する必要がある．
|
|
|
60
|
|
|
61 \begin{lstlisting}[caption=RBtreeInvariantの実装 , label=RBtreeInvariant.agda]
|
|
|
62 data RBtreeInvariant {n : Level} {A : Set n} : (tree : bt (Color ∧ A)) → Set n where
|
|
|
63 rb-leaf : RBtreeInvariant leaf
|
|
|
64 rb-single : {c : Color} → (key : @$\mathbb{N}$@) → (value : A) → RBtreeInvariant (node key @$\llangle$@ c , value @$\rrangle$@ leaf leaf)
|
|
|
65 rb-right-red : {key key@$_1$@ : @$\mathbb{N}$@} → {value value@$_1$@ : A}
|
|
|
66 → {t t@$_1$@ : bt (Color ∧ A)} → key < key@$_1$@
|
|
|
67 → black-depth t ≡ black-depth t@$_1$@
|
|
|
68 → RBtreeInvariant (node key@$_1$@ @$\llangle$@ Black , value@$_1$@ @$\rrangle$@ t t@$_1$@)
|
|
|
69 → RBtreeInvariant (node key @$\llangle$@ Red , value @$\rrangle$@ leaf (node key@$_1$@ @$\llangle$@ Black , value@$_1$@ @$\rrangle$@ t t@$_1$@))
|
|
|
70 rb-right-black : ?
|
|
|
71 rb-left-red : ?
|
|
|
72 rb-left-black : {key key@$_1$@ : @$\mathbb{N}$@} → {value value@$_1$@ : A}
|
|
|
73 → {t t@$_1$@ : bt (Color ∧ A)} → key < key@$_1$@ → {c : Color}
|
|
|
74 → black-depth t ≡ black-depth t@$_1$@
|
|
|
75 → RBtreeInvariant (node key@$_1$@ @$\llangle$@ c , value@$_1$@ @$\rrangle$@ t t@$_1$@)
|
|
|
76 → RBtreeInvariant (node key @$\llangle$@ Black , value @$\rrangle$@ (node key@$_1$@ @$\llangle$@ c , value@$_1$@ @$\rrangle$@ t t@$_1$@) leaf)
|
|
|
77 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)}
|
|
|
78 → key < key@$_1$@ → key@$_1$@ < key@$_2$@
|
|
|
79 → 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$@)
|
|
|
80 → RBtreeInvariant (node key @$\llangle$@ Black , value @$\rrangle$@ t@$_1$@ t@$_2$@)
|
|
|
81 → RBtreeInvariant (node key@$_2$@ @$\llangle$@ Black , value@$_2$@ @$\rrangle$@ t@$_3$@ t@$_4$@)
|
|
|
82 → 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$@))
|
|
|
83 rb-node-black : ?
|
|
|
84 \end{lstlisting}
|
|
|
85 ソースコード\ref{RBtreeInvariant.agda}を解説していく．
|
|
|
86
|
|
|
87 agdaでは「？」と記述することで，該当箇所の記述を省略することができる．ここでは，全体を記述すると冗長になってしまうため，最低限の説明が必要な部分を除き，記述を省略している．
|
|
|
88
|
|
|
89 1行目では，RBtreeIvariant型を定義している．入力として，RedBlackTreeを受け取る．
|
|
|
90
|
|
|
91 2行目ではrb-leafを定義しており，これはleafのInvariantを示している．RBtreeInvariantの引数にleafを渡すことで実装している．
|
|
|
92
|
|
|
93 3行目ではrb-singleを定義しており，これはノードの左右にleafがついている木の最小単位のようなノードを示している．RBtreeInvaritantの引数に (node key$\llangle$c , value $\rrangle$ leaf leaf)を渡すことで実装している．
|
|
|
94
|
|
|
95 4行目から8行目までは，rb-right-redを定義しており，これはノードの右側に子ノード，左側にはleafがあるようなノードのInvariantを示している．
|
|
|
96 また，親ノードは赤と黒の2パターン存在するので，それぞれ別に定義する必要があり，4行目から8行目は赤の親ノード，9行目は黒の親ノードを定義している．
|
|
|
97
|
|
|
98 5行目では，$key \textless key_1$ を入力として受けるように記述されている．これは，このInvariantを示すためには，親子間のKeyの大小関係を必ず明示しなければいけないという意味になり，Keyの制約を満たす場合のみを通すことから，このInvariantを示すことで，Keyの正当性を示すことが可能になる．
|
|
|
99
|
|
|
100 ６行目では，親ノードからみた孫ノードの黒の深さが同じであることを入力として受けている．これはKeyの大小関係と同じように，このInvariantを示すことで，黒の深さの正当性を示すことが可能になる．
|
|
|
101
|
|
|
102 7行目では，子ノードの色が黒であるInvariantを入力として受けている．rb-right-redでは，親は赤ノードであるため，必ず子ノードは黒であるという条件を含めていることが確認できる．
|
|
|
103
|
|
|
104 11行目から15行目では，rb-left-blackを定義しており，これはノードの右側にleaf，左側には子ノードがあるようなノードのInvariantを示している．
|
|
|
105 これは，前述したrb-right-red,rb-right-blackの左右の子を入れ替えたものであり，本質的な構造は似ているため，説明を省略する．
|
|
|
106 ただし，親ノードが黒のとき，子ノードは赤と黒の2パターンが存在し，どちらの色でも可能という意味で$\llangle$c , value $\rrangle$と記述されている．
|
|
|
107
|
|
|
108 16行目から21行目では，rb-node-redを定義しており，これは左右それぞれに子ノードを持つようなノードのInvariantを示している．
|
|
|
109 また，親ノードは赤と黒の2パターン存在するので，それぞれ別に定義する必要があり，16行目から21行目は赤の親ノード，22行目からは黒の親ノードを定義している．
|
|
|
110
|
|
|
111 以上のように，RedBlackTreeの制約をInvariantの入力に含めることで，これを示した際にRedBlackTreeの正当性を証明することができる．
|
|
|
112
|
|
|
113 \subsection{stackInvariantの実装}
|
|
|
114 GearsOSのファイルシステムとデータベースでは，非破壊的なRedBlackTreeを採用することが予定されている．非破壊的とは，操作を行う際に木を上書きせず，コピーして木を構築することを意味し，読み込みと書き込みを同時に行うことができるなどの利点がある．非破壊的なRedBlackTreeを構築するためにはstackを使う必要がある．
|
|
|
115
|
|
|
116 stackInvariantとは，木の操作を行う際に辿った木を積むstackが，辿った順に構成されていることを示すInvariantである．つまり，このInvariantを示すことで，対象のstackが積んできた木の履歴を見れるような形になっている．これを実装することにより，木をバランスさせる際などにstackを見て，ひとつ前の木に戻り操作を行うなどの実装が可能になる．
|
|
|
117
|
|
|
118 \begin{lstlisting}[caption=stackInvariantの実装 , label=stackInvariant.agda]
|
|
|
119 data stackInvariant {n : Level} {A : Set n} (key : @$\mathbb{N}$@) : (top orig : bt A) → (stack : List (bt A)) → Set n where
|
|
|
120 s-nil : {tree0 : bt A} → stackInvariant key tree0 tree0 (tree0 :: [])
|
|
|
121 s-right : (tree tree0 tree@$_1$@ : bt A) → {key@$_1$@ : @$\mathbb{N}$@ } → {v1 : A } → {st : List (bt A)}
|
|
|
122 → key@$_1$@ < key
|
|
|
123 → stackInvariant key (node key@$_1$@ v1 tree@$_1$@ tree) tree0 st
|
|
|
124 → stackInvariant key tree tree0 (tree :: st)
|
|
|
125 s-left : (tree@$_1$@ tree0 tree : bt A) → {key@$_1$@ : @$\mathbb{N}$@ } → {v1 : A } → {st : List (bt A)}
|
|
|
126 → key < key@$_1$@
|
|
|
127 → stackInvariant key (node key@$_1$@ v1 tree@$_1$@ tree) tree0 st
|
|
|
128 → stackInvariant key tree@$_1$@ tree0 (tree@$_1$@ :: st)
|
|
|
129 \end{lstlisting}
|
|
|
130 ソースコード\ref{stackInvariant.agda}について解説する．
|
|
|
131
|
|
|
132 1行目では，stackInvariantの型を定義している．入力は，key,top,orig,stackの4つを受け取る．topとorigは両方ともbt型であり，topはstackの一番上にある木，origは一番下にある木を意味する．GearsAgdaにおいて，stackはList型を用いて定義する．List型は，任意の型を中に持ち，List (bt A)の書くことで木をListの中に持たせることができる．List型は， (tree0 :: [])のように記述することができ，「::」で要素同士を並べていく．「[]」は空であることを意味し，Listの終わりであることを示す．
|
|
|
133
|
|
|
134 ２行目では，stackの最小単位であるs-nilを定義している．これは，topとorigに受け取る木が同じであるといった特徴がある．
|
|
|
135
|
|
|
136 ３行目から６行目では，s-rightを定義している．
|
|
|
137 ５行目を見ると，入力でstackInvariantを受け取っている．これは，一個前の木で示されたstackInvariantであり，s-rightでは，この木の右側の子をstackに積んだことを示す．
|
|
|
138 ４行目を見ると，keyの大小関係を入力として受け取っており，対象のKeyよりも一個前のkey$_1$が小さく，木の順序性を保っていることが確認できる．
|
|
|
139 ６行目では，一個前のstackInvariantが示しているstackのstに，新たな木を積んだことを示すstackを(tree :: st)と表していることが確認できる．
|
|
|
140
|
|
|
141 7行目から10行目では，s-leftを定義している．s-leftでは右側ではなく左側の子をstackに積んだことを示すInvariantになっている．その他の大まかな実装はs-rightと同じであるため，説明を省略する．
|
|
|
142
|
|
|
143 以上により，一番下の木origから，対象の木topまでを辿った木を積むstackの正当性を示すInvariantを定義することができた．
|
|
|
144 %\subsection{replacedRBTreeの実装}
|
|
|
145
|
|
|
146
|
|
|
147
|
|
|
148
|
|
|
149
|
|
|
150
|
|
|
151
|
|
|
152
|
|
|
153
|
|
|
154
|
|
|
155
|
|
|
156
|
|
|
157
|
|
|
158
|
|
|
159
|
|
|
160
|
|
|
161
|
|
|
162
|
|
|
163
|
|
|
164
|
|
|
165
|
|
|
166
|
|
|
167
|
