Mercurial > hg > Papers > 2021 > soto-prosym

comparison slide/slide.md @ 12:62e56d73f104

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
WIP カンペを追加 14ページまで
author soto <soto@cr.ie.u-ryukyu.ac.jp>
date Fri, 07 Jan 2022 00:58:07 +0900
parents 8a97e69f8615
children 76c3378c61dc
comparison
equal deleted inserted replaced
11:8a97e69f8615 12:62e56d73f104
74 74
75 75
76 # Agda の基本 76 # Agda の基本
77 - Agdaとは定理証明支援器であり、関数型言語 77 - Agdaとは定理証明支援器であり、関数型言語
78 - Agdaでの関数は、最初に型について定義した後に、関数を定義する事で記述する 78 - Agdaでの関数は、最初に型について定義した後に、関数を定義する事で記述する
79 - これが Curry-Howard 対応となる
80 - 型の定義部分で、入力と出力の型を定義できる 79 - 型の定義部分で、入力と出力の型を定義できる
81 - input → output のようになる 80 - input → output のようになる
82 - 関数の定義は = を用いて行う 81 - 関数の定義は = を用いて行う
83 - 関数名の後、 = の前で受け取る引数を記述します 82 - 関数名の後、 = の前で受け取る引数を記述します
84 83
102 open Env 101 open Env
103 ``` 102 ```
104 103
105 型に対応する値の導入(intro) 104 型に対応する値の導入(intro)
106 ``` 105 ```
107 record {varx = zero ; vary = suc zero} 106 record {varn = zero ; vari = suc zero}
108 ``` 107 ```
109 record の値のアクセス(elim) 108 record の値のアクセス(elim)
110 ``` 109 ```
111 (env : Env) → varx env 110 (env : Env) → varn env
112 ``` 111 ```
113 112
114 113
115 114
116 # Gears Agda の記法 115 # Gears Agda の記法
117 Gears Agda では CbC と対応させるためにすべてLoopで記述する 116 Gears Agda では CbC と対応させるためにすべてLoopで記述する
118 loopは`→ t`の形式で表現する 117 loopは`→ t`の形式で表現する
119 再起呼び出しは使わない(構文的には禁止していないので注意が必要) 118 再帰呼び出しは使わない(構文的には禁止していないので注意が必要)
120 ``` 119 ```
121 {-# TERMINATING #-} 120 {-# TERMINATING #-}
122 whileLoop : {l : Level} {t : Set l} → Env → (Code : Env → t) → t 121 whileLoop : {l : Level} {t : Set l} → Env → (Code : Env → t) → t
123 whileLoop env next with lt 0 (varn env) 122 whileLoop env next with lt 0 (varn env)
124 whileLoop env next | false = next env 123 whileLoop env next | false = next env
172 whileLoop env next | false = next env 171 whileLoop env next | false = next env
173 whileLoop env next | true = whileLoop (record {varn = (varn env) - 1 ; vari = (vari env) + 1}) next 172 whileLoop env next | true = whileLoop (record {varn = (varn env) - 1 ; vari = (vari env) + 1}) next
174 ``` 173 ```
175 - `{-# TERMINATING #-}` 174 - `{-# TERMINATING #-}`
176 - with 文 175 - with 文
177 - 型と値
178 176
179 # Gears Agda の Pre Condition Post Condition 177 # Gears Agda の Pre Condition Post Condition
180 ``` 178 ```
181 whileLoopSeg : {l : Level} {t : Set l} → {c10 : N } → (env : Env) → (varn env + vari env ≡ c10) 179 whileLoopSeg : {l : Level} {t : Set l} → {c10 : N } → (env : Env) → (varn env + vari env ≡ c10)
182 → (next : (e1 : Env )→ varn e1 + vari e1 ≡ c10 → varn e1 < varn env → t) 180 → (next : (e1 : Env )→ varn e1 + vari e1 ≡ c10 → varn e1 < varn env → t)
218 proofGearsTermS {c10} = whileTest' {_} {_} {c10} (λ n p → conversion1 n p (λ n1 p1 → 216 proofGearsTermS {c10} = whileTest' {_} {_} {c10} (λ n p → conversion1 n p (λ n1 p1 →
219 TerminatingLoopS Env (λ env → varn env)(λ n2 p2 loop → whileLoopSeg {_} {_} {c10} n2 p2 loop 217 TerminatingLoopS Env (λ env → varn env)(λ n2 p2 loop → whileLoopSeg {_} {_} {c10} n2 p2 loop
220 (λ ne pe → whileTestSpec1 c10 ne pe)) n1 p1 )) 218 (λ ne pe → whileTestSpec1 c10 ne pe)) n1 p1 ))
221 ``` 219 ```
222 - conversion1はPre Condition をPost Conditionに変換する 220 - conversion1はPre Condition をPost Conditionに変換する
223 - whileLoopSeg
224 - ⊤ 221 - ⊤
225 222
226 # test との違い 223 # test との違い
227 - test では実数を与えた際の出力が仕様に沿ったものであるかを検証する 224 - test では実数を与えた際の出力が仕様に沿ったものであるかを検証する
228 - コーナーケースで仕様に沿った動きをしていない場合を考慮できない 225 - コーナーケースで仕様に沿った動きをしていない場合を考慮できない
443 # 今後の研究方針 440 # 今後の研究方針
444 - Deleteの実装 441 - Deleteの実装
445 - Red Black Tree の実装 442 - Red Black Tree の実装
446 - 今回定義した条件はそのまま Red Black Tree の検証に使用できるはず 443 - 今回定義した条件はそのまま Red Black Tree の検証に使用できるはず
447 - Contextを用いた並列実行時のプログラムの正しさの証明 444 - Contextを用いた並列実行時のプログラムの正しさの証明
448 - syncronized queue 445 - synchronized queue
449 - concarent tree 446 - concurrent tree
450 - xv.6への適用 447 - xv.6への適用
451 - モデル検査 448 - モデル検査
452 449
450 読めない間は待っている
451 tree
452
453 # まとめ 453 # まとめ
454 - Gears Agda にて Binary Tree を検証することができた 454 - Gears Agda にて Binary Tree を検証することができた
455 - Gears Agda における Termination を使用しない実装の仕方を確率した 455 - Gears Agda における Termination を使用しない実装の仕方を確立した
456 - Hoare Logic による検証もできるようになった 456 - Hoare Logic による検証もできるようになった
457 - 今後は Red Black Tree の検証をすすめる 457 - 今後は Red Black Tree の検証をすすめる
458 - モデル検査をしたい 458 - モデル検査をしたい
459 459
460 <!-- 英語版も欲しい--> 460 <!-- 英語版も欲しい-->