# HG changeset patch
# User kono
# Date 1519268661 -32400
# Node ID 73baedb5cdfb5d20fd9e1c290a1bb6060e558546
# Parent  989de96fe049ddeb2cdda7b5c6698a064aff2c91
fix

diff -r 989de96fe049 -r 73baedb5cdfb slide/slide.md
--- a/slide/slide.md	Thu Feb 22 03:18:45 2018 +0900
+++ b/slide/slide.md	Thu Feb 22 12:04:21 2018 +0900
@@ -17,7 +17,7 @@
 ## プログラムの信頼性の保証
 * 今回は **定理証明** をつかって仕様を検証する
 * 定理証明には定理証明支援系の言語 Agda を使用する
-  * Agda では型でプログラムの性質を論理式で記述し、型に対応する関数部分で論理式を解くことで証明を記述できる
+  * Agda では型でプログラムの性質を論理式で記述し、型を生成する関数を定義することで証明を記述できる
 <!-- interface の説明 -->
 * 今回は Agda を用いて CodeGear 、DataGear、Interfaceを定義した
 * この単位を用いて実装された Stack に Interface を実装し、性質の一部を証明した
@@ -35,23 +35,21 @@
 
 
 ## Agda の型
-* 例として popSingleLinkedStack を使う
-* singleLinkedStack は Stack の実装部分で push、 pop の
-* Agda の 型は **関数名 : 型** で定義される
+* Agda の 型は **関数名 : 型** 
 * Agda の 項、関数部分は **関数名 = 値**
-* なにかを受け取って計算して次の関数に継続する型(**-> (fa -> t) -> t**)
+* popSingleLinkedStack は Stack のpop のCodeGearで、継続に型Maybe aを受けとるCodeGear(** (fa -> t) -> t**)に渡す
+* Stack は空かもしれないので Maybe a を返す
 <!-- * stackを受け取り、stackの先頭を取ってという処理を行い、次の関数に渡すという関数の型 -->
-* このような形で CodeGear を Agda で定義できる
 
 ```AGDA
-popSingleLinkedStack : -> SingleLinkedStack a 
+popSingleLinkedStack : SingleLinkedStack a 
        -> (Code : SingleLinkedStack a -> (Maybe a) -> t) -> t
 ```
 
 ## Maybe
-* **Maybe** はNothingかJustを返す型でAgda の **data** として定義されている
-* ここでは Just か Nothing をパターンマッチで返す
-* 要素にも型を書く必要がある
+* **Maybe** はNothingかJust aに二つの場合を持つ型でAgda の **data** と定義されている
+* Just か Nothing はパターンマッチで場合分けする
+* Nothing と Just a は Maybe を生成する constructor
 
 ```AGDA
 data Maybe a : Set where
@@ -59,10 +57,11 @@
   Just    : a -> Maybe a
 ```
 
-## Agda でのデータの定義
-* Agda でのデータの定義の例として **refl** 定義を使用する
+## data を用いた等式のAgda での9証明
+* x ≡ x はAgdaでは常に正しい論理式
 * data は **data データ名 : 型** と書く
-* **refl** は左右の項が等しいことを表している
+* **refl** は左右の項が等しいことを表す x ≡ x を生成する項
+*  x ≡ x を証明したい時には refl と書く
 
 
 ```AGDA
@@ -70,13 +69,15 @@
   refl : x ≡ x
 ```
 
-## Agdaの関数
-* 例として popSingleLinkedStack を使う
+## Agda でのpopSingleLinkedStack での定義
 * Agdaでの関数の定義は **関数名 = 関数の実装** の書く
+* stack と cs は引数
+* top stack は Maybe a なので Nothing または Just
+* with でdataの場合分けをパターンマッチで行う
 <!-- * 関数での引数は **関数名 a b =** のように書く -->
 
 ```AGDA
-popSingleLinkedStack :  -> SingleLinkedStack a -> 
+popSingleLinkedStack :  SingleLinkedStack a -> 
    (Code : SingleLinkedStack a -> (Maybe a) -> t) -> t
 popSingleLinkedStack stack cs with (top stack)
 popSingleLinkedStack stack cs | Nothing = cs stack  Nothing
@@ -84,9 +85,8 @@
 ```
 
 ## record
-* record は複数のデータを纏めて記述する型
-* **record レコード名** と書き、その次の行に **field** と書く
-* その下の行に **フィールド名:型名** と列挙する
+* record は複数のデータをまとめて記述する型 (Java のオブジェクトと同じ)
+* **record レコード名** と書き、その次の行の **field** の後に**フィールド名:型名** と列挙する
 * SingleLinkedStack では top というフィールドに Maybe のかかっている Element 型の要素aが定義されている
 * Element では record で data と次の要素 next を定義している
 
@@ -114,13 +114,12 @@
 ## Agda での Interface の定義
 * singleLinkedStack の色々な実装を抽象的に表すために record を使い **StackMethods** をつくった
 * 実装時は関数の中で record を構築している
-* push、 pop は実装によらないAPI
+* push、 pop は実装によらないAPI、t は継続の返す型を表すSet
 <!-- わかりやすい説明を！ -->
 * push、 pop に singlelinkedstack の実装が入る
 
 ```AGDA
-record StackMethods {n m : Level } (a : Set n ) 
-    {t : Set m }(stackImpl : Set n ) : Set (m Level.⊔ n) where
+record StackMethods (stackImpl : Set n ) : Set  where
       field
         push : stackImpl -> a -> (stackImpl -> t) -> t
         pop  : stackImpl -> (stackImpl -> Maybe a -> t) -> t
@@ -133,13 +132,12 @@
 * このとき、どのような状態の Stack に push し、 pop をしても値が等しくなることを示したい
 * そのため、**状態の不定な** Stack を作成する関数を作成した
 
-## 不定な Stack の定義
-* 不定な Stack を作成する stackInSomeState という関数を作成した
+## 不定な Stack を作成する stackInSomeState という関数の定義
+* 不定なtackは入力(s : SingleLinkedStack a )で与える
 * stackInSomeState は stack を受け取り、状態の決まっていない stack を record を作成する
 
 ```AGDA
-stackInSomeState : {l m : Level } {D : Set l} {t : Set m } 
-   (s : SingleLinkedStack D ) -> Stack {l} {m} D {t}  ( SingleLinkedStack  D )
+stackInSomeState : (s : SingleLinkedStack a ) -> Stack a ( SingleLinkedStack  a )
 stackInSomeState s =  record { stack = s ; stackMethods = singleLinkedStackSpec }
 ```
 
@@ -150,10 +148,10 @@
 * 型部分に注目する
 
 ```AGDA
-push->push->pop2 : {l : Level } {D : Set l} (x y : D ) (s : SingleLinkedStack D ) ->
+push->push->pop2 : {l : Level } {a : Set l} (x y : a ) (s : SingleLinkedStack a ) ->
     pushStack ( stackInSomeState s )  x ( \s1 -> pushStack s1 y ( \s2 ->
     pop2Stack s2 ( \s3 y1 x1 -> (Just x ≡ x1 ) ∧ (Just y ≡ y1 ) ) ))    
-push->push->pop2 {l} {D} x y s = ?
+push->push->pop2 {l} {a} x y s = ?
 ```
 
 ## ラムダ式
@@ -161,7 +159,7 @@
 * **\s1 ->** はラムダ式で push->push->pop2 の型では次の CodeGear 部分にラムダ式を使いStackを渡している
 
 ```AGDA
-push->push->pop2 : {l : Level } {D : Set l} (x y : D ) (s : SingleLinkedStack D ) ->
+push->push->pop2 : {l : Level } {a : Set l} (x y : a ) (s : SingleLinkedStack a ) ->
     pushStack ( stackInSomeState s )  x ( \s1 -> pushStack s1 y ( \s2 ->
     pop2Stack s2 ( \s3 y1 x1 -> (Just x ≡ x1 ) ∧ (Just y ≡ y1 ) ) ))
 ```
@@ -178,7 +176,7 @@
 * そこで **∧** の部分を record で定義した
 
 ```AGDA
-push->push->pop2 {l} {D} x y s = { }0
+push->push->pop2 {l} {a} x y s = { }0
 ```
 
 ```AGDA
@@ -204,9 +202,9 @@
 * ∧でまとめたpi1、pi2は **refl** で証明することができた
 
 ```AGDA
-push->push->pop2 : {l : Level } {D : Set l} (x y : D ) (s : SingleLinkedStack D ) ->
+push->push->pop2 : {l : Level } {a : Set l} (x y : a ) (s : SingleLinkedStack a ) ->
     pushStack ( stackInSomeState s )  x ( \s1 -> pushStack s1 y ( \s2 -> pop2Stack s2 ( \s3 y1 x1 -> (Just x ≡ x1 ) ∧ (Just y ≡ y1 ) ) ))
-push->push->pop2 {l} {D} x y s = record { pi1 = refl ; pi2 = refl }
+push->push->pop2 {l} {a} x y s = record { pi1 = refl ; pi2 = refl }
 ```
 
 ## まとめと今後の課題