# HG changeset patch # User soto # Date 1641370556 -32400 # Node ID edabf6c6885d68c1185755e1a93d7e5bcdf22dbe # Parent c563ad7f60cddb1a18bf45c9ddc1eeafe4c8402e WIP slide diff -r c563ad7f60cd -r edabf6c6885d slide/slide.md --- a/slide/slide.md Wed Dec 29 16:50:35 2021 +0900 +++ b/slide/slide.md Wed Jan 05 17:15:56 2022 +0900 @@ -58,7 +58,83 @@ - 当研究室でCbCという言語を開発している - C言語からループ構造とサブルーチンを取り除き、継続を導入したC言語の下位言語となる - 先行研究では Hoare Logic を用いて 簡単なプログラムの検証を行った -- 本研究では Gears Agda にて 重要なアルゴリズムの一つである Red Black Tree を検証する +- 本研究では Gears Agda にて重要なアルゴリズムの一つである Red Black Tree を検証する + + +# 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 +open Env +``` + +記述する際の基本的な例を以下に挙げる +``` +record {varx = zero ; vary = suc zero} +``` + + +# 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) } +``` + # CbC について - CbCとは当研究室で開発しているC言語の下位言語 @@ -67,8 +143,8 @@ - 処理の単位を Code Gear, データの単位を Data Gear として記述するプログラミング言語 - CbC のプログラミングでは Data Gear を Code Gear で変更し、その変更を次の Code Gear に渡して処理を行う。 + # Gears Agda の記法 -このこーどで使用しているAgdaの構文は解説が必要 - Agda では関数の再帰呼び出しが可能であるが、CbC で再起処理を実装しても値は帰って来ない - Agda で実装を行う際には再帰呼び出しを行わないようにする。 ``` @@ -77,8 +153,16 @@ ... | zero = exit (record { varx = varx env ; vary = vary env }) ... | suc y = next (record { varx = suc (varx env) ; vary = y }) ``` +- `→ t` で Set に遷移させるようにし、この後に関数が続くことと、関数を tail call していることで Continuation を定義している -- → t で Set に遷移させるようにし, この後に関数が続くことと関数を tail call していることで Continuation を定義している + +# Gears Agda と Gears CbC の対応 +- Gears Agda で実装を行い、同時に検証も行う +- これを CbC に変換する + +- Gears Agda は検証向きの実装となり、CbCでは高速な実行向きとなる +- Gears Agda での検証がCbCによる高速な実行の信頼性となる + # Hoare Logic について - Hoare Logic とは C.A.R Hoare、R.W Floyd が考案したプログラムの検証の手法 @@ -88,8 +172,16 @@ pre/post conditionの -# Gears Agda による検証の例(一部) -plus +# Gears Agda による検証の例(実装) +- 例として while program の検証をする + - まずは実装部分 +``` +{-# 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 +``` # Binary Tree について