|
0
|
1 \chapter{Red Black Tree の実装}
|
|
|
2
|
|
|
3 Left Learning Red Black Tree の実装において、
|
|
|
4 通常の言語であれば再起処理を用いて実装を行える部分を
|
|
|
5 継続にて実行可能なように変更する必要がある。
|
|
|
6 本節では、この課題に対して Gears Agda での
|
|
|
7 Left Learning Red Black Tree の実装方法について述べる。
|
|
|
8
|
|
|
9 \section{Gears Agda での Red Black Tree の 記述}
|
|
|
10 Gears Agda にて Red Black Tree を実装する際の手順を、
|
|
|
11 下\figref{rbt_imple}を参考に説明する。
|
|
|
12
|
|
|
13 \begin{figure}[H]
|
|
|
14 \begin{center}
|
|
|
15 \includegraphics[height=7.5cm]{pic/imple.pdf}
|
|
|
16 \end{center}
|
|
|
17 \caption{再起処理を回避する手順}
|
|
|
18 \label{rbt_imple}
|
|
|
19 \end{figure}
|
|
|
20
|
|
|
21 41の値を Left Leaning Red Black Tree に insert もしくは delete する際の手順を説明する。
|
|
|
22 まず Root node である 59 と比較した際に、41はそれより小さい。
|
|
|
23 この際、left node に遷移するが、CbC では再起処理が行えないため、listに保持していく。
|
|
|
24 順々に辿っていき、対象の場所に到達すると insert / delete を行う。
|
|
|
25 その後はlistからnodeを取り出し、結合することで Left Leaning Red Black Tree の操作を行う。
|
|
|
26
|
|
|
27 \subsection{定義した Data Gear の記述}
|
|
|
28
|
|
|
29 Left Learning Red Black Tree の記述の際に、 Code Gear
|
|
|
30 に渡している Data Gear である Env の記述を \coderef{env_imple} に示す。
|
|
|
31
|
|
|
32 \lstinputlisting[label=env_imple, caption=insertにて目的の nodeまで辿るプログラム, firstline=13, lastline=39] {src/agda/rbt_t.agda}
|
|
|
33
|
|
|
34 箇条書きにてそれぞれについて解説を行う。
|
|
|
35
|
|
|
36
|
|
|
37 \begin{itemize}
|
|
|
38 \item col: 色のことで、red と black の data 型で記述し、パターンマッチを行う。
|
|
|
39 \item node: その名の通り node に格納されている値を保存する。 色と自然数が入る
|
|
|
40 \item tree: tree の構造 を保存する。ここで node と x / right tree を持つ
|
|
|
41 \item rbt: 上3つの要素を合わせて持つことで Left Learning Red Black Tree を定義する
|
|
|
42 \item Env: rbt 以外に追加や削除を行う対象となる値と、 rbtを保存できる List を持つ Data Gear
|
|
|
43 \end{itemize}
|
|
|
44
|
|
|
45 \subsection{目的の node まで辿る Gears Agda}
|
|
|
46 上記に示した手順通りにAgdaで記述すると下 \coderef{insert_imple}のようになる。
|
|
|
47 例は insert を行う場合の記述となる。
|
|
|
48
|
|
|
49 \lstinputlisting[label=insert_imple, caption=insertにて目的の nodeまで辿るプログラム, firstline=157, lastline=166] {src/agda/rbt_t.agda}
|
|
|
50
|
|
|
51 ソースコードの解説をする。上から3行はコメントで、この関数で行っていることを doに、
|
|
|
52 next / exit では4章で述べた次の関数遷移先を記載している。
|
|
|
53
|
|
|
54 5行目にて withを使用することで vart のパターンマッチを行っている。
|
|
|
55 vart が bt-empty である場合に 6行目が動作する。
|
|
|
56 bt-empty であれば node の一番下であるため、
|
|
|
57 varn を tree の値として insert して exit に遷移する。
|
|
|
58
|
|
|
59 7行目は vart が bt-empty ではないパターンの動作を記述している。
|
|
|
60 ここでは insertを行う値である varn と 現在いる位置の tree の値と比較を行い、
|
|
|
61 再度パターンマッチを行う。
|
|
|
62
|
|
|
63 8行目は比較した結果、同値だった場合であり、そのままexitに遷移している。
|
|
|
64
|
|
|
65 9行目は入力の値 varn の方が小さい場合を指している。
|
|
|
66 vart に left tree を入れ、varl には 現在の tree から left treeを除いた
|
|
|
67 treeを追加している。それを next に遷移させている。
|
|
|
68
|
|
|
69 10行目は入力の値 varn の方が大きい場合を指している。
|
|
|
70 9行目とは逆に、vart に right tree を入れ、varl には 現在の tree から right treeを除いた
|
|
|
71 treeを追加している。それをまたnext に遷移させている。
|
|
|
72
|
|
|
73 以上の手順により、目的の node まで辿っている。
|
|
|
74
|
|
|
75 \subsection{目的の node まで辿った後の Gears Agda}
|
|
|
76 目的の node にたどり着いた後、List に格納された tree と vart の結合を行う。
|
|
|
77 Gears Agda でそれを記述すると\coderef{mearge_imple}のようになる。
|
|
|
78
|
|
|
79 \lstinputlisting[label=mearge_imple, caption=insertにて目的の nodeまで辿るプログラム, firstline=145, lastline=155] {src/agda/rbt_t.agda}
|
|
|
80 ソースコードの解説をする。
|
|
|
81 5行目にて with を使用して varl についてパターンマッチを行っている。
|
|
|
82
|
|
|
83 6行目が varl に何も入っていない場合で、実行終了のため exitに遷移している。
|
|
|
84
|
|
|
85 7行目は varl に何か入っていた場合で、ここでは varl に入っているものが
|
|
|
86 何であるのか8行目と合わせてパターンマッチを行っている。
|
|
|
87 ここでは varl に入っていたものが bt-empty であった場合について記述されている。
|
|
|
88 bt-emptyが入ってくることは実装上ありえないので、exitに遷移することで強制終了している。
|
|
|
89
|
|
|
90 8行目では varl に入っていたものが bt-empty ではなかった場合で、
|
|
|
91 それをxtreeと命名している。
|
|
|
92 ここで vart に入っている値と xtree に入っている値を比較を行い、
|
|
|
93 さらにパターンマッチを行う。
|
|
|
94
|
|
|
95 9行目が入っている値と同じ値であった場合で、
|
|
|
96 特に操作する必要がないので vart に xtree を入れ、
|
|
|
97 varl を一つ進める。
|
|
|
98
|
|
|
99 10行目は vartが大きい場合で、
|
|
|
100 varnに xtree の値を入れ、
|
|
|
101 xtree の right tree に
|
|
|
102 現在のvart を入れたものを vartにして
|
|
|
103 varlを一つ進めている。
|
|
|
104
|
|
|
105 11行目は vartが小さい場合で、
|
|
|
106 10行目と逆のことをしている。
|
|
|
107 varnに xtree の値を入れ、
|
|
|
108 xtree の left tree に
|
|
|
109 現在のvart を入れたものを vartにして
|
|
|
110 varlを一つ進めている。
|
|
|
111
|
|
|
112 以上の組み合わせを行い、
|
|
|
113 Gears Agda にて 再起処理を使わず
|
|
|
114 に Left Learning Red Black Tree の insert / delete を
|
|
|
115 記述した。
|
|
|
116
|
|
|
117
|
|
|
118 % 以上のように Tree の基本操作である insert, find, delete の実装を行った。
|
|
|
119
|
|
|
120
|
