Papers/2021/soto-prosym: slide/slide.md comparison

comparison slide/slide.md @ 11:8a97e69f8615

いったんスライドは完成

author	soto <soto@cr.ie.u-ryukyu.ac.jp>
date	Thu, 06 Jan 2022 16:57:53 +0900
parents	60d4617eac84
children	62e56d73f104

comparison

equal deleted inserted replaced

-:60d4617eac84
+:8a97e69f8615
 - 処理の単位を Code Gear, データの単位を Data Gear として記述するプログラミング言語
 - CbC のプログラミングでは Data Gear を Code Gear で変更し、その変更を次の Code Gear に渡して処理を行う。
 # Agda の基本
-- Agdaとは定理証明支援器であり、関数型言語である
+- Agdaとは定理証明支援器であり、関数型言語
-- Agdaでの関数は、最初に型について定義した後に、関数を定義する事で記述できる
+- Agdaでの関数は、最初に型について定義した後に、関数を定義する事で記述する
 - これが Curry-Howard 対応となる
 - 型の定義部分で、入力と出力の型を定義できる
 -  input → output のようになる
 - 関数の定義は = を用いて行う
 - 関数名の後、 = の前で受け取る引数を記述します
+<!--
 ```
 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
 vari : N
 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 を返すで継続を表す(tは呼び出し時に任意に指定してもよい. testに使える)
+- t を返すことで継続を表す(tは呼び出し時に任意に指定してもよい. testに使える)
 - tail call により light weight continuation を定義している
 # Gears Agda と Gears CbC の対応
 Gears Agda
 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は
+- conversion1はPre Condition をPost Conditionに変換する
 - whileLoopSeg
 - ⊤
 # test との違い
 - test では実数を与えた際の出力が仕様に沿ったものであるかを検証する
 - 今回の定理証明を用いた証明では実数を必要としない
 - そのため、入力の型の範囲全てに対して仕様を満たしているか検証できる
 # Gears Agda による BinaryTree の実装
-- Agdaが変数への再代入を許していないためそのままでは木構造を実装できない
+CbCと並行した実装をするため、Stackを明示した実装をする
-- 木構造を辿る際に現在いるノード以下の木構造をそのまま stack に格納する
-- replace / delete などの操作を行った後に stack を参照し Tree を再構築する
+```
-- CbCへの変換の時に問題になりそうな予感
+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
-# 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 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)
 → (next : N → A → bt A → List (bt A) → t )
 → (exit : bt A → t) → t
 <!--
 これは途中省略してよさそう
 -->
+# Binary Tree の3種類の Invariant
-# Gears Agda による BinaryTree の実装 loop connecter
+Tree Invariant
-```
+- Binary Tree が Key の順序に沿って構成されていることを表すData構造
-```
+Stack Invariant
+- Stackが木の昇順に構成されていることを表す
-# Gears Agda による Binary Tree の検証 Invariant
-具体的な例を一つ挙げて、Invariantの説明を行う
+Replace Tree
-- Binary Tree の性質である、左の子のkeyは親より小さく、
+- 2つの木の1つのnodeが入れ替わっていることを示す
-右の子のkeyは親より大きいことを検証
-- Stack に格納されているTreeはその次のStackの減少列になっているか
+# Tree Invariant
-- Tree を正しく入れ替えられているか
+- Invariant というよりも可能な Binary Tree 全体の集合を表す型
+- 制約付きのBinary Tree
-# Gears Agda による Binary Tree の検証 Invariant
-- Tree Invariant
 ```
 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₁ (node key value t₁ t₂) (node key₂ value₂ t₃ t₄))
 ```
 <!--
+t-leaf はコンストラクタ
 コードの解説
 省略した方がたぶん絶対良い
 right と left なんかはほとんど対照的なので省略とかでよさそう
 あとは、木構造の仕様を満たすためにData型になっている説明があるとよさそう
 -->
-# 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
 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)}
 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
-- Replace Invariant
+- 木の特定の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)
 r-node : {value₁ : A} → {t t₁ : bt A}
 → replacedTree key value (node key value₁ t t₁) (node key value t 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 の検証
+# find の Hoare Condition
-Binary Tree の実装に対して上述した3つのInvariantを
+findPでは treeInvariant をつかって stackInvariant を生成する
-Meta Data Gear として渡しながら実行できるように記述する
+停止性を証明する木の深さの不等式も証明する
 ```
-findP : {n m : Level} {A : Set n} {t : Set m} → (env : Env A)
+findP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree tree0 : bt A ) → (stack : List (bt A))
-→ treeInvariant env ∧ stackInvariant env
+→  treeInvariant tree ∧ stackInvariant key tree tree0 stack
-→ (exit : (env : Env A) → treeInvariant env ∧ stackInvariant env → t ) → t
+→ (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にも継続がある
+```
+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 の検証までしか行えていないが、
+- Deleteの実装
-今回定義した条件はそのまま Red Black Tree の検証に使用できるはず
+- Red Black Tree の実装
-- 今後は Gears Agda による実装と条件の追加をおこなう
+- 今回定義した条件はそのまま Red Black Tree の検証に使用できるはず
+- Contextを用いた並列実行時のプログラムの正しさの証明
+- syncronized queue
+- concarent tree
+- xv.6への適用
 - モデル検査
 # まとめ
 - Gears Agda にて Binary Tree を検証することができた
 - Gears Agda における Termination を使用しない実装の仕方を確率した
 - Hoare Logic による検証もできるようになった
 - 今後は Red Black Tree の検証をすすめる
 - モデル検査をしたい
-英語版も欲しい
+<!-- 英語版も欲しい-->
-condition を テンプレみたいに作ってかきやすくする話

Mercurial > hg > Papers > 2021 > soto-prosym

comparison slide/slide.md @ 11:8a97e69f8615