Binary file paper/final_thesis.pdf has changed

Binary file paper/pic/imple/実装.pdf has changed

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/src/agda/rbt_imple.agda	Sun Feb 14 21:23:12 2021 +0900
@@ -0,0 +1,140 @@
+module rbt_imple where
+
+open import Level renaming ( suc to succ ; zero to Zero )
+open import Relation.Binary
+open import Data.Nat hiding (_≤_  ; _≤?_)
+open import Data.List hiding ([_])
+open import Data.Product
+open import Data.Nat.Properties as NP
+
+open import rbt_t
+
+--このmutalの部分は別場所に書いてimportしたい。その方が綺麗に検証できそう
+mutual
+  data  right-List : Set where
+    [] : right-List
+    [_] : ℕ → right-List
+    _∷>_Cond_ : (x : ℕ) → (xs : right-List ) → (p : x Data.Nat.> top-r xs) → right-List
+
+  top-r : right-List → ℕ
+  top-r [] = {!!}
+  top-r [ x ] = x
+  top-r (x ∷> l Cond x₁) = x
+
+  insert-r : ℕ → right-List → right-List
+  insert-r x l with l
+  ... | [] = {!!}
+  ... | [ y ] = ?
+  ... | y ∷> ys Cond p with <-cmp x y
+  ... | tri< a ¬b ¬c = l
+  ... | tri≈ ¬a b ¬c = l
+  ... | tri> ¬a ¬b c = x ∷> l Cond c
+
+  data  left-List : Set where
+    [] : left-List
+    [_] : ℕ -> left-List
+    _<∷_Cond_ : (x : ℕ) -> (xs : left-List ) -> (p : x Data.Nat.< top-l xs) -> left-List
+
+  top-l : left-List → ℕ
+  top-l [] = {!!}
+  top-l [ x ] = x
+  top-l (x <∷ l Cond x₁) = x
+
+  insert-l : ℕ -> left-List -> left-List
+  insert-l x [] = [ x ]
+  insert-l x l@([ y ]) with <-cmp x y
+  ... | tri< a ¬b ¬c = x <∷ l Cond a
+  ... | tri≈ ¬a b ¬c = l
+  ... | tri> ¬a ¬b c = l
+  insert-l x l@(y <∷ ys Cond p) with <-cmp x y
+  ... | tri< a ¬b ¬c = x <∷ l Cond a
+  ... | tri≈ ¬a b ¬c = l
+  ... | tri> ¬a ¬b c = l
+
+
+record meta : Set where
+  field
+    deeps : ℕ
+    black-nodes : ℕ
+    l-list : left-List
+    r-list : right-List
+open meta
+
+record tree-meta (A B C D : Set) : Set where
+  field
+    key : A
+    meta-data : B
+    ltree : C
+    rtree : D
+open tree
+
+{-
+
+data rbt-meta : Set where
+  bt-empty : rbt-meta
+  bt-node  : (node : tree-meta (node col ℕ ) meta rbt-meta rbt-meta ) → rbt-meta
+
+test'1 = whileTestPCall' bt-empty 0
+test'2 = whileTestPCall' (rbt_t.Env.vart test'1) 1
+test'3 = whileTestPCall' (rbt_t.Env.vart test'2) 2
+test'4 = whileTestPCall' (rbt_t.Env.vart test'3) 3
+test'5 = whileTestPCall' (rbt_t.Env.vart test'4) 4
+test'6 = whileTestPCall' (rbt_t.Env.vart test'5) 5
+test'7 = whileTestPCall' (rbt_t.Env.vart test'6) 6
+test'8 = whileTestPCall' (rbt_t.Env.vart test'7) 7
+test'9 = whileTestPCall' (rbt_t.Env.vart test'8) 8
+test'10 = whileTestPCall' (rbt_t.Env.vart test'9) 9
+test'11 = whileTestPCall' (rbt_t.Env.vart test'10) 10
+test'12 = whileTestPCall' (rbt_t.Env.vart test'11) 11
+test'13 = whileTestPCall' (rbt_t.Env.vart test'12) 12
+test'14 = whileTestPCall' (rbt_t.Env.vart test'13) 13
+test'15 = whileTestPCall' (rbt_t.Env.vart test'14) 14
+
+testdata = rbt_t.Env.vart test'7
+
+-- ここからmetaの作成
+
+makemeta-comm : rbt_t.rbt → ℕ → meta → rbt-meta
+
+--make meta black nodes
+makemeta-black-nodes :  rbt_t.rbt → ℕ → meta → rbt-meta
+makemeta-black-nodes = {!!}
+
+-- make meta deeps
+set-black-nodes : rbt_t.rbt → meta → ℕ
+set-black-nodes rbt fls with rbt
+... | bt-empty = (suc (black-nodes fls) )
+... | bt-node node with (node.coler (key node))
+... | black = (suc (black-nodes fls) )
+... | red = (black-nodes fls)
+
+--make meta list
+makemeta-comm rbt num fls with rbt
+... | bt-empty = bt-empty
+... | bt-node node = bt-node ( record { key = key node
+  ; meta-data = ( record {deeps = (deeps fls)
+    ; black-nodes = set-black-nodes rbt fls
+    ; l-list = insert-l (node.number (key node)) (l-list fls)
+    ; r-list = insert-r (node.number (key node))  (r-list fls) } )
+  ; ltree = makemeta-comm (ltree node) (node.number (key node)) ( record { deeps = (suc (deeps fls))
+    ; black-nodes = set-black-nodes rbt fls
+    ; l-list = insert-l (node.number (key node)) (l-list fls)
+    ; r-list = (r-list fls) } )
+  ; rtree = makemeta-comm (rtree node) (node.number (key node)) ( record { deeps = (suc (deeps fls))
+    ; black-nodes = set-black-nodes rbt fls
+    ; l-list = (l-list fls)
+    ; r-list = insert-r (node.number (key node)) (r-list fls) } ) })
+
+-- init
+makemeta : rbt → rbt-meta
+makemeta rbt with rbt
+... | bt-empty = bt-empty
+... | bt-node node = bt-node ( record { key = key node
+  ; meta-data =  ( record { deeps = 0 ; black-nodes = 1; l-list = [] ; r-list = [] } )
+  ; ltree = makemeta-comm (ltree node) (node.number (key node))
+    ( record { deeps = 1 ; black-nodes = 1 ; l-list = insert-l (node.number (key node)) [] ; r-list = [] } )
+  ; rtree = makemeta-comm (rtree node) (node.number (key node))
+    ( record { deeps = 1 ; black-nodes = 1 ; l-list = [] ; r-list = insert-r (node.number (key node)) [] } ) })
+
+---test11 = makemeta (rbt_t.Env.vart test'11)
+-}

--- a/paper/src/agda/rbt_t.agda	Sat Feb 13 00:30:44 2021 +0900
+++ b/paper/src/agda/rbt_t.agda	Sun Feb 14 21:23:12 2021 +0900
@@ -38,6 +38,7 @@
     varl : List rbt
 open Env
 
+
 whileTest-next : {l : Level} {t : Set l}  → (c10 : rbt) → (n : ℕ) → (list : List rbt) → (next : Env → t) → (exit : Env → t) → t
 whileTest-next c10 n list next exit = next (record {vart = c10 ; varn = n ; varl = list} )
 
@@ -141,17 +142,28 @@
 merge-tree record { vart = vart ; varn = varn ; varl = (bt-node record { key = record { coler = coler ; number = number } ; ltree = ltree ; rtree = rtree } ∷ varl₁) } next exit | tri< a ¬b ¬c
   = next record { vart = (bt-node record { key = record { coler = coler ; number = number } ; ltree = vart ; rtree = rtree }) ; varn = number ; varl = varl₁ }
 
---修正後
-merge-tree1 :  {le : Level} {t : Set le} → Env → (next : Env → t) → (exit : Env → t) → t
-merge-tree1 env next exit with varl env
+-- do marge-tree
+-- next merge-tree-c
+-- exit fin
+merge-tree-c :  {le : Level} {t : Set le} → Env → (next : Env → t) → (exit : Env → t) → t
+merge-tree-c env next exit with varl env
 ... | [] = exit env
 ... | bt-empty ∷ nl = exit env
-... | bt-node node₁ ∷ nl with <-cmp (varn env) (number ( key node₁ ))
-... | tri≈ ¬a b ¬c = next (record env { varn = number (key node₁) ; varl = nl })
--- next (record{ vart = vart env ; varn = number (key node₁) ; varl = nl })
-... | tri> ¬a ¬b c = next (record env { vart = (bt-node record { key = key node₁ ; ltree = ltree node₁ ; rtree = vart env }) ; varn = number (key node₁) ; varl = nl })
--- next (record{ vart = (bt-node record { key = key node₁ ; ltree = ltree node₁ ; rtree = vart env }) ; varn = number (key node₁) ; varl = nl })
-... | tri< a ¬b ¬c = next (record{ vart = (bt-node record { key = key node₁ ; ltree = vart env ; rtree = rtree node₁ }) ; varn = number (key node₁) ; varl = nl })
+... | bt-node xtree ∷ varl with <-cmp (varn env) (number ( key xtree ))
+... | tri≈ ¬a b ¬c = next (record env { vart = bt-node xtree ; varn = number (key xtree) ; varl = varl })
+... | tri> ¬a ¬b c = next (record env { vart = (bt-node record xtree{rtree = Env.vart env}) ; varn = number (key xtree) ; varl = varl })
+... | tri< a ¬b ¬c = next (record env { vart = (bt-node record xtree{ltree = Env.vart env}) ; varn = number (key xtree) ; varl = varl })
+
+-- do brandh
+-- next insert-c
+-- exit merge-tree
+insert-c : {le : Level} {t : Set le} → Env → (next : Env → t) → (exit : Env → t) → t
+insert-c env next exit with Env.vart env
+... | bt-empty = exit record env{vart = (bt-node (record { key = record { coler = red ; number = Env.varn env }; ltree = bt-empty; rtree = bt-empty }))}
+... | bt-node node with <-cmp (Env.varn env) (node.number (tree.key node))
+... | tri≈ ¬a b ¬c = exit env
+... | tri> ¬a ¬b c = next record env{vart = (tree.ltree node) ; varl = (bt-node record node{ltree = bt-empty}) ∷ (Env.varl env) }
+... | tri< a ¬b ¬c = next record env{vart = (tree.rtree node) ; varl = (bt-node record node{rtree = bt-empty}) ∷ (Env.varl env) }
 
 -- insert
 bt-insert : {le : Level} {t : Set le} → Env → (next : Env → t) → (exit : Env → t) → t
@@ -170,15 +182,11 @@
 bt-insert record {vart = (bt-node record { key = key ; ltree = ltree ; rtree = rtree }) ; varn = varn ; varl = varl } next exit | tri< a ¬b ¬c
   = next (record {vart = rtree ; varn = varn ; varl = (bt-node record { key = key ; ltree = ltree ; rtree = bt-empty }) ∷ varl })
 
-
-
 -- normal loop without termination
 {-# TERMINATING #-}
 insert : {l : Level} {t : Set l} → Env → (exit : Env → t) → t
 insert env exit = bt-insert env (λ env → insert env exit ) exit
 
-
-
 init-col : {l : Level} {t : Set l} → Env → (exit : Env → t) → t
 init-col env exit = init-node-coler env exit exit
 

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/src/agda/rbt_varif.agda	Sun Feb 14 21:23:12 2021 +0900
@@ -0,0 +1,52 @@
+module rbt_varif where
+open import Level renaming ( suc to succ ; zero to Zero )
+open import Relation.Binary
+open import Data.Nat hiding (_≤_  ; _≤?_)
+open import Data.List hiding ([_])
+open import Data.Product
+open import Data.Nat.Properties as NP
+
+mutual
+  data  right-List : Set where
+    [] : right-List
+    [_] : ℕ → right-List
+    _∷>_Cond_ : (x : ℕ) → (xs : right-List ) → (p : x Data.Nat.> top-r xs) → right-List
+
+  top-r : right-List → ℕ
+  top-r [] = {!!}
+  top-r [ x ] = x
+  top-r (x ∷> l Cond x₁) = x
+
+  insert-r : ℕ → right-List → right-List
+  insert-r x [] = {!!}
+  insert-r x [ y ] with <-cmp x y
+  ... | tri< a ¬b ¬c = [ y ]
+  ... | tri≈ ¬a b ¬c = [ y ]
+  ... | tri> ¬a ¬b c = x ∷>  [ y ] Cond c
+  insert-r x (y ∷> ys Cond p) with <-cmp x y
+  ... | tri< a ¬b ¬c = (y ∷> ys Cond p)
+  ... | tri≈ ¬a b ¬c = (y ∷> ys Cond p)
+  ... | tri> ¬a ¬b c = x ∷> (y ∷> ys Cond p) Cond c
+  
+
+  data  left-List : Set where
+    [] : left-List
+    [_] : ℕ -> left-List
+    _<∷_Cond_ : (x : ℕ) -> (xs : left-List ) -> (p : x Data.Nat.< top-l xs) -> left-List
+
+  top-l : left-List → ℕ
+  top-l [] = {!!}
+  top-l [ x ] = x
+  top-l (x <∷ l Cond x₁) = x
+
+  insert-l : ℕ -> left-List -> left-List
+  insert-l x [] = [ x ]
+  insert-l x l@([ y ]) with <-cmp x y
+  ... | tri< a ¬b ¬c = x <∷ l Cond a
+  ... | tri≈ ¬a b ¬c = l
+  ... | tri> ¬a ¬b c = l
+  insert-l x l@(y <∷ ys Cond p) with <-cmp x y
+  ... | tri< a ¬b ¬c = x <∷ l Cond a
+  ... | tri≈ ¬a b ¬c = l
+
+  ... | tri> ¬a ¬b c = l

--- a/paper/tex/rbt_imple.tex	Sat Feb 13 00:30:44 2021 +0900
+++ b/paper/tex/rbt_imple.tex	Sun Feb 14 21:23:12 2021 +0900
@@ -1,14 +1,120 @@
 \chapter{Red Black Tree の実装}
 
-\section{Agda による Red Black Tree の 実装}
-通常は再起処理を使用して Red Black Tree を行う。
-しかし、今回はCbCで実装された Red Black Tree を検証するので、
-下図の手順を元に実装を行う。
+Left Learning Red Blacl Tree の実装において、
+通常の言語であれば再起処理を用いて実装を行える部分を
+継続にて実行可能なように変更する必要がある。
+本節では、この課題に対して Gears Agda での
+Left Learning Red Black Tree の実装方法について述べる。
+
+\section{Gears Agda での Red Black Tree の 記述}
+Gears Agda にて Red Black Tree を実装する際の手順を、
+下\figref{rbt_imple}を参考に説明する。
+
+\begin{figure}[H]
+  \begin{center}
+    \includegraphics[height=7.5cm]{pic/imple/実装.pdf}
+  \end{center}
+  \caption{再起処理を回避する手順}
+  \label{rbt_imple}
+\end{figure}
+
+41の値を Left Leaning Red Black Tree に insert もしくは delete する際の手順を説
+明する。
+まず Root node である 59 と比較した際に、41はそれより小さい。
+この際、left node に遷移するが、CbC では再起処理が行えないため、listに保持していく。
+順々に辿っていき、対象の場所に到達すると insert / delete を行う。
+その後はlistからnodeを取り出し、結合することで Left Leaning Red Black Tree の操作を行う。
+
+\subsection{定義した Data Gear の記述}
+
+Left Learning Red Black Tree の記述の際に、 Code Gear
+に渡している Data Gear である Env の記述を \coderef{env_imple} に示す。
+
+\lstinputlisting[label=env_imple, caption=insertにて目的の nodeまで辿るプログラム, firstline=13, lastline=39] {src/agda/rbt_t.agda}
+
+箇条書きにてそれぞれについて解説を行う。
+
+\begin{description}
+\item[col] 色のことで、red と black の data 型で記述し、パターンマッチを行えるようにした
+\item[node] その名の通り node に格納されている値を保存する。 色と値となる自然数が入る
+\item[tree] tree の構造 を保存する。ここで node と x / right tree を持つ
+\item[rbt] 上3つの要素を合わせて持つことで Left Learning Red Black Tree を定義する
+\item[Env] rbt 以外に追加や削除を行う対象となる値と、 rbtを保存できる List を持つ Data Gear
+\end{description}
+
+\subsection{目的の node まで辿る Gears Agda}
+上記に示した手順通りにAgdaで記述すると下 \coderef{insert_imple}のようになる。
+例は insert を行う場合の記述となる。
+
+\lstinputlisting[label=insert_imple, caption=insertにて目的の nodeまで辿るプログラム, firstline=157, lastline=166] {src/agda/rbt_t.agda}
+
+ソースコードの解説をする。上から3行はコメントで、この関数で行っていることを doに、
+next / exit では4章で述べた次の関数遷移先を記載している。
+
+5行目にて withを使用することで vart のパターンマッチを行っている。
+vart が bt-empty である場合に 6行目が動作する。
+bt-empty であれば node の一番下であるため、
+varn を tree の値として insert して exit に遷移する。
 
-上記に示した手順通りにAgdaで記述すると以下のようなソースコードになる。
+7行目は vart が bt-empty ではないパターンの動作を記述している。
+ここでは insertを行う値である varn と 現在いる位置の tree の値と比較を行い、
+再度パターンマッチを行う。
+
+8行目は比較した結果、同値だった場合であり、そのままexitに遷移している。
+
+9行目は入力の値 varn の方が小さい場合を指している。
+vart に left tree を入れ、varl には 現在の tree から left treeを除いた
+treeを追加している。それを next に遷移させている。
+
+10行目は入力の値 varn の方が大きい場合を指している。
+9行目とは逆に、vart に right tree を入れ、varl には 現在の tree から right treeを除いた
+treeを追加している。それをまたnext に遷移させている。
+
+以上の手順により、目的の node まで辿っている。
+
+\subsection{目的の node まで辿った後の Gears Agda}
+目的の node にたどり着いた後、List に格納された tree と vart の結合を行う。
+Gears Agda でそれを記述すると\coderef{mearge_imple}のようになる。
+
+\lstinputlisting[label=mearge_imple, caption=insertにて目的の nodeまで辿るプログラム, firstline=145, lastline=155] {src/agda/rbt_t.agda}
+ソースコードの解説をする。
+5行目にて with を使用して varl についてパターンマッチを行っている。
+
+6行目が varl に何も入っていない場合で、実行終了のため exitに遷移している。
+
+7行目は varl に何か入っていた場合で、ここでは varl に入っているものが
+何であるのか8行目と合わせてパターンマッチを行っている。
+ここでは varl に入っていたものが bt-empty であった場合について記述されている。
+bt-emptyが入ってくることは実装上ありえないので、exitに遷移することで強制終了している。
+
+8行目では varl に入っていたものが bt-empty ではなかった場合で、
+それをxtreeと命名している。
+ここで vart に入っている値と xtree に入っている値を比較を行い、
+さらにパターンマッチを行う。
+
+9行目が入っている値と同じ値であった場合で、
+特に操作する必要がないので vart に xtree を入れ、
+varl を一つ進める。
+
+10行目は vartが大きい場合で、
+varnに xtree の値を入れ、
+xtree の right tree に
+現在のvart を入れたものを vartにして
+varlを一つ進めている。
+
+11行目は vartが小さい場合で、
+10行目と逆のことをしている。
+varnに xtree の値を入れ、
+xtree の left tree に
+現在のvart を入れたものを vartにして
+varlを一つ進めている。
+
+以上の組み合わせを行い、
+Gears Agda にて 再起処理を使わず
+に Left Learning Red Black Tree の insert / delete を
+記述した。
 
 
-以上のように Tree の基本操作である insert, find, delete の実装を行った。
+% 以上のように Tree の基本操作である insert, find, delete の実装を行った。
 
 
-

--- a/paper/tex/rbt_verif.tex	Sat Feb 13 00:30:44 2021 +0900
+++ b/paper/tex/rbt_verif.tex	Sun Feb 14 21:23:12 2021 +0900
@@ -1,11 +1,60 @@
 \chapter{Red Black Tree の検証}
+実装が困難であったため、検証するまでには至らなかった。
+
+\section{Meta Data Gearの記述}
+検証するにあたり、Meta Deta Gear を作成し Pre / Post Condition と
+比較することで Hoare Triple に当てはめることは第5章で前述した。
+\subsection{大小関係を検証する Meta Data Gear}
+Red Black Tree は Binary Search Tree の 定義を持っているので、
+parent から見て left node には parent の値より小さい値が、
+right node には大きい値が入る。これを検証する必要がある。
+
+大小関係を検証するにあたり、Fresh List を用いた検証手法が考えられた。
+Fresh Listの記述を以下に示す。
+% ソースコードを載せる。
+
+Fresh Listは一つの値に対して、それより後の値との大小関係の証明が入っている。
+そのため、正確性が増すが、Fresh List への insert が困難であったため、
+証明付き Data 構造を持った List を \coderef{list_v}
+のように定義した。
 
-Input Data Gear が Pre Condition を、 Output Data Gearが Post Condition を 満たしているか検証することで Hoare Logic に当てはめる。
+\lstinputlisting[label=list_v, caption=証明付き Data 構造を持った List,firstline=9,lastline=30] {src/agda/rbt_varif.agda}
+証明付き Data 構造を持った List の定義は right-List で行っている。
+List の Top と比較した際に、
+Topの値より大きい値でなければ insert できない。
+加えて insert できた値が Top より大きい事を示す証明も持つ事ができる。
 
-以下の要素を検証するための Meta Code Gear を実装する。
+mutual は 以下の記述全てに対して掛かっている。
+これは right-List の定義の中で、top-r　を呼び出しており、
+top-r は定義の部分で right-List を使用している。
+したがって相互呼び出しとなっている。
+Agdaは 逐次処理であるため、プログラムの上に宣言してある関数や型しか使用できない。
+mutual を掛けることで、プログラムの下で宣言している関数や型を使用する事ができる。
+
+right-List の定義は、何も入っていない場合は right-List で停止するようにしている。
+List に一つしか値が入っていない場合は、証明付き Data 構造を持つ必要がない。
+そのため特記して記述している。
+List に他の値が入っている場合は、top とその次の値との比較を証明を持っている。
+
+top-r は Listに入っている Top の値を持ってくる関数を記述している。
+insert-r は right-List に 値を insert するための関数で、
+right-List の top と入れる引数を比較し、
+inserする際は値とその証明の両方を持つ事で 証明付き Data 構造を
+持った List となっている。
 
 
-そして、 Meta Code Gear から 生成される Meta Data Gear が Pre / Post Conditionを
-満たしているのか確認することで、関数一つ一つに対して Hoare Logic を用いた検証を行う
-%
+
+
+以上を用いて Meta Data Gear を作成する Gears Agda は以下になる。
+
+
+これを用いることで、各 node より上の node の大小関係を検証できると考えた。
 
+%\subsection{Black node の数え上げ}
+%他にも、Left Learning Red Brack Tree の black node の数え上げを記述した。
+
+%\subsection{Meta Data Gear の作成}
+
+
+
+