# HG changeset patch
# User soto <soto@cr.ie.u-ryukyu.ac.jp>
# Date 1641455873 -32400
# Node ID 8a97e69f861502f83a45d1e95fa8cce843799387
# Parent  60d4617eac8468b023af095daea08b4bd5fb37d3
いったんスライドは完成

diff -r 60d4617eac84 -r 8a97e69f8615 MindMap/sample.km
--- a/MindMap/sample.km	Thu Jan 06 13:59:12 2022 +0900
+++ b/MindMap/sample.km	Thu Jan 06 16:57:53 2022 +0900
@@ -724,7 +724,7 @@
                     "id": "cgxlvb49n1c0",
                     "created": 1641372156518,
                     "text": "目標",
-                    "expandState": "collapse",
+                    "expandState": "expand",
                     "font-family": "arial,helvetica,sans-serif",
                     "font-size": 48,
                     "layout": null
@@ -747,7 +747,7 @@
                     "id": "cgxm64t605k0",
                     "created": 1641373004791,
                     "text": "発表の目次",
-                    "expandState": "collapse",
+                    "expandState": "expand",
                     "layout": null,
                     "font-family": "arial,helvetica,sans-serif",
                     "font-size": 48
@@ -759,7 +759,8 @@
                             "created": 1641373104149,
                             "text": "CbCとGears Agda",
                             "layout": null,
-                            "font-size": 48
+                            "font-size": 48,
+                            "progress": 9
                         },
                         "children": []
                     },
@@ -769,7 +770,8 @@
                             "created": 1641373136530,
                             "text": "Meta level と normal level",
                             "layout": null,
-                            "font-size": 48
+                            "font-size": 48,
+                            "progress": 9
                         },
                         "children": []
                     },
@@ -789,7 +791,8 @@
                             "created": 1641373193809,
                             "text": "While Program",
                             "layout": null,
-                            "font-size": 48
+                            "font-size": 48,
+                            "progress": 9
                         },
                         "children": [
                             {
@@ -934,7 +937,8 @@
                             "text": "将来",
                             "layout": null,
                             "font-family": "arial,helvetica,sans-serif",
-                            "font-size": 48
+                            "font-size": 48,
+                            "progress": 9
                         },
                         "children": [
                             {
diff -r 60d4617eac84 -r 8a97e69f8615 slide/slide.md
--- a/slide/slide.md	Thu Jan 06 13:59:12 2022 +0900
+++ b/slide/slide.md	Thu Jan 06 16:57:53 2022 +0900
@@ -74,13 +74,15 @@
 
 
 # Agda の基本 
-- Agdaとは定理証明支援器であり、関数型言語である
-- Agdaでの関数は、最初に型について定義した後に、関数を定義する事で記述できる
+- Agdaとは定理証明支援器であり、関数型言語
+- Agdaでの関数は、最初に型について定義した後に、関数を定義する事で記述する
     - これが Curry-Howard 対応となる
 - 型の定義部分で、入力と出力の型を定義できる
   -  input → output のようになる
 - 関数の定義は = を用いて行う
   - 関数名の後、 = の前で受け取る引数を記述します
+
+<!--
 ```
 sample1 : (A : Set ) → Set
 sample1 a = a
@@ -88,11 +90,10 @@
 sample2 : (A : Set ) → (B : Set ) → Set
 sample2 a b = b
 ```
-
+-->
 
 # Agda の基本 record
-- 2つのものが同時に存在すること
-- Record 型とはオブジェクトあるいは構造体
+オブジェクトあるいは構造体
 ```
 record Env  : Set where
   field
@@ -123,7 +124,7 @@
 whileLoop env next | false = next env
 whileLoop env next | true = whileLoop (record {varn = (varn env) - 1 ; vari = (vari env) + 1}) next
 ```
-- t を返すで継続を表す(tは呼び出し時に任意に指定してもよい. testに使える)
+- t を返すことで継続を表す(tは呼び出し時に任意に指定してもよい. testに使える)
 - tail call により light weight continuation を定義している
 
 
@@ -218,7 +219,7 @@
     TerminatingLoopS Env (λ env → varn env)(λ n2 p2 loop → whileLoopSeg {_} {_} {c10} n2 p2 loop 
     (λ ne pe → whileTestSpec1 c10 ne pe)) n1 p1 )) 
 ```
-- conversion1は
+- conversion1はPre Condition をPost Conditionに変換する
 - whileLoopSeg
 - ⊤
 
@@ -230,29 +231,25 @@
 
 
 # Gears Agda による BinaryTree の実装 
-- Agdaが変数への再代入を許していないためそのままでは木構造を実装できない
-  - 木構造を辿る際に現在いるノード以下の木構造をそのまま stack に格納する
-  - replace / delete などの操作を行った後に stack を参照し Tree を再構築する
-  - CbCへの変換の時に問題になりそうな予感
-- ここの説明いらないかも？
+CbCと並行した実装をするため、Stackを明示した実装をする
 
-
-# Gears Agda による BinaryTree の実装 find node
 ```
-find : {n m : Level} {A : Set n} {t : Set m} → (env : Env A )
-  → (next : (env : Env A ) → t ) → (exit : (env : Env A ) → t ) → t
+find : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree : bt A ) → List (bt A)
+  → (next : bt A → List (bt A) → t ) → (exit : bt A → List (bt A) → t ) → t
 find key leaf st _ exit = exit leaf st
 find key (node key₁ v1 tree tree₁) st next exit with <-cmp key key₁
 find key n st _ exit | tri≈ ¬a b ¬c = exit n st
 find key n@(node key₁ v1 tree tree₁) st next _ | tri< a ¬b ¬c = next tree (n ∷ st)
 find key n@(node key₁ v1 tree tree₁) st next _ | tri> ¬a ¬b c = next tree₁ (n ∷ st)
 ```
+置き換えるnodeまでTreeを辿り、Stackに逆順にTreeを積んでいく
 
 <!--
 findは全部書いても大丈夫そう
 -->
 
 # Gears Agda による BinaryTree の実装 replace node
+置き換えたnodeをStackを解消しながらTreeを再構成する
 ```
 replace : {n m : Level} {A : Set n} {t : Set m} 
   → (key : N) → (value : A) → bt A → List (bt A) 
@@ -276,21 +273,19 @@
 これは途中省略してよさそう
 -->
 
+# Binary Tree の3種類の Invariant
+Tree Invariant
+- Binary Tree が Key の順序に沿って構成されていることを表すData構造
 
-# Gears Agda による BinaryTree の実装 loop connecter
-```
-
-```
+Stack Invariant
+- Stackが木の昇順に構成されていることを表す
 
-# Gears Agda による Binary Tree の検証 Invariant
-具体的な例を一つ挙げて、Invariantの説明を行う
-- Binary Tree の性質である、左の子のkeyは親より小さく、
-右の子のkeyは親より大きいことを検証
-- Stack に格納されているTreeはその次のStackの減少列になっているか
-- Tree を正しく入れ替えられているか
+Replace Tree
+- 2つの木の1つのnodeが入れ替わっていることを示す
 
-# Gears Agda による Binary Tree の検証 Invariant
-- Tree Invariant
+# Tree Invariant
+- Invariant というよりも可能な Binary Tree 全体の集合を表す型
+- 制約付きのBinary Tree
 ```
 data treeInvariant {n : Level} {A : Set n} : (tree : bt A) → Set n where
     t-leaf : treeInvariant leaf 
@@ -309,6 +304,9 @@
 ```
 
 <!--
+t-leaf はコンストラクタ
+
+
 コードの解説
 省略した方がたぶん絶対良い
 right と left なんかはほとんど対照的なので省略とかでよさそう
@@ -316,8 +314,11 @@
 -->
 
 
-# Gears Agda による Binary Tree の検証 Invariant
-- Stack Invariant
+# Stack Invariant
+- StackにはTreeを辿った履歴が残っている
+- 辿り方はKeyの値に依存する
+- 実際のStackよりも豊富な情報を持っている<!--Keyの比較が入っているから-->
+
 ```
 data stackInvariant {n : Level} {A : Set n} (key : N) : (top orig : bt A) 
   → (stack : List (bt A)) → Set n where
@@ -330,8 +331,8 @@
       → stackInvariant key tree₁ tree0 (tree₁ ∷ st)
 ```
 
-# Gears Agda による Binary Tree の検証 Invariant
-- Replace Invariant
+# Replace Tree
+- 木の特定のnodeが正しく置き換えられているか
 ```
 data replacedTree {n : Level} {A : Set n} (key : N) (value : A) : (before after : bt A) → Set n where
     r-leaf : replacedTree key value leaf (node key value leaf leaf)
@@ -345,20 +346,108 @@
           → replacedTree key value (node k v1 t1 t2) (node k v1 t t2) 
 ```
 
-# Gears Agda による Binary Tree の検証
-Binary Tree の実装に対して上述した3つのInvariantを
-Meta Data Gear として渡しながら実行できるように記述する
+# find の Hoare Condition
+findPでは treeInvariant をつかって stackInvariant を生成する
+停止性を証明する木の深さの不等式も証明する
+```
+findP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree tree0 : bt A ) → (stack : List (bt A))
+           →  treeInvariant tree ∧ stackInvariant key tree tree0 stack  
+           → (next : (tree1 : bt A) → (stack : List (bt A)) 
+              → treeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack 
+                → bt-depth tree1 < bt-depth tree   → t )
+           → (exit : (tree1 : bt A) → (stack : List (bt A)) 
+              → treeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack
+                → (tree1 ≡ leaf ) ∨ ( node-key tree1 ≡ just key )  → t ) → t
+```
+
+# Hoare Condition の拡張
+testなどでは仮定が入ることがある
+Hoare Conditionを拡張可能な部分があるrecordで定義する
+Cが拡張される部分で, これはDataの継続に相当する
+Code Gear に継続があるように Data Gearにも継続がある
 ```
-findP : {n m : Level} {A : Set n} {t : Set m} → (env : Env A)
-  → treeInvariant env ∧ stackInvariant env
-  → (exit : (env : Env A) → treeInvariant env ∧ stackInvariant env → t ) → t
+record findPR {n : Level} {A : Set n} (key : ℕ) (tree : bt A ) (stack : List (bt A)) 
+  (C : ℕ → bt A → List (bt A) → Set n) : Set n where
+   field
+     tree0 : bt A
+     ti0 : treeInvariant tree0
+     ti : treeInvariant tree
+     si : stackInvariant key tree tree0 stack
+     ci : C key tree stack     -- data continuation
+```
+
+# 拡張部分の記述と推論
+拡張部分はrecord findPC で定義する
+拡張部分の推論はrecord findExt で定義する
+```
+record findPC {n : Level} {A : Set n} (value : A) (key1 : ℕ) (tree : bt A ) (stack : List (bt A)) : Set n where
+   field
+     tree1 : bt A
+     ci : replacedTree key1 value tree1 tree
+   
+record findExt {n : Level} {A : Set n} (key : ℕ) (C : ℕ → bt A → List (bt A) → Set n) : Set (Level.suc n) where
+   field
+      c1 : {key₁ : ℕ} {tree tree₁ : bt A } {st : List (bt A)} {v1 : A}
+        → findPR key (node key₁ v1 tree tree₁) st C → key < key₁  → C key tree (tree ∷ st)
+      c2 : {key₁ : ℕ} {tree tree₁ : bt A } {st : List (bt A)} {v1 : A}
+        → findPR key (node key₁ v1 tree tree₁) st C → key > key₁  → C key tree₁ (tree₁ ∷ st)
 ```
 
+# replade Node の Invariant
+repraceTree は置き換えるべきnodeが実行時に決まるので関数を挟んだInvariantになる
+```
+child-replaced :  {n : Level} {A : Set n} (key : ℕ)   (tree : bt A) → bt A
+child-replaced key leaf = leaf
+child-replaced key (node key₁ value left right) with <-cmp key key₁
+... | tri< a ¬b ¬c = left
+... | tri≈ ¬a b ¬c = node key₁ value left right
+... | tri> ¬a ¬b c = right
+
+record replacePR {n : Level} {A : Set n} (key : ℕ) (value : A) (tree repl : bt A ) 
+  (stack : List (bt A)) (C : bt A → bt A → List (bt A) → Set n) : Set n where
+   field
+     tree0 : bt A
+     ti : treeInvariant tree0
+     si : stackInvariant key tree tree0 stack
+     ri : replacedTree key value (child-replaced key tree ) repl
+     ci : C tree repl stack     -- data continuation
+```
+
+# 最終的な証明コード
+insertしたkeyをfindすると元の値が取れてくることを証明する
+insertTreeSpec0が仕様
+conteinsTreeがtestコードかつ証明になっている
+証明の詳細はコードのHoara condition の証明に入っている
+```
+insertTreeSpec0 : {n : Level} {A : Set n} → (tree : bt A) → (value : A) 
+  → top-value tree ≡ just value → ⊤
+insertTreeSpec0 _ _ _ = tt
+
+containsTree : {n : Level} {A : Set n} → (tree tree1 : bt A) → (key : ℕ) → (value : A) 
+  → treeInvariant tree1 → replacedTree key value tree1 tree  → ⊤
+containsTree {n}  {A}  tree tree1 key value P RT =
+   TerminatingLoopS (bt A ∧ List (bt A) )
+     {λ p → findPR key (proj1 p) (proj2 p) (findPC value ) } (λ p → bt-depth (proj1 p)) 
+              ⟪ tree , tree ∷ []  ⟫ ?
+       $ λ p P loop → findPPC1 key value (proj1 p) (proj2 p) P (λ t s P1 lt → loop ⟪ t , s ⟫ P1 lt )  
+       $ λ t1 s1 P2 found? → insertTreeSpec0 t1 value (lemma6 t1 s1 found? P2) 
+```
+
+# replace Tree の性質
+Replace Tree 自体は Tree に特定の値が入っていることを示すData構造になっている
+これをHoare条件として持ち歩くことにより、Binary Treeの詳細に立ち入らず何が入っているかを指定できる
+
+これにより木を用いるプログラムでの証明を記述できる
+insert Tree や Find Node の停止性も証明されている
 
 # 今後の研究方針
-- 現在は Binary Tree の検証までしか行えていないが、
-今回定義した条件はそのまま Red Black Tree の検証に使用できるはず
-- 今後は Gears Agda による実装と条件の追加をおこなう
+- Deleteの実装
+- Red Black Tree の実装
+  - 今回定義した条件はそのまま Red Black Tree の検証に使用できるはず
+- Contextを用いた並列実行時のプログラムの正しさの証明
+  - syncronized queue
+  - concarent tree
+- xv.6への適用
 - モデル検査
 
 # まとめ
@@ -368,7 +457,4 @@
   - 今後は Red Black Tree の検証をすすめる
 - モデル検査をしたい
 
-英語版も欲しい
-
-condition を テンプレみたいに作ってかきやすくする話
-
+<!-- 英語版も欲しい-->