GearsAgda によるRed Black Treeの検証

ほぼできた

削除は複雑だが、対称にできると良い。削除するノードをleafになるように変形する

replace invariant を再利用できる?

削除は右の木の一番左を削除したと考えられる

hoareBinaryTree をできるだけ simple にする

(replacedTree を削れない?)

全面書き換えの時間はないが、redBlackTreeのinvariant を付け加える

binaryTreeのinvariantをredBlackTreeに付加する

invarinant までは書けた

replace のinvariant を持ち歩く感じか

だとすると、そのrotation をく必要がある。

replaceInariant がやっかいだが

ttee invarinat なら左右のノードのappend にすべての要素がある

key が等しい時は左右は等しいなら

真ん中のところだけが入れ替わる

keyが等しくない時は、違うところ以外は一致する

GearsAgdaなので loop でかく

find

replace

それぞれに、loop connector がある

TreeとStackがあるが、それぞれにinvariant がある

Treeと TreeInvariantを別にしているが、それはむだ

一つにする

データ構造の部分と、メタの制約部分を分離して書きたい

これはあまり良くないらしい

RedBlack Tree は

Red / Black のflag

深さの制約

を TreeInvariant に付け加えれば良い

Termination は TerminatingLoopS でやってる。これは、for文みたいなもの。

fmap (Functor)でもいいのだが、insert とかはFunctorではない