--- 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 について
 <!-- たぶん聴講者はわかると思うのでかるくで良い -->