Mercurial > hg > Papers > 2021 > soto-prosym

comparison slide/slide.md @ 10:60d4617eac84

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix slide intro
author soto <soto@cr.ie.u-ryukyu.ac.jp>
date Thu, 06 Jan 2022 13:59:12 +0900
parents e02e29a614c9
children 8a97e69f8615
comparison
equal deleted inserted replaced
9:e02e29a614c9 10:60d4617eac84
39 position: absolute; 39 position: absolute;
40 left: 50px; 40 left: 50px;
41 top: 35px; 41 top: 35px;
42 } 42 }
43 43
44 section.fig_cg p {
45 top: 300px;
46 text-align: center;
47 }
48
44 --- 49 ---
45 <!-- headingDivider: 1 --> 50 <!-- headingDivider: 1 -->
46 51
47 # Gears Agda による <br> Left Learning Red Black Tree の検証 52 # Gears Agda による <br> Left Learning Red Black Tree の検証
48 <!-- class: title --> 53 <!-- class: title -->
85 ``` 90 ```
86 91
87 92
88 # Agda の基本 record 93 # Agda の基本 record
89 - 2つのものが同時に存在すること 94 - 2つのものが同時に存在すること
90 - Record 型とはオブジェクトあるいは構造体のようなもの 95 - Record 型とはオブジェクトあるいは構造体
91 ``` 96 ```
92 record Env : Set where 97 record Env : Set where
93 field 98 field
94 varn : N 99 varn : N
95 vari : N 100 vari : N
96 open Env 101 open Env
97 ``` 102 ```
98 103
99 記述する際の基本的な例を以下に挙げる 104 型に対応する値の導入(intro)
100 ``` 105 ```
101 record {varx = zero ; vary = suc zero} 106 record {varx = zero ; vary = suc zero}
102 ``` 107 ```
103 108 record の値のアクセス(elim)
104 109 ```
105 # Agda の基本 data 110 (env : Env) → varx env
106 - 一つでも存在すること
107 - どちらかが成り立つ型を Data 型 で書く
108 ```
109 data bt {n : Level} (A : Set n) : Set n where
110 leaf : bt A
111 node : (key : N) → (value : A) → (left : bt A ) → (right : bt A ) → bt A
112 ```
113
114 記述する際の基本的な例を以下に挙げる
115 ```
116 datasample : bt → N
117 datasample leaf = zero
118 datasample (node key value left right) = suc zero
119 ```
120
121
122
123 # Agda の基本 短縮記法
124 - with を使用することでその変数のパターンマッチすることもできる
125 ```
126 patternmatch-default : Env → N
127 patternmatch-default record { varn = zero ; vari = i } = i
128 patternmatch-default record { varn = suc n ; vari = i } = patternmatch-default record { varn = n ; vari = suc i }
129 ```
130
131 ```
132 patternmatch-extraction : env → N
133 patternmatch-extraction env with varn env
134 patternmatch-extraction zero = vari env
135 patternmatch-extraction suc n = patternmatch-extraction record { varn = n ; vari = suc (vari env) }
136 ```
137 - ... | `を使用することで関数の定義部分を省略できる
138 ```
139 patternmatch-extraction' : env → N
140 patternmatch-extraction' env with varn env
141 ... | zero = vari env
142 ... | suc n = patternmatch-default' record { varn = n ; vari = suc (vari env) }
143 ``` 111 ```
144 112
145 113
146 114
147 # Gears Agda の記法 115 # Gears Agda の記法
148 - Agda では関数の再帰呼び出しが可能であるが、CbC で再起処理を実装しても値は帰って来ない 116 Gears Agda では CbC と対応させるためにすべてLoopで記述する
149 - Agda で実装を行う際には再帰呼び出しを行わないようにする。 117 loopは`→ t`の形式で表現する
150 ``` 118 再起呼び出しは使わない(構文的には禁止していないので注意が必要)
151 plus-com : {l : Level} {t : Set l} → Env → (next : Env → t) → (exit : Env → t) → t
152 plus-com env next exit with vary env
153 ... | zero = exit (record { varx = varx env ; vary = vary env })
154 ... | suc y = next (record { varx = suc (varx env) ; vary = y })
155 ```
156 - `→ t` で Set に遷移させるようにし、この後に関数が続くことと、関数を tail call していることで Continuation を定義している
157
158
159 # Gears Agda と Gears CbC の対応 x
160 - 証明のしやすいGears Agda で実装を行いながらContext単位で同時に検証も行う
161
162 - Gears Agda は検証向きの実装となり、CbCでは高速な実行向きとなる
163 - Gears Agda での検証がCbCによる高速な実行の信頼性となる
164
165 # Normal level と Meta Level を用いた信頼性の向上
166 CbCのプログラムの実行部分は以下の2つから構成される
167 - Normal Level は軽量継続で関数型プログラミングとなる
168 - atomicってなんだろう
169 - ポインタの操作はここでは行わず Meta Level にて行う
170 - Meta Level では信頼性を保証するために必要な計算を行う
171 - メモリやCPUなどの資源管理
172 - context
173 - 証明
174 - 並列実行（他のプロセスとの干渉）
175 - monad
176
177 # s
178 ![bg right:80%](meta_cg_dg.svg)
179
180 # Hoare Logic について
181 - Hoare Logic とは C.A.R Hoare, R.W Floyd が考案したプログラムの検証の手法
182 - 「プログラムの事前条件 (P) が成立しているときコマンド (C) 実行して停止すると事後条件 (Q) が成り立つ」というもの
183 - CbC の実行を継続するという性質に非常に相性が良い
184
185 pre/post condition を Gears Agda では Meta Input Data Gear として
186 プログラム中に遷移させていくことで、プログラムが終始仕様に沿った動きをしている
187 ことを検証する
188
189
190
191 # Gears Agda による検証の例（実装）
192 - while program の検証を例に挙げる
193 - 以下は実装部分のコードとなる
194 ``` 119 ```
195 {-# TERMINATING #-} 120 {-# TERMINATING #-}
196 whileLoop : {l : Level} {t : Set l} → Env → (Code : Env → t) → t 121 whileLoop : {l : Level} {t : Set l} → Env → (Code : Env → t) → t
197 whileLoop env next with lt 0 (varn env) 122 whileLoop env next with lt 0 (varn env)
198 whileLoop env next | false = next env 123 whileLoop env next | false = next env
199 whileLoop env next | true = whileLoop (record {varn = (varn env) - 1 ; vari = (vari env) + 1}) next 124 whileLoop env next | true = whileLoop (record {varn = (varn env) - 1 ; vari = (vari env) + 1}) next
200 ``` 125 ```
201 126 - t を返すで継続を表す(tは呼び出し時に任意に指定してもよい. testに使える)
202 127 - tail call により light weight continuation を定義している
203 # Gears Agda による検証の例（検証付き実装） 128
204 - 先ほど実装した while program に対して証明を付ける 129
205 - loop を接続する Meta Gear も用意する 130 # Gears Agda と Gears CbC の対応
131 Gears Agda
132 - 証明向きの記述
133 - Hoare Condition を含む
134
135 Gears CbC
136 - 実行向きの記述
137 - メモリ管理, 並列実行を含む
138
139 Context
140 - processに相当する
141 - Code Gear 単位で並列実行
142
143
144 # Normal level と Meta Level を用いた信頼性の向上
145 Normal Level
146 - 軽量継続
147 - Code Gear 単位で関数型プログラミングとなる
148 - atomic(Code Gear 自体の実行は割り込まれない)
149 - ポインタの操作は含まれない
150
151 Meta Level
152 - メモリやCPUなどの資源管理, ポインタ操作
153 - Hoare Condition と証明
154 - Contextによる並列実行
155 - monadに相当するData構造
156
157 #
158 <!-- class: fig_cg -->
159 ![height:700px](meta_cg_dg.svg)
160
161 # Gears Agda と Hoare Logic
162 <!-- class: slide -->
163 C.A.R Hoare, R.W Floyd が考案
164 - Pre Condition → Command → Post Condition
165
166 Gears Agda による Command の例
167 ```
168 {-# TERMINATING #-}
169 whileLoop : {l : Level} {t : Set l} → Env → (Code : Env → t) → t
170 whileLoop env next with lt 0 (varn env)
171 whileLoop env next | false = next env
172 whileLoop env next | true = whileLoop (record {varn = (varn env) - 1 ; vari = (vari env) + 1}) next
173 ```
174 - `{-# TERMINATING #-}`
175 - with 文
176 - 型と値
177
178 # Gears Agda の Pre Condition Post Condition
179 ```
180 whileLoopSeg : {l : Level} {t : Set l} → {c10 : N } → (env : Env) → (varn env + vari env ≡ c10)
181 → (next : (e1 : Env )→ varn e1 + vari e1 ≡ c10 → varn e1 < varn env → t)
182 → (exit : (e1 : Env )→ vari e1 ≡ c10 → t) → t
183 ```
184 - Terminatingを避けるためにloopを分割
185 - `varn env + vari env ≡ c10` が Pre Condition
186 - `varn e1 + vari e1 ≡ c10` が Post Condition
187 - `varn e1 < varn env → t` が停止を保証する減少列
188
189 これは命題なので証明を与えてPre ConditionからPost Conditionを導出する必要がある
190 証明は値として次のCodeGearに渡される
191
192 # Loop の接続
193 分割したloopを接続するMeta Code Gearを作成する
206 ``` 194 ```
207 TerminatingLoopS : {l : Level} {t : Set l} ( Index : Set ) 195 TerminatingLoopS : {l : Level} {t : Set l} ( Index : Set )
208 → {Invraiant : Index → Set } → ( reduce : Index → N) 196 → {Invraiant : Index → Set } → ( reduce : Index → N)
209 → (loop : (r : Index) → Invraiant r 197 → (loop : (r : Index) → Invraiant r
210 → (next : (r1 : Index) → Invraiant r1 → reduce r1 < reduce r → t ) → t) 198 → (next : (r1 : Index) → Invraiant r1 → reduce r1 < reduce r → t ) → t)
211 → (r : Index) → (p : Invraiant r) → t 199 → (r : Index) → (p : Invraiant r) → t
212 ``` 200 ```
213 - 入力として仕様の証明を受け取る 201 - IndexはLoop変数
214 - 出力として次の関数に仕様の証明を渡す 202 - Invariantはloop変数の不変条件
215 - Hoare Conditionがプログラムの開始から停止するまで接続されていれば証明は完成 203 - loopに接続するCode Gearを与える
216 - Meta Gear にて証明を値としてあたえているため 204 - reduceは停止性を保証する減少列
217 205
218 <!-- 206 これを一般的に証明することができている
219 コードの解説 207
220 あとで… 208 # 実際のloopの接続
221 --> 209 証明したい性質を以下のように記述する
210 ```
211 whileTestSpec1 : (c10 : N) → (e1 : Env ) → vari e1 ≡ c10 → ⊤
212 whileTestSpec1 _ _ x = tt
213 ```
214 loopをTerminatingLoopSで接続して仕様記述に繋げる
215 ```
216 proofGearsTermS : {c10 : N} → ⊤
217 proofGearsTermS {c10} = whileTest' {_} {_} {c10} (λ n p → conversion1 n p (λ n1 p1 →
218 TerminatingLoopS Env (λ env → varn env)(λ n2 p2 loop → whileLoopSeg {_} {_} {c10} n2 p2 loop
219 (λ ne pe → whileTestSpec1 c10 ne pe)) n1 p1 ))
220 ```
221 - conversion1は
222 - whileLoopSeg
223 - ⊤
222 224
223 # test との違い 225 # test との違い
224 - test では実数を与えた際の出力が仕様に沿ったものであるかを検証する 226 - test では実数を与えた際の出力が仕様に沿ったものであるかを検証する
225 - コーナーケースで仕様に沿った動きをしていない場合を考慮できない 227 - コーナーケースで仕様に沿った動きをしていない場合を考慮できない
226 - 今回の定理証明を用いた証明では実数を必要としない 228 - 今回の定理証明を用いた証明では実数を必要としない