# HG changeset patch # User ryokka # Date 1547538748 -32400 # Node ID fde9ee0cc8ae2c8c6495635b4ef777ed5ca946a7 # Parent e8fe28afe61e8d14c3b323e24859b9f46e79f744 fix diff -r e8fe28afe61e -r fde9ee0cc8ae slide/slide.md --- a/slide/slide.md Tue Jan 15 15:56:33 2019 +0900 +++ b/slide/slide.md Tue Jan 15 16:52:28 2019 +0900 @@ -43,28 +43,39 @@ ## Agda とは - Agda は定理証明支援系の言語 - 依存型を持つ関数型言語 -- 型を明記する必要がある +- Curry-Howard の証明支援系 +- 型と値がある - Agda の文法については次のスライドから軽く説明する -## Agda のデータ型 -- データ型は代数的なデータ構造 -- **data** キーワードの後に、**名前 : 型** -- 次の行以降は**コンストラクタ名 : 型** -- 型は**->**または**→**で繋げる - - 例えば、suc の型**Nat → Nat*は**Nat** を受け取り**Nat**を返す型 - - これにより 3 を suc (suc (suc zero)) のように表せる +## Agda での Gears の記述(whileLoop) +- Agda での CodeGear は通常の関数とは異なり、継続渡し (CPS : Continuation Passing Style) で記述された関数 +- CPS の関数は引数として継続を受け取って継続に計算結果を渡す +- **名前 : 引数 → (Code : fa → t) → t** +- **t** は継続 +- **(Code : fa → t)** は次の継続先 +- DataGear は Agda での CodeGear に使われる引数 +```AGDA + whileTest : {l : Level} {t : Set l} -> (c10 : ℕ) → (Code : Env -> t) -> t + whileTest c10 next = next (record {varn = c10 ; vari = 0} ) + + {-# 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 +``` + +## Agda での DataGear +- **DataGear** は CodeGear の引数 +- **データ型**と**レコード型**がある +- データ型は一つのデータ ```AGDA data Nat : Set where zero : Nat suc : Nat → Nat ``` - - - -## Agda のレコード型 -- C 言語での構造体に近い -- 複数のデータをまとめる -- 関数内で構築できる +- レコード型は複数のデータをまとめる - 構築時は**record レコード名 {フィールド名 = 値}** - 複数ある場合は **record Env {varn = 1 ; varn = 2}**のように **;** を使って列挙 ```AGDA @@ -74,20 +85,6 @@ vari : Nat ``` -## Agda の関数 -- 関数にも型が必要(1行目) - - 引き算はは自然数を２つ取って結果の自然数を返す - - **_** は任意の値、名前で使うと受け取った引数が順番に入る -- 関数本体は **関数名 = 値** -- 関数ではパターンマッチがかける - - ここでは関数名に **_** を使っているため**Nat**の定義にから zero かそれ以外でパターンマッチ -```AGDA - _-_ : Nat → Nat → Nat - x - zero = x - zero - _ = zero - (suc x) - (suc y) = x - y -``` - ## Agda での証明 - 関数の型に証明すべき論理式 - 関数自体にそれを満たす導出 @@ -102,6 +99,76 @@ ∧true {x} | true = refl ``` +## Gears をベースにした HoareLogic と証明(全体) +- Gears をベースにした while Program + - これは証明でもある +- whileループを任意の回数にするため**c10**は引数 +- whileTest' の継続に conversion1、その継続に whileLoop' が来て最後の継続に vari が c10 と等しい +```AGDA + proofGears : {c10 : Nat } → Set + proofGears {c10} = whileTest' {_} {_} {c10} (λ n p1 → conversion1 n p1 + (λ n1 p2 → whileLoop' n1 p2 (λ n2 → ( vari n2 ≡ c10 )))) +``` + +## Gears と HoareLogic をベースにした証明(whileTest) +- ここは代入する Command +- 最初の Command なので PreCondition がない +- もとの whileProgram では PComm を2回していたがまとめた +- proof2は Post Condition が成り立つことの証明 + - **_/\\_** は pi1 と pi2 のフィールドをもつレコード型 + - ２つのものを引数に取り、両方が同時に成り立つことを示す +- Gears での PostCondition は **引数 → (Code : fa → PostCondition → t) → t** +```AGDA + whileTest' : {l : Level} {t : Set l} → {c10 : Nat } → + (Code : (env : Env) → ((vari env) ≡ 0) /\ ((varn env) ≡ c10) → t) → t + whileTest' {_} {_} {c10} next = next env proof2 + where + env : Env + env = record {vari = 0 ; varn = c10} + proof2 : ((vari env) ≡ 0) /\ ((varn env) ≡ c10) <-- PostCondition + proof2 = record {pi1 = refl ; pi2 = refl} +``` + +## Gears と HoareLogic をベースにした証明(conversion) +- conversion は Condition から LoopInvaliant への変換を行う CodeGear +- proof4 は LoopInvaliant の証明 +- Gears での HoareLogic の完全な記述は **引数 → PreCondition → (Code : fa → PostCondition → t) → t** +```AGDA + conversion1 : {l : Level} {t : Set l } → (env : Env) → {c10 : Nat } → + ((vari env) ≡ 0) /\ ((varn env) ≡ c10) + → (Code : (env1 : Env) → (varn env1 + vari env1 ≡ c10) → t) → t + conversion1 env {c10} p1 next = next env proof4 + where + proof4 : varn env + vari env ≡ c10 + proof4 = let open ≡-Reasoning in + begin + varn env + vari env + ≡⟨ cong ( λ n → n + vari env ) (pi2 p1 ) ⟩ + c10 + vari env + ≡⟨ cong ( λ n → c10 + n ) (pi1 p1 ) ⟩ + c10 + 0 + ≡⟨ +-sym {c10} {0} ⟩ + c10 + ∎ +``` + +## Gears と HoareLogic をベースにした証明(全体) +- 最終状態で返ってくる i の値は c10 と一致する +- これにより証明が可能 +```AGDA + proofGears : {c10 : Nat } → Set + proofGears {c10} = whileTest' {_} {_} {c10} (λ n p1 → conversion1 n p1 + (λ n1 p2 → whileLoop' n1 p2 (λ n2 → ( vari n2 ≡ c10 )))) +``` + +## まとめと今後の課題 +- HoareLogic の while を使った例題を作成、証明を行った +- Gears を用いた HoareLogic ベースの検証方法を導入した + - 証明が引数として渡される記述のため証明とプログラムを一体化できた +- 今後の課題 + - RedBlackTree や SynchronizedQueue などのデータ構造の検証(HoareLogic ベースで) + + ## Agda 上での HoareLogic * Agda での HoareLogic は初期のAgda の実装である Agda1(現在のものはAgda2)で実装されたものと それを Agda2 に書き写したものが存在している。 @@ -301,98 +368,3 @@ -## Agda での Gears -- Agda での CodeGear は通常の関数とは異なり、継続渡し (CPS : Continuation Passing Style) で記述された関数 -- CPS の関数は引数として継続を受け取って継続に計算結果を渡す -- **名前 : 引数 → (Code : fa → t) → t** -- **t** は継続 -- **(Code : fa → t)** は次の継続先 -- DataGear は Agda での CodeGear に使われる引数 -```AGDA -_-_ : {t : Set} → Nat → Nat → (Code : Nat → t) → t -x - zero = (λ next → next x) -zero - _ = (λ next → next zero) -(suc x) - (suc y) = (x - y) -``` - -## Gears をベースにした HoareLogic と証明(全体) -- Gears をベースにした while Program - - これは証明でもある -- whileループを任意の回数にするため**c10**は引数 -- whileTest' の継続に conversion1、その継続に whileLoop' が来て最後の継続に vari が c10 と等しい -```AGDA - proofGears : {c10 : Nat } → Set - proofGears {c10} = whileTest' {_} {_} {c10} (λ n p1 → conversion1 n p1 - (λ n1 p2 → whileLoop' n1 p2 (λ n2 → ( vari n2 ≡ c10 )))) -``` - -## Gears と HoareLogic をベースにした証明(whileTest) -- ここは代入する Command -- 最初の Command なので PreCondition がない -- もとの whileProgram では PComm を2回していたがまとめた -- proof2は Post Condition が成り立つことの証明 - - **_/\\_** は pi1 と pi2 のフィールドをもつレコード型 - - ２つのものを引数に取り、両方が同時に成り立つことを示す -- Gears での PostCondition は **引数 → (Code : fa → PostCondition → t) → t** -```AGDA - whileTest' : {l : Level} {t : Set l} → {c10 : Nat } → - (Code : (env : Env) → ((vari env) ≡ 0) /\ ((varn env) ≡ c10) → t) → t - whileTest' {_} {_} {c10} next = next env proof2 - where - env : Env - env = record {vari = 0 ; varn = c10} - proof2 : ((vari env) ≡ 0) /\ ((varn env) ≡ c10) <-- PostCondition - proof2 = record {pi1 = refl ; pi2 = refl} -``` - -## Gears と HoareLogic をベースにした証明(conversion) -- conversion は Condition から LoopInvaliant への変換を行う CodeGear -- proof4 は LoopInvaliant の証明 -- Gears での HoareLogic の完全な記述は **引数 → PreCondition → (Code : fa → PostCondition → t) → t** -```AGDA - conversion1 : {l : Level} {t : Set l } → (env : Env) → {c10 : Nat } → - ((vari env) ≡ 0) /\ ((varn env) ≡ c10) - → (Code : (env1 : Env) → (varn env1 + vari env1 ≡ c10) → t) → t - conversion1 env {c10} p1 next = next env proof4 - where - proof4 : varn env + vari env ≡ c10 - proof4 = let open ≡-Reasoning in - begin - varn env + vari env - ≡⟨ cong ( λ n → n + vari env ) (pi2 p1 ) ⟩ - c10 + vari env - ≡⟨ cong ( λ n → c10 + n ) (pi1 p1 ) ⟩ - c10 + 0 - ≡⟨ +-sym {c10} {0} ⟩ - c10 - ∎ -``` - -## Gears と HoareLogic をベースにした証明(whileLoop) -- whileLoop は loopInvaliant が true の間 WhileLoop を回し続けるCodeGear -- この CodeGear は Agda がループが終わることが証明できてないため **{-# TERMINATING #-}** で明示 -- false になると次の CodeGear へ -```AGDA - {-# 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 -``` - -## Gears と HoareLogic をベースにした証明(全体) -- 最終状態で返ってくる i の値は c10 と一致する -- これにより証明が可能 -```AGDA - proofGears : {c10 : Nat } → Set - proofGears {c10} = whileTest' {_} {_} {c10} (λ n p1 → conversion1 n p1 - (λ n1 p2 → whileLoop' n1 p2 (λ n2 → ( vari n2 ≡ c10 )))) -``` - -## まとめと今後の課題 -- HoareLogic の while を使った例題を作成、証明を行った -- Gears を用いた HoareLogic ベースの検証方法を導入した - - 証明が引数として渡される記述のため証明とプログラムを一体化できた -- 今後の課題 - - RedBlackTree や SynchronizedQueue などのデータ構造の検証(HoareLogic ベースで)