# HG changeset patch # User soto # Date 1641484687 -32400 # Node ID 62e56d73f104cc6e598631c3af2ca2d0fa3767b7 # Parent 8a97e69f861502f83a45d1e95fa8cce843799387 WIP カンペを追加 14ページまで diff -r 8a97e69f8615 -r 62e56d73f104 MindMap/slide.html --- a/MindMap/slide.html Thu Jan 06 16:57:53 2022 +0900 +++ b/MindMap/slide.html Fri Jan 07 00:58:07 2022 +0900 @@ -48,7 +48,7 @@ top: 300px; text-align: center; } -" data-heading-divider="1" class="title" data-marpit-pagination="1" data-marpit-pagination-total="24" style="--paginate:true;--class:title;--theme:default;--style:section { +" data-heading-divider="1" class="title" data-marpit-pagination="1" data-marpit-pagination-total="28" style="--paginate:true;--class:title;--theme:default;--style:section { background-color: #FFFFFF; font-size: 28px; color: #4b4b4b; @@ -131,7 +131,7 @@ top: 300px; text-align: center; } -" data-heading-divider="1" class="slide" data-marpit-pagination="2" data-marpit-pagination-total="24" style="--paginate:true;--class:slide;--theme:default;--style:section { +" data-heading-divider="1" class="slide" data-marpit-pagination="2" data-marpit-pagination-total="28" style="--paginate:true;--class:slide;--theme:default;--style:section { background-color: #FFFFFF; font-size: 28px; color: #4b4b4b; @@ -227,7 +227,7 @@ top: 300px; text-align: center; } -" data-heading-divider="1" class="slide" data-marpit-pagination="3" data-marpit-pagination-total="24" style="--paginate:true;--class:slide;--theme:default;--style:section { +" data-heading-divider="1" class="slide" data-marpit-pagination="3" data-marpit-pagination-total="28" style="--paginate:true;--class:slide;--theme:default;--style:section { background-color: #FFFFFF; font-size: 28px; color: #4b4b4b; @@ -318,7 +318,7 @@ top: 300px; text-align: center; } -" data-heading-divider="1" class="slide" data-marpit-pagination="4" data-marpit-pagination-total="24" style="--paginate:true;--class:slide;--theme:default;--style:section { +" data-heading-divider="1" class="slide" data-marpit-pagination="4" data-marpit-pagination-total="28" style="--paginate:true;--class:slide;--theme:default;--style:section { background-color: #FFFFFF; font-size: 28px; color: #4b4b4b; @@ -360,12 +360,8 @@ ;--heading-divider:1;" data-size="16:9">

Agda の基本

-
sample1 : (A : Set ) → Set
-sample1 a = a
-
-sample2 : (A : Set ) → (B : Set ) → Set
-sample2 a b = b
-

Agda の基本 record

-
    -
  • 2つのものが同時に存在すること
    • -
  • Record 型とはオブジェクトあるいは構造体
    • -
+

オブジェクトあるいは構造体

record Env  : Set where
   field
     varn : N
@@ -520,202 +507,7 @@
    top: 300px;
    text-align: center;
 }
-" data-heading-divider="1" class="slide" data-marpit-pagination="6" data-marpit-pagination-total="24" style="--paginate:true;--class:slide;--theme:default;--style:section {
-  background-color: #FFFFFF;
-  font-size: 28px;
-  color: #4b4b4b;
-  font-family: "Droid Sans Mono", "Hiragino Maru Gothic ProN";
-  background-image: url("logo.svg");
-  background-position: right 3% bottom 2%;
-  background-repeat: no-repeat;
-  background-attachment: 5%;
-  background-size: 20% auto;
-}
-
-  section.title h1 {
-    color: #808db5;
-    text-align: center;
-    }
-  
-  section.title p {
-      bottom: 25%;
-      width: 100%;
-      position: absolute;
-      font-size: 25px;
-      color: #4b4b4b;
-      background: linear-gradient(transparent 90%, #ffcc00 0%);
-  }
-
-section.slide h1 {
-    width: 95%;
-    color: white;
-    background-color: #808db5;
-    position: absolute;
-    left: 50px; 
-    top: 35px;
-}
-
-section.fig_cg p {
-   top: 300px;
-   text-align: center;
-}
-;--heading-divider:1;" data-size="16:9">
-
Agda の基本 data

-
    
-
  • 一つでも存在すること
    • 
-
  • どちらかが成り立つ型を Data 型 で書く
    • 
-

-
data bt {n : Level} (A : Set n) : Set n where
-  leaf : bt A
-  node : (key : N) → (value : A) → (left : bt A ) → (right : bt A ) → bt A
-

-
記述する際の基本的な例を以下に挙げる

-
datasample : bt → N
-datasample leaf = zero
-datasample (node key value left right) = suc zero
-

-
-

-
Agda の基本 短縮記法

-
    
-
  • with を使用することでその変数のパターンマッチすることもできる
    • 
-

-
patternmatch-default : Env → N
-patternmatch-default record { varn = zero ; vari = i } = i
-patternmatch-default record { varn = suc n ; vari = i } = patternmatch-default record { varn = n ; vari = suc i }
-

-
patternmatch-extraction : env → N
-patternmatch-extraction env with varn env
-patternmatch-extraction zero = vari env
-patternmatch-extraction suc n = patternmatch-extraction record { varn = n ; vari = suc (vari env) }
-

-
    
-
  • ... | `を使用することで関数の定義部分を省略できる
    • 
-

-
patternmatch-extraction' : env → N
-patternmatch-extraction' env with varn env
-... | zero = vari env
-... | suc n = patternmatch-default' record { varn = n ; vari = suc (vari env) }
-

-

-

 
Gears Agda の記法

-
    
-
  • Agda では関数の再帰呼び出しが可能であるが、CbC で再起処理を実装しても値は帰って来ない
-
      
-
    • Agda で実装を行う際には再帰呼び出しを行わないようにする。
      • 
-
    
-
    • 
-

-
plus-com : {l : Level} {t : Set l} → Env → (next : Env → t) → (exit : Env → t) → t
-plus-com env next exit with vary env
-... | zero = exit (record { varx = varx env ; vary = vary env })
-... | suc y = next (record { varx = suc (varx env) ; vary = y })
+
Gears Agda では CbC と対応させるためにすべてLoopで記述する

+loopは→ tの形式で表現する

+再帰呼び出しは使わない(構文的には禁止していないので注意が必要)

+
{-# TERMINATING #-}
+whileLoop : {l : Level} {t : Set l} → Env → (Code : Env → t) → t
+whileLoop env next with lt 0 (varn env)
+whileLoop env next | false = next env
+whileLoop env next | true = whileLoop (record {varn = (varn env) - 1 ; vari = (vari env) + 1}) next
 

 
    
-
  • → t で Set に遷移させるようにし、この後に関数が続くことと、関数を tail call していることで Continuation を定義している
    • 
+
  • t を返すことで継続を表す(tは呼び出し時に任意に指定してもよい. testに使える)
    • 
+
  • tail call により light weight continuation を定義している
    • 
 

 
-

-
Gears Agda と Gears CbC の対応 x

+
Gears Agda と Gears CbC の対応

+
Gears Agda

+
    
+
  • 証明向きの記述
    • 
+
  • Hoare Condition を含む
    • 
+

+
Gears CbC

 
    
-
  • 
-
    証明のしやすいGears Agda で実装を行いながらContext単位で同時に検証も行う
    
-
    • 
-
  • 
-
    Gears Agda は検証向きの実装となり、CbCでは高速な実行向きとなる
    
-
    • 
-
  • 
-
    Gears Agda での検証がCbCによる高速な実行の信頼性となる
    
-
    • 
+
  • 実行向きの記述
    • 
+
  • メモリ管理, 並列実行を含む
    • 
+

+
Context

+
    
+
  • processに相当する
    • 
+
  • Code Gear 単位で並列実行
    • 
 

 

-

 
Normal level と Meta Level を用いた信頼性の向上

-
    
-
  • CbCのプログラムの実行部分は以下の2つから構成される
    • 
-
  • Normal Level は軽量継続で関数型プログラミングとなる
-
      
-
    • ポインタの操作はここでは行わず Meta Level にて行う
      • 
-
    
-
    • 
-
  • Meta Level では信頼性を保証するために必要な計算を行う
+
    Normal Level
    
 
      
-
    • メモリやCPUなどの資源管理
      • 
-
    • context
      • 
-
    • 証明
      • 
-
    • 並列実行（他のプロセスとの干渉）
      • 
-
    • monad
      • 
+
    • 軽量継続
      • 
+
    • Code Gear 単位で関数型プログラミングとなる
      • 
+
    • atomic(Code Gear 自体の実行は割り込まれない)
      • 
+
    • ポインタの操作は含まれない
      • 
 
    
-
    • 
+
    Meta Level
    
+
      
+
    • メモリやCPUなどの資源管理, ポインタ操作
      • 
+
    • Hoare Condition と証明
      • 
+
    • Contextによる並列実行
      • 
+
    • monadに相当するData構造
      • 
 
    
-
-
    
 

-

+

+
+

+

+

+
Gears Agda の Pre Condition Post Condition

+
whileLoopSeg : {l : Level} {t : Set l} → {c10 :  N } → (env : Env) → (varn env + vari env ≡ c10)
+   → (next : (e1 : Env )→ varn e1 + vari e1 ≡ c10 → varn e1 < varn env → t) 
+   → (exit : (e1 : Env )→ vari e1 ≡ c10 → t) → t
+

+
    
+
  • Terminatingを避けるためにloopを分割
    • 
+
  • varn env + vari env ≡ c10 が Pre Condition
    • 
+
  • varn e1 + vari e1 ≡ c10 が Post Condition
    • 
+
  • varn e1 < varn env → t が停止を保証する減少列
    • 
+

+
これは命題なので証明を与えてPre ConditionからPost Conditionを導出する必要がある

+証明は値として次のCodeGearに渡される

+

 

-
Gears Agda による検証の例（検証付き実装）

-
    
-
  • 先ほど実装した while program に対して証明を付ける
    • 
-
  • loop を接続する Meta Gear も用意する
    • 
-

+
Loop の接続

+
分割したloopを接続するMeta Code Gearを作成する

 
TerminatingLoopS : {l : Level} {t : Set l} ( Index : Set ) 
   → {Invraiant : Index → Set } → ( reduce : Index → N) 
   → (loop : (r : Index) → Invraiant r 
@@ -1153,14 +1115,12 @@
   → (r : Index) → (p : Invraiant r) → t
 

 
    
-
  • 入力として仕様の証明を受け取る
    • 
-
  • 出力として次の関数に仕様の証明を渡す
    • 
-
  • Hoare Conditionがプログラムの開始から停止するまで接続されていれば証明は完成
-
      
-
    • Meta Gear にて証明を値としてあたえているため
      • 
+
    • IndexはLoop変数
      • 
+
    • Invariantはloop変数の不変条件
      • 
+
    • loopに接続するCode Gearを与える
      • 
+
    • reduceは停止性を保証する減少列
      • 
 
    
-
    • 
-

+
これを一般的に証明することができている

 

 

+
実際のloopの接続

+
証明したい性質を以下のように記述する

+
whileTestSpec1 : (c10 : N) →  (e1 : Env ) → vari e1 ≡ c10 → ⊤
+whileTestSpec1 _ _ x = tt
+

+
loopをTerminatingLoopSで接続して仕様記述に繋げる

+
proofGearsTermS : {c10 :  N} → ⊤
+proofGearsTermS {c10} = whileTest' {_} {_}  {c10} (λ n p →  conversion1 n p (λ n1 p1 →
+    TerminatingLoopS Env (λ env → varn env)(λ n2 p2 loop → whileLoopSeg {_} {_} {c10} n2 p2 loop 
+    (λ ne pe → whileTestSpec1 c10 ne pe)) n1 p1 )) 
+

+
    
+
  • conversion1はPre Condition をPost Conditionに変換する
    • 
+
  • whileLoopSeg
    • 
+
  • ⊤
    • 
+

+

+

 
Gears Agda による BinaryTree の実装

-
    
-
  • Agdaが変数への再代入を許していないためそのままでは木構造を実装できない
-
      
-
    • 木構造を辿る際に現在いるノード以下の木構造をそのまま stack に格納する
      • 
-
    • replace / delete などの操作を行った後に stack を参照し Tree を再構築する
      • 
-
    • CbCへの変換の時に問題になりそうな予感
      • 
-
    
-
    • 
-
  • ここの説明いらないかも？
    • 
-

-

-

-
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
+
CbCと並行した実装をするため、Stackを明示した実装をする

+
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を積んでいく

 
 

 
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) 
   → (next : N → A → bt A → List (bt A) → t ) 
@@ -1571,7 +1539,7 @@
    top: 300px;
    text-align: center;
 }
-" data-heading-divider="1" class="slide" data-marpit-pagination="17" data-marpit-pagination-total="24" style="--paginate:true;--class:slide;--theme:default;--style:section {
+" data-heading-divider="1" class="slide" data-marpit-pagination="17" data-marpit-pagination-total="28" style="--paginate:true;--class:slide;--theme:default;--style:section {
   background-color: #FFFFFF;
   font-size: 28px;
   color: #4b4b4b;
@@ -1611,9 +1579,19 @@
    text-align: center;
 }
 ;--heading-divider:1;" data-size="16:9">
-
Gears Agda による BinaryTree の実装 loop connecter

-

-

+
Binary Tree の3種類の Invariant

+
Tree Invariant

+
    
+
  • Binary Tree が Key の順序に沿って構成されていることを表すData構造
    • 
+

+
Stack Invariant

+
    
+
  • Stackが木の昇順に構成されていることを表す
    • 
+

+
Replace Tree

+
    
+
  • 2つの木の1つのnodeが入れ替わっていることを示す
    • 
+

 
 

-
Gears Agda による Binary Tree の検証 Invariant

-
具体的な例を一つ挙げて、Invariantの説明を行う

+
Tree Invariant

 
    
-
  • Binary Tree の性質である、左の子のkeyは親より小さく、
    
-右の子のkeyは親より大きいことを検証
    • 
-
  • Stack に格納されているTreeはその次のStackの減少列になっているか
    • 
-
  • Tree を正しく入れ替えられているか
    • 
+
  • Invariant というよりも可能な Binary Tree 全体の集合を表す型
    • 
+
  • 制約付きのBinary Tree
    • 
 

+
data treeInvariant {n : Level} {A : Set n} : (tree : bt A) → Set n where
+    t-leaf : treeInvariant leaf 
+    t-single : (key : N) → (value : A) →  treeInvariant (node key value leaf leaf) 
+    t-right : {key key₁ : N} → {value value₁ : A} → {t₁ t₂ : bt A} → (key < key₁) 
+      → treeInvariant (node key₁ value₁ t₁ t₂)
+      → treeInvariant (node key value leaf (node key₁ value₁ t₁ t₂)) 
+    t-left  : {key key₁ : N} → {value value₁ : A} → {t₁ t₂ : bt A} → (key < key₁) 
+      → treeInvariant (node key value t₁ t₂)
+      → treeInvariant (node key₁ value₁ (node key value t₁ t₂) leaf ) 
+    t-node  : {key key₁ key₂ : N} → {value value₁ value₂ : A} 
+      → {t₁ t₂ t₃ t₄ : bt A} → (key < key₁) → (key₁ < key₂)
+      → treeInvariant (node key value t₁ t₂) 
+      → treeInvariant (node key₂ value₂ t₃ t₄)
+      → treeInvariant (node key₁ value₁ (node key value t₁ t₂) (node key₂ value₂ t₃ t₄)) 
+

 

 

-
Gears Agda による Binary Tree の検証 Invariant

+
Stack Invariant

 
    
-
  • Tree Invariant
    • 
+
  • StackにはTreeを辿った履歴が残っている
    • 
+
  • 辿り方はKeyの値に依存する
    • 
+
  • 実際のStackよりも豊富な情報を持っている
    • 
 

-
data treeInvariant {n : Level} {A : Set n} : (tree : bt A) → Set n where
-    t-leaf : treeInvariant leaf 
-    t-single : (key : N) → (value : A) →  treeInvariant (node key value leaf leaf) 
-    t-right : {key key₁ : N} → {value value₁ : A} → {t₁ t₂ : bt A} → (key < key₁) 
-      → treeInvariant (node key₁ value₁ t₁ t₂)
-      → treeInvariant (node key value leaf (node key₁ value₁ t₁ t₂)) 
-    t-left  : {key key₁ : N} → {value value₁ : A} → {t₁ t₂ : bt A} → (key < key₁) 
-      → treeInvariant (node key value t₁ t₂)
-      → treeInvariant (node key₁ value₁ (node key value t₁ t₂) leaf ) 
-    t-node  : {key key₁ key₂ : N} → {value value₁ value₂ : A} 
-      → {t₁ t₂ t₃ t₄ : bt A} → (key < key₁) → (key₁ < key₂)
-      → treeInvariant (node key value t₁ t₂) 
-      → treeInvariant (node key₂ value₂ t₃ t₄)
-      → treeInvariant (node key₁ value₁ (node key value t₁ t₂) (node key₂ value₂ t₃ t₄)) 
+
data stackInvariant {n : Level} {A : Set n} (key : N) : (top orig : bt A) 
+  → (stack : List (bt A)) → Set n where
+    s-single : {tree0 : bt A} → stackInvariant key tree0 tree0 (tree0 ∷ [])
+    s-right : {tree tree0 tree₁ : bt A} → {key₁ : N } → {v1 : A } → {st : List (bt A)} 
+      → key₁ < key  → stackInvariant key (node key₁ v1 tree₁ tree) tree0 st 
+      → stackInvariant key tree tree0 (tree ∷ st)
+    s-left :  {tree₁ tree0 tree : bt A} → {key₁ : N } → {v1 : A } → {st : List (bt A)} 
+      → key  < key₁ → stackInvariant key (node key₁ v1 tree₁ tree) tree0 st 
+      → stackInvariant key tree₁ tree0 (tree₁ ∷ st)
 

 
 

-
Gears Agda による Binary Tree の検証 Invariant

+
Replace Tree

 
    
-
  • Stack Invariant
    • 
+
  • 木の特定のnodeが正しく置き換えられているか
    • 
 

-
data stackInvariant {n : Level} {A : Set n} (key : N) : (top orig : bt A) 
-  → (stack : List (bt A)) → Set n where
-    s-single : {tree0 : bt A} → stackInvariant key tree0 tree0 (tree0 ∷ [])
-    s-right : {tree tree0 tree₁ : bt A} → {key₁ : N } → {v1 : A } → {st : List (bt A)} 
-      → key₁ < key  → stackInvariant key (node key₁ v1 tree₁ tree) tree0 st 
-      → stackInvariant key tree tree0 (tree ∷ st)
-    s-left :  {tree₁ tree0 tree : bt A} → {key₁ : N } → {v1 : A } → {st : List (bt A)} 
-      → key  < key₁ → stackInvariant key (node key₁ v1 tree₁ tree) tree0 st 
-      → stackInvariant key tree₁ tree0 (tree₁ ∷ st)
+
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)
+    r-node : {value₁ : A} → {t t₁ : bt A} 
+      → replacedTree key value (node key value₁ t t₁) (node key value t t₁) 
+    r-right : {k : N } {v1 : A} → {t t1 t2 : bt A}
+          → k < key →  replacedTree key value t2 t 
+          →  replacedTree key value (node k v1 t1 t2) (node k v1 t1 t) 
+    r-left : {k : N } {v1 : A} → {t t1 t2 : bt A}
+          → key < k →  replacedTree key value t1 t 
+          → replacedTree key value (node k v1 t1 t2) (node k v1 t t2) 
 

 
 

-
Gears Agda による Binary Tree の検証 Invariant

-
    
-
  • Replace Invariant
    • 
-

-
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)
-    r-node : {value₁ : A} → {t t₁ : bt A} 
-      → replacedTree key value (node key value₁ t t₁) (node key value t t₁) 
-    r-right : {k : N } {v1 : A} → {t t1 t2 : bt A}
-          → k < key →  replacedTree key value t2 t 
-          →  replacedTree key value (node k v1 t1 t2) (node k v1 t1 t) 
-    r-left : {k : N } {v1 : A} → {t t1 t2 : bt A}
-          → key < k →  replacedTree key value t1 t 
-          → replacedTree key value (node k v1 t1 t2) (node k v1 t t2) 
+
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
 

 
 

-
Gears Agda による Binary Tree の検証

-
Binary Tree の実装に対して上述した3つのInvariantを

-Meta 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
+
Hoare Condition の拡張

+
testなどでは仮定が入ることがある

+Hoare Conditionを拡張可能な部分があるrecordで定義する

+Cが拡張される部分で, これはDataの継続に相当する

+Code Gear に継続があるように Data Gearにも継続がある

+
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を用いた並列実行時のプログラムの正しさの証明
+
      
+
    • synchronized queue
      • 
+
    • concurrent tree
      • 
+
    
+
    • 
+
  • xv.6への適用
    • 
 
  • モデル検査
    • 
 

+
読めない間は待っている

+tree

 

-
{if(r===window.origin)try{if(e&&"string"==typeof e&&e.startsWith(t)){const[,t]=e.split(","),r=Number.parseFloat(t);Number.isNaN(r)||(o=r)}}catch(t){console.error(t)}})));let l=!1;Array.from(i.querySelectorAll("svg[data-marpit-svg]"),(t=>{var e,n,i,s;t.style.transform||(t.style.transform="translateZ(0)");const c=a||o||t.currentScale||1;r!==c&&(r=c,l=c);const d=t.getBoundingClientRect(),{length:u}=t.children;for(let r=0;r{null==e||e.postMessage(`${t}${l}`,"null"===window.origin?"*":window.origin)}))}r=1,o=void 0;const i=(t,e,r)=>{if(t.getAttribute(e)!==r)return t.setAttribute(e,r),!0};function a({once:t=!1,target:e=document}={}){const r="Apple Computer, Inc."===navigator.vendor?[n]:[];let o=!t;const a=()=>{for(const t of r)t({target:e});!function(t=document){Array.from(t.querySelectorAll('svg[data-marp-fitting="svg"]'),(t=>{var e;const r=t.firstChild,o=r.firstChild,{scrollWidth:n,scrollHeight:a}=o;let l,s=1;if(t.hasAttribute("data-marp-fitting-code")&&(l=null===(e=t.parentElement)||void 0===e?void 0:e.parentElement),t.hasAttribute("data-marp-fitting-math")&&(l=t.parentElement),l){const t=getComputedStyle(l),e=Math.ceil(l.clientWidth-parseFloat(t.paddingLeft||"0")-parseFloat(t.paddingRight||"0"));e&&(s=e)}const c=Math.max(n,s),d=Math.max(a,1),u=`0 0 ${c} ${d}`;i(r,"width",`${c}`),i(r,"height",`${d}`),i(t,"preserveAspectRatio",getComputedStyle(t).getPropertyValue("--preserve-aspect-ratio")||"xMinYMin meet"),i(t,"viewBox",u)&&t.classList.toggle("__reflow__")}))}(e),o&&window.requestAnimationFrame(a)};return a(),()=>{o=!1}}const l=Symbol(),s=document.currentScript;((t=document)=>{if("undefined"==typeof window)throw new Error("Marp Core's browser script is valid only in browser context.");if(t[l])return t[l];const e=a({target:t}),r=()=>{e(),delete t[l]};Object.defineProperty(t,l,{configurable:!0,value:r})})(s?s.getRootNode():document)}();
-
研究目的
コードの解説
-あとで…
findは全部書いても大丈夫そう
これは途中省略してよさそう
コードの解説
+
研究目的
```
+sample1 : (A : Set ) → Set
+sample1 a = a
+
+sample2 : (A : Set ) → (B : Set ) → Set
+sample2 a b = b
+```
findは全部書いても大丈夫そう
これは途中省略してよさそう
t-leaf はコンストラクタ
+
+
+コードの解説
 省略した方がたぶん絶対良い
 right と left なんかはほとんど対照的なので省略とかでよさそう
-あとは、木構造の仕様を満たすためにData型になっている説明があるとよさそう

\ No newline at end of file
diff -r 8a97e69f8615 -r 62e56d73f104 MindMap/slide.pdf
Binary file MindMap/slide.pdf has changed
diff -r 8a97e69f8615 -r 62e56d73f104 slide/note.md
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/slide/note.md	Fri Jan 07 00:58:07 2022 +0900
@@ -0,0 +1,122 @@
+
+
+# タイトル
+
+Gears Agdaにおける
+Left Learning Red Black Tree の検証について
+
+琉球大学 並列信頼研究室の上地が発表します
+
+# 目的
+そのまま読む
+
+# CbC
+もそのまま読む
+
+# Agda
+もそのまま読む
+
+# Agda の基本
+Agda の基本となる型の１つである Data 型について説明します
+
+record Env とあるところで Env という Record 型を定義  
+することを示しています
+
+そしてその中にvarnとvariがあり、その型が自然数であることを定義しています
+
+次に、記述する際の導入が以下のようになり
+varxに0を、variに1を定義しています
+
+導入後は変数 スペース record名でその中身にアクセスできます
+
+# Gears Agda の記法
+何と対応しているからLoopで記述するんだっけ
+
+Agdaの構文的に禁止していないので再帰呼び出しは使用しないよう注意が必要です
+
+以下がwhile loopのノーマルレベルでの記述になります
+
+まず型の方で
+Envを受け取り、Codeを受け取り、
+tを返すといった流れになっています
+
+このCodeはEnvを受け取った後にｔを返すというものです
+
+次に、入力を env next で受け取っています
+
+このcodeは後で再び説明するので、withの方はおいておいてください
+
+パターンマッチの方で、false trueの場合をかんがえています
+これはfalseの場合はnextにenvを渡します
+nextはenvを受け取ってtを返すので正しいです
+これがtを返すことでこの後も関数が続くこと、継続を示します
+
+
+# Gears Agdaと Gears CbCの対応
+そのまま読むでよさそう
+Contextだけ調べた方がよいかも
+
+
+# Normal levelと～
+今回検証に使用するHoare Conditionと証明も Meta levelです
+
+画像はよなおせ
+
+# Hoare logic
+プログラム が事前条件 P に関して停止し、停止後には必ず事後条件 Q が成り立つならば、プログラム S は、事前条件 P と事後条件 Q とに関して正当（correct）であるという
+
+簡単な例としてGears Agdaにてwhile loopを検証します
+
+以下のコードを詳細に説明します
+
+入力と出力に関しては前述しました
+このたーみねーてぃんぐはこの関数が停止することを示しています
+この実装ではagdaはloopが終了するのかわからず、コンパイルできないので
+このあのてーとをつけて停止することを明示します
+
+with文は引数であたえられた値を展開します。
+今回はその値をパターンマッチしています。
+
+これがless than で0とvarnを比較しています
+
+このwhileloopは、
+varnがこれからループする回数で、variがループした回数になります
+
+なので、これが0になると終了し次の関数であるnextに遷移し
+0でないならループする回数varxから今回分の１引いて
+variには今回分の1を足したものをEnvとしてもう一度関数を実行するという記述になっています
+
+# post condition 
+先ほど実装したノーマルレベルなwhile loopに対して
+事前条件となるPre / Post Condition を追加した実装をします
+
+そのまえにterminatingが付いていると停止性の証明をしたことにはならないので～
+
+
+このconditionはループしたい回数は
+これからループする回数とループした回数の和と等しいというものです
+
+exitのPostConditionもつけるべきだな…
+
+# loopの接続
+loopが前のページのWhile LoopSeg だな
+
+loopの部分の証明のみだな
+
+# 実際のloopの接続
+最終的にはループした回数が入力のループしたい回数と一致していることを
+証明したいので以下のようになります
+
+で、前回のものは最初から構造体（record）に値が格納されている状態から始まっていたので
+proofGearsTermS では、入力が自然数で、recordの定義から検証を行っている
+
+そしてそれを行っているのが最初の関数であるwhileTest'で
+ここでvarnが入力c10と一致し、variが0であることを証明している
+
+次の関数であるversionでは、whileTest'のrecord定義時のConditionから
+loop時のconditionを生成しています
+
+# testとの違い
+そのまま読むよ
+
+Condition 
diff -r 8a97e69f8615 -r 62e56d73f104 slide/slide.md
--- a/slide/slide.md	Thu Jan 06 16:57:53 2022 +0900
+++ b/slide/slide.md	Fri Jan 07 00:58:07 2022 +0900
@@ -76,7 +76,6 @@
 # Agda の基本 
 - Agdaとは定理証明支援器であり、関数型言語
 - Agdaでの関数は、最初に型について定義した後に、関数を定義する事で記述する
-    - これが Curry-Howard 対応となる
 - 型の定義部分で、入力と出力の型を定義できる
   -  input → output のようになる
 - 関数の定義は = を用いて行う
@@ -104,11 +103,11 @@
 
 型に対応する値の導入(intro)
 ```
-record {varx = zero ; vary = suc zero}
+record {varn = zero ; vari = suc zero}
 ```
 record の値のアクセス(elim)
 ```
-(env : Env) → varx env
+(env : Env) → varn env
 ```
 
 
@@ -116,7 +115,7 @@
 # Gears Agda の記法
 Gears Agda では CbC と対応させるためにすべてLoopで記述する
 loopは`→ t`の形式で表現する
-再起呼び出しは使わない(構文的には禁止していないので注意が必要)
+再帰呼び出しは使わない(構文的には禁止していないので注意が必要)
 ```
 {-# TERMINATING #-}
 whileLoop : {l : Level} {t : Set l} → Env → (Code : Env → t) → t
@@ -174,7 +173,6 @@
 ```
 - `{-# TERMINATING #-}`
 - with 文
-- 型と値
 
 # Gears Agda の Pre Condition Post Condition
 ```
@@ -220,7 +218,6 @@
     (λ ne pe → whileTestSpec1 c10 ne pe)) n1 p1 )) 
 ```
 - conversion1はPre Condition をPost Conditionに変換する
-- whileLoopSeg
 - ⊤
 
 # test との違い
@@ -445,14 +442,17 @@
 - Red Black Tree の実装
   - 今回定義した条件はそのまま Red Black Tree の検証に使用できるはず
 - Contextを用いた並列実行時のプログラムの正しさの証明
-  - syncronized queue
-  - concarent tree
+  - synchronized queue
+  - concurrent tree
 - xv.6への適用
 - モデル検査
 
+読めない間は待っている
+tree
+
 # まとめ
 - Gears Agda にて Binary Tree を検証することができた
-  - Gears Agda における Termination を使用しない実装の仕方を確率した
+  - Gears Agda における Termination を使用しない実装の仕方を確立した
   - Hoare Logic による検証もできるようになった
   - 今後は Red Black Tree の検証をすすめる
 - モデル検査をしたい