Mercurial > hg > Papers > 2018 > ryokka-thesis

changeset 16:989de96fe049

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix slide
author ryokka
date Thu, 22 Feb 2018 03:18:45 +0900
parents 22f582c4908d
children 73baedb5cdfb
files slide/Makefile slide/slide.html slide/slide.md
diffstat 3 files changed, 171 insertions(+), 108 deletions(-) [+]
line wrap: on
line diff
--- a/slide/Makefile	Thu Feb 22 00:23:06 2018 +0900
+++ b/slide/Makefile	Thu Feb 22 03:18:45 2018 +0900
@@ -6,7 +6,7 @@
 	slideshow b $< -t s6cr --h2
 
 all: $(TARGET).html
-	open $(TARGET).html
+	open $(TARGET).html -a Google\ Chrome
 
 clean: 
 	rm -f *.html
--- a/slide/slide.html	Thu Feb 22 00:23:06 2018 +0900
+++ b/slide/slide.html	Thu Feb 22 03:18:45 2018 +0900
@@ -2,7 +2,7 @@
 <html>
 <head>
    <meta http-equiv="content-type" content="text/html;charset=utf-8">
-   <title>「Agda による継続を用いたプログラムの検証」</title>
+   <title>Agda による継続を用いたプログラムの検証</title>
 
 <meta name="generator" content="Slide Show (S9) v2.5.0 on Ruby 2.4.1 (2017-03-22) [x86_64-darwin16]">
 <meta name="author"    content="外間 政尊" >
@@ -66,7 +66,7 @@
       <tr>
         <td>
           <div align="center">
-            <h1><font color="#808db5">「Agda による継続を用いたプログラムの検証」</font></h1>
+            <h1><font color="#808db5">Agda による継続を用いたプログラムの検証</font></h1>
           </div>
         </td>
       </tr>
@@ -86,21 +86,40 @@
 <!-- === begin markdown block ===
 
       generated by markdown/1.2.0 on Ruby 2.4.1 (2017-03-22) [x86_64-darwin16]
-                on 2018-02-22 00:23:00 +0900 with Markdown engine kramdown (1.15.0)
+                on 2018-02-22 03:18:20 +0900 with Markdown engine kramdown (1.15.0)
                   using options {}
   -->
 
 <!-- _S9SLIDE_ -->
 <h2 id="section">プログラムの信頼性の保証</h2>
 <ul>
-  <li>動作するプログラムの信頼性を保証したい</li>
-  <li>プログラムの仕様を検証するには <strong>モデル検査</strong> と <strong>定理証明</strong> の２つの手法がある
+  <li>動作するプログラムの信頼性を保証したい
+<!-- ちょっとあれかも --></li>
+  <li>信頼性の保証をするためにはプログラムの仕様を検証する必要がある</li>
+  <li>プログラムの仕様を検証するにはモデル検査と <strong>定理証明</strong> の２つの手法がある
     <ul>
       <li>モデル検査 はプログラムの持つ状態を数え上げて仕様を満たしているかを確認する</li>
       <li>定理証明　はプログラムの性質を論理式で記述しそれが常に正しいことを証明する</li>
     </ul>
   </li>
-  <li>また、当研究室では検証しやすい単位として CodeGear、DataGearという単位を用いてプログラムを記述する手法を提案している</li>
+  <li>また、当研究室では検証しやすい単位として CodeGear、DataGear という単位を用いてプログラムを記述する手法を提案している</li>
+</ul>
+
+
+</div>
+<div class='slide '>
+<!-- _S9SLIDE_ -->
+<h2 id="section-1">プログラムの信頼性の保証</h2>
+<ul>
+  <li>今回は <strong>定理証明</strong> をつかって仕様を検証する</li>
+  <li>定理証明には定理証明支援系の言語 Agda を使用する
+    <ul>
+      <li>Agda では型でプログラムの性質を論理式で記述し、型に対応する関数部分で論理式を解くことで証明を記述できる
+<!-- interface の説明 --></li>
+    </ul>
+  </li>
+  <li>今回は Agda を用いて CodeGear 、DataGear、Interfaceを定義した</li>
+  <li>この単位を用いて実装された Stack に Interface を実装し、性質の一部を証明した</li>
 </ul>
 
 
@@ -109,11 +128,10 @@
 <!-- _S9SLIDE_ -->
 <h2 id="codegear--datagear">CodeGear と DataGear</h2>
 <ul>
-  <li>CodeGear とはプログラムを記述する際の処理の単位である。</li>
-  <li>DataGear は CodeGear で扱うデータの単位であり、処理に必要なデータが全て入っている。</li>
+  <li>CodeGear とはプログラムを記述する際の処理の単位である</li>
+  <li>DataGear は CodeGear で扱うデータの単位であり、処理に必要なデータが全て入っている</li>
   <li>CodeGear はメタ計算によって CodeGear へ接続される</li>
   <li>メタ計算を切り替えることで処理に変更を加えることなくプログラムの性質を検証できる</li>
-  <li>Agda 上で CodeGear 、 DataGear という単位を定義した</li>
 </ul>
 
 <div style="text-align: center;">
@@ -124,25 +142,14 @@
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
-<h2 id="agda-">Agda とは</h2>
+<h2 id="agda-">Agda の型</h2>
 <ul>
-  <li>定理証明支援系の関数型言語</li>
-  <li>型を明示する必要がある</li>
-  <li>また、インデントも意味を持つ</li>
-  <li>型に命題を入れ、関数部分に証明を記述する事ができる</li>
-</ul>
-
-
-</div>
-<div class='slide '>
-<!-- _S9SLIDE_ -->
-<h2 id="agda--1">Agda の型、関数</h2>
-<ul>
-  <li>例として singleLinkedStack の pop を使う</li>
+  <li>例として popSingleLinkedStack を使う</li>
+  <li>singleLinkedStack は Stack の実装部分で push、 pop の</li>
   <li>Agda の 型は <strong>関数名 : 型</strong> で定義される</li>
   <li>Agda の 項、関数部分は <strong>関数名 = 値</strong></li>
-  <li>なにかを受け取って計算して次の関数に継続する型(<strong>-&gt; (fa -&gt; t) -&gt; t</strong>)</li>
-  <li>これはstackを受け取り、stackの先頭を取ってという処理を行い、次の関数に渡すという関数の型</li>
+  <li>なにかを受け取って計算して次の関数に継続する型(<strong>-&gt; (fa -&gt; t) -&gt; t</strong>)
+<!-- * stackを受け取り、stackの先頭を取ってという処理を行い、次の関数に渡すという関数の型 --></li>
   <li>このような形で CodeGear を Agda で定義できる</li>
 </ul>
 
@@ -156,7 +163,7 @@
 <!-- _S9SLIDE_ -->
 <h2 id="maybe">Maybe</h2>
 <ul>
-  <li><strong>Maybe</strong> はNothingかJustを返す型でAgda の dataとして定義されている</li>
+  <li><strong>Maybe</strong> はNothingかJustを返す型でAgda の <strong>data</strong> として定義されている</li>
   <li>ここでは Just か Nothing をパターンマッチで返す</li>
   <li>要素にも型を書く必要がある</li>
 </ul>
@@ -170,10 +177,11 @@
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
-<h2 id="refl">refl</h2>
+<h2 id="agda--1">Agda でのデータの定義</h2>
 <ul>
-  <li>data は <strong>data データ名 :</strong> と書く</li>
-  <li>等しいという data として <strong>refl</strong> が定義されている</li>
+  <li>Agda でのデータの定義の例として <strong>refl</strong> 定義を使用する</li>
+  <li>data は <strong>data データ名 : 型</strong> と書く</li>
+  <li><strong>refl</strong> は左右の項が等しいことを表している</li>
 </ul>
 
 <pre lang="AGDA"><code>data _≡_ {a} {A : Set a} (x : A) : A → Set a where
@@ -186,8 +194,9 @@
 <!-- _S9SLIDE_ -->
 <h2 id="agda">Agdaの関数</h2>
 <ul>
-  <li>例として popSingleLinkedStack の関数を使う</li>
-  <li>関数での引数は <strong>関数名 a b :</strong> のように書く</li>
+  <li>例として popSingleLinkedStack を使う</li>
+  <li>Agdaでの関数の定義は <strong>関数名 = 関数の実装</strong> の書く
+<!-- * 関数での引数は **関数名 a b =** のように書く --></li>
 </ul>
 
 <pre lang="AGDA"><code>popSingleLinkedStack :  -&gt; SingleLinkedStack a -&gt; 
@@ -203,14 +212,15 @@
 <!-- _S9SLIDE_ -->
 <h2 id="record">record</h2>
 <ul>
-  <li>record は複数のデータを纏めて記述する型で、他の言語のオブジェクトのように <strong>レコード名.フィールド名</strong> でアクセスできる</li>
-  <li>SingleLinkedStack を例にとる</li>
+  <li>record は複数のデータを纏めて記述する型</li>
   <li><strong>record レコード名</strong> と書き、その次の行に <strong>field</strong> と書く</li>
   <li>その下の行に <strong>フィールド名:型名</strong> と列挙する</li>
   <li>SingleLinkedStack では top というフィールドに Maybe のかかっている Element 型の要素aが定義されている</li>
   <li>Element では record で data と次の要素 next を定義している</li>
 </ul>
 
+<!-- * 他の言語のオブジェクトのように **レコード名.フィールド名** でアクセスできる。例えば **SingleLinkedStack.top** のようにアクセスできる -->
+
 <pre lang="AGDA"><code>record SingleLinkedStack (a : Set) : Set where
   field
     top : Maybe (Element a)
@@ -228,9 +238,9 @@
   <li>複数書くときは <strong>;</strong> で区切る</li>
 </ul>
 
-<pre lang="Agda"><code>pushSingleLinkedStack2 : {n m : Level } {t : Set m } {Data : Set n} -&gt;
+<pre lang="Agda"><code>pushSingleLinkedStack : {n m : Level } {t : Set m } {Data : Set n} -&gt;
     SingleLinkedStack Data -&gt; Data -&gt; (Code : SingleLinkedStack Data -&gt; t) -&gt; t
-pushSingleLinkedStack2 stack datum next = 
+pushSingleLinkedStack stack datum next = 
     next record {top = Just (record {datum = datum;next =(top stack)})}
 </code></pre>
 
@@ -240,9 +250,10 @@
 <!-- _S9SLIDE_ -->
 <h2 id="agda--interface-">Agda での Interface の定義</h2>
 <ul>
-  <li>stack の色々な実装を抽象的に表すために record を使い <strong>StackMethods</strong> をつくった</li>
+  <li>singleLinkedStack の色々な実装を抽象的に表すために record を使い <strong>StackMethods</strong> をつくった</li>
   <li>実装時は関数の中で record を構築している</li>
-  <li>push、 pop は実装によらないAPI</li>
+  <li>push、 pop は実装によらないAPI
+<!-- わかりやすい説明を！ --></li>
   <li>push、 pop に singlelinkedstack の実装が入る</li>
 </ul>
 
@@ -257,12 +268,22 @@
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
-<h2 id="agda--interface--1">Agda での Interface を含めた部分的な証明</h2>
+<h2 id="section-2">証明の概要</h2>
 <ul>
-  <li>stackInSomeState で不定な Stack を作成し、そこに push し、直後に pop した値が push した値と等しいことを示している</li>
-  <li>Agda 中では不明な部分を <strong>?</strong> と書くことができる</li>
-  <li><strong>?</strong> 部分には値が入る</li>
-  <li>証明部分はラムダ式で与える</li>
+  <li>今回は singleLinkedStack の実装を抽象的に表す Interface を通し、 <strong>任意の数</strong> を push し pop したとき、
+push した値と pop した値が等しくなることを証明する</li>
+  <li>このとき、どのような状態の Stack に push し、 pop をしても値が等しくなることを示したい</li>
+  <li>そのため、<strong>状態の不定な</strong> Stack を作成する関数を作成した</li>
+</ul>
+
+
+</div>
+<div class='slide '>
+<!-- _S9SLIDE_ -->
+<h2 id="stack-">不定な Stack の定義</h2>
+<ul>
+  <li>不定な Stack を作成する stackInSomeState という関数を作成した</li>
+  <li>stackInSomeState は stack を受け取り、状態の決まっていない stack を record を作成する</li>
 </ul>
 
 <pre lang="AGDA"><code>stackInSomeState : {l m : Level } {D : Set l} {t : Set m } 
@@ -270,9 +291,21 @@
 stackInSomeState s =  record { stack = s ; stackMethods = singleLinkedStackSpec }
 </code></pre>
 
+
+</div>
+<div class='slide '>
+<!-- _S9SLIDE_ -->
+<h2 id="agda--interface--1">Agda での Interface を含めた部分的な証明</h2>
+<ul>
+  <li>push を２回行い、直後に pop を2回した値が push した値がpopした後の値と等しいことを示している</li>
+  <li>Agda 中では不明な部分を <strong>?</strong> と書くことができ、<strong>?</strong>部分には証明が入る</li>
+  <li>証明部分はラムダ式で与える</li>
+  <li>型部分に注目する</li>
+</ul>
+
 <pre lang="AGDA"><code>push-&gt;push-&gt;pop2 : {l : Level } {D : Set l} (x y : D ) (s : SingleLinkedStack D ) -&gt;
     pushStack ( stackInSomeState s )  x ( \s1 -&gt; pushStack s1 y ( \s2 -&gt;
-    pop2Stack s2 ( \s3 y1 x1 -&gt; (Just x ≡ x1 ) ∧ (Just y ≡ y1 ) ) ))
+    pop2Stack s2 ( \s3 y1 x1 -&gt; (Just x ≡ x1 ) ∧ (Just y ≡ y1 ) ) ))    
 push-&gt;push-&gt;pop2 {l} {D} x y s = ?
 </code></pre>
 
@@ -280,10 +313,10 @@
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
-<h2 id="section-1">ラムダ式</h2>
+<h2 id="section-3">ラムダ式</h2>
 <ul>
   <li>ラムダ式は関数内で無名の関数を定義することができる</li>
-  <li><strong>\s1 -&gt;</strong> はラムダ式で pushStack の次の CodeGear 部分にラムダ式を使いStackを継続している</li>
+  <li><strong>\s1 -&gt;</strong> はラムダ式で push-&gt;push-&gt;pop2 の型では次の CodeGear 部分にラムダ式を使いStackを渡している</li>
 </ul>
 
 <pre lang="AGDA"><code>push-&gt;push-&gt;pop2 : {l : Level } {D : Set l} (x y : D ) (s : SingleLinkedStack D ) -&gt;
@@ -296,17 +329,23 @@
 <div class='slide '>
 <!-- _S9SLIDE_ -->
 <h2 id="agda--interface--2">Agda での Interface を含めた部分的な証明</h2>
+
 <ul>
-  <li>証明部分に書いた ? はコンパイル後に <strong>{ }0</strong> に変わり、中に入る型が表示される</li>
-  <li>x、y はMaybe なので Justで返ってくる</li>
-  <li>push した x、 y と x1、 y1 が共に等しいことを証明したい</li>
-  <li>そこで <strong>∧</strong> の部分をrecordで定義した</li>
+  <li>
+    <p>? 部分はコンパイル時に Agda から内部に入る型を示してもらえる</p>
+  </li>
+  <li>
+    <p>ここでは最終的に <strong>(Just x ≡ x1) ∧ (Just y ≡ y1)</strong> が返ってくる事がわかる</p>
+  </li>
+  <li>
+    <p>(Just x ≡ x1)と(Just y ≡ y1)の２つが同時成り立ってほしい</p>
+  </li>
+  <li>
+    <p>そこで <strong>∧</strong> の部分を record で定義した</p>
+  </li>
 </ul>
 
-<pre lang="AGDA"><code>push-&gt;push-&gt;pop2 : {l : Level } {D : Set l} (x y : D ) (s : SingleLinkedStack D ) -&gt;
-    pushStack ( stackInSomeState s )  x ( \s1 -&gt; pushStack s1 y ( \s2 -&gt;
-    pop2Stack s2 ( \s3 y1 x1 -&gt; (Just x ≡ x1 ) ∧ (Just y ≡ y1 ) ) ))
-push-&gt;push-&gt;pop2 {l} {D} x y s = { }0
+<pre lang="AGDA"><code>push-&gt;push-&gt;pop2 {l} {D} x y s = { }0
 </code></pre>
 
 <pre lang="AGDA"><code>-- Goal
@@ -322,7 +361,7 @@
 <!-- _S9SLIDE_ -->
 <h2 id="agda--interface--3">Agda での Interface を含めた部分的な証明(∧)</h2>
 <ul>
-  <li>a と b の証明から aかつb を作るコンストラクタ</li>
+  <li>a と b の証明から a かつ b を作るために</li>
   <li>直積を表す型を定義する</li>
 </ul>
 
@@ -350,12 +389,14 @@
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
-<h2 id="section-2">今後の課題</h2>
+<h2 id="section-4">まとめと今後の課題</h2>
 <ul>
-  <li>本研究では Agda での Interface の記述及び Interface を含めた一部の証明を行った。</li>
-  <li>これにより、 Interface を経由しても一部の性質は実装と同様の働きをすることが証明できた。</li>
-  <li>また、これにより CbC での Interface 記述では考えられていなかった細かな記述が明らかになった。</li>
-  <li>今後の課題としては Hoare Logic を継続を用いた Agda で表現し、その Hoare Logic をベースとして証明を行えるかを確認する。また RedBlackTree の挿入、削除の性質に関する証明も行おうと考えている。</li>
+  <li>本研究では CodeGear、DataGear を Agda に定義できた</li>
+  <li>また Agda で Interface の記述及び Interface を含めた一部の証明を行えた</li>
+  <li>これにより、 Interface を経由しても一部の性質は実装と同様の働きをすることが証明できた
+<!-- * また、これにより CbC での Interface 記述では考えられていなかった細かな記述が明らかになった --></li>
+  <li>今後の課題としては  継続を用いた Agda で Hoare Logic を表現し、その Hoare Logic をベースとして証明を行えるかを確認する</li>
+  <li>また RedBlackTree の挿入、削除の性質に関する証明も行おうと考えている</li>
 </ul>
 
 
--- a/slide/slide.md	Thu Feb 22 00:23:06 2018 +0900
+++ b/slide/slide.md	Thu Feb 22 03:18:45 2018 +0900
@@ -1,4 +1,4 @@
-title: 「Agda による継続を用いたプログラムの検証」
+title: Agda による継続を用いたプログラムの検証
 author: 外間 政尊
 profile: @並列信頼研
 lang: Japanese
@@ -7,37 +7,40 @@
 
 ## プログラムの信頼性の保証
 * 動作するプログラムの信頼性を保証したい
-* プログラムの仕様を検証するには **モデル検査** と **定理証明** の２つの手法がある
+<!-- ちょっとあれかも -->
+* 信頼性の保証をするためにはプログラムの仕様を検証する必要がある
+* プログラムの仕様を検証するにはモデル検査と **定理証明** の２つの手法がある
   * モデル検査 はプログラムの持つ状態を数え上げて仕様を満たしているかを確認する
-  * 定理証明　はプログラムの性質を論理式で記述しそれが常に正しいことを証明する
-* また、当研究室では検証しやすい単位として CodeGear、DataGearという単位を用いてプログラムを記述する手法を提案している
+  * 定理証明　はプログラムの性質を論理式で記述しそれが常に正しいことを証明する  
+* また、当研究室では検証しやすい単位として CodeGear、DataGear という単位を用いてプログラムを記述する手法を提案している
+
+## プログラムの信頼性の保証
+* 今回は **定理証明** をつかって仕様を検証する
+* 定理証明には定理証明支援系の言語 Agda を使用する
+  * Agda では型でプログラムの性質を論理式で記述し、型に対応する関数部分で論理式を解くことで証明を記述できる
+<!-- interface の説明 -->
+* 今回は Agda を用いて CodeGear 、DataGear、Interfaceを定義した
+* この単位を用いて実装された Stack に Interface を実装し、性質の一部を証明した
 
 
 ## CodeGear と DataGear
-* CodeGear とはプログラムを記述する際の処理の単位である。
-* DataGear は CodeGear で扱うデータの単位であり、処理に必要なデータが全て入っている。
+* CodeGear とはプログラムを記述する際の処理の単位である
+* DataGear は CodeGear で扱うデータの単位であり、処理に必要なデータが全て入っている
 * CodeGear はメタ計算によって CodeGear へ接続される
 * メタ計算を切り替えることで処理に変更を加えることなくプログラムの性質を検証できる
-* Agda 上で CodeGear 、 DataGear という単位を定義した
 
 <div style="text-align: center;">
     <img src="./fig/cgdg.svg" alt="goto" width="800">
 </div>
 
 
-## Agda とは
-* 定理証明支援系の関数型言語
-* 型を明示する必要がある
-* また、インデントも意味を持つ
-* 型に命題を入れ、関数部分に証明を記述する事ができる
-
-
-## Agda の型、関数
-* 例として singleLinkedStack の pop を使う
+## Agda の型
+* 例として popSingleLinkedStack を使う
+* singleLinkedStack は Stack の実装部分で push、 pop の
 * Agda の 型は **関数名 : 型** で定義される
 * Agda の 項、関数部分は **関数名 = 値**
 * なにかを受け取って計算して次の関数に継続する型(**-> (fa -> t) -> t**)
-* これはstackを受け取り、stackの先頭を取ってという処理を行い、次の関数に渡すという関数の型
+<!-- * stackを受け取り、stackの先頭を取ってという処理を行い、次の関数に渡すという関数の型 -->
 * このような形で CodeGear を Agda で定義できる
 
 ```AGDA
@@ -46,7 +49,7 @@
 ```
 
 ## Maybe
-* **Maybe** はNothingかJustを返す型でAgda の dataとして定義されている
+* **Maybe** はNothingかJustを返す型でAgda の **data** として定義されている
 * ここでは Just か Nothing をパターンマッチで返す
 * 要素にも型を書く必要がある
 
@@ -56,9 +59,11 @@
   Just    : a -> Maybe a
 ```
 
-## refl
-* data は **data データ名 :** と書く
-* 等しいという data として **refl** が定義されている
+## Agda でのデータの定義
+* Agda でのデータの定義の例として **refl** 定義を使用する
+* data は **data データ名 : 型** と書く
+* **refl** は左右の項が等しいことを表している
+
 
 ```AGDA
 data _≡_ {a} {A : Set a} (x : A) : A → Set a where
@@ -66,8 +71,9 @@
 ```
 
 ## Agdaの関数
-* 例として popSingleLinkedStack の関数を使う
-* 関数での引数は **関数名 a b :** のように書く
+* 例として popSingleLinkedStack を使う
+* Agdaでの関数の定義は **関数名 = 関数の実装** の書く
+<!-- * 関数での引数は **関数名 a b =** のように書く -->
 
 ```AGDA
 popSingleLinkedStack :  -> SingleLinkedStack a -> 
@@ -78,13 +84,14 @@
 ```
 
 ## record
-* record は複数のデータを纏めて記述する型で、他の言語のオブジェクトのように **レコード名.フィールド名** でアクセスできる
-* SingleLinkedStack を例にとる
+* record は複数のデータを纏めて記述する型
 * **record レコード名** と書き、その次の行に **field** と書く
 * その下の行に **フィールド名:型名** と列挙する
 * SingleLinkedStack では top というフィールドに Maybe のかかっている Element 型の要素aが定義されている
 * Element では record で data と次の要素 next を定義している
 
+<!-- * 他の言語のオブジェクトのように **レコード名.フィールド名** でアクセスできる。例えば **SingleLinkedStack.top** のようにアクセスできる -->
+
 ```AGDA
 record SingleLinkedStack (a : Set) : Set where
   field
@@ -98,16 +105,17 @@
 * 複数書くときは **;** で区切る
 
 ```Agda
-pushSingleLinkedStack2 : {n m : Level } {t : Set m } {Data : Set n} ->
+pushSingleLinkedStack : {n m : Level } {t : Set m } {Data : Set n} ->
     SingleLinkedStack Data -> Data -> (Code : SingleLinkedStack Data -> t) -> t
-pushSingleLinkedStack2 stack datum next = 
+pushSingleLinkedStack stack datum next = 
     next record {top = Just (record {datum = datum;next =(top stack)})}
 ```
 
 ## Agda での Interface の定義
-* stack の色々な実装を抽象的に表すために record を使い **StackMethods** をつくった
+* singleLinkedStack の色々な実装を抽象的に表すために record を使い **StackMethods** をつくった
 * 実装時は関数の中で record を構築している
 * push、 pop は実装によらないAPI
+<!-- わかりやすい説明を！ -->
 * push、 pop に singlelinkedstack の実装が入る
 
 ```AGDA
@@ -118,11 +126,16 @@
         pop  : stackImpl -> (stackImpl -> Maybe a -> t) -> t
 ```
 
-## Agda での Interface を含めた部分的な証明
-* stackInSomeState で不定な Stack を作成し、そこに push し、直後に pop した値が push した値と等しいことを示している
-* Agda 中では不明な部分を **?** と書くことができる
-* **?** 部分には値が入る
-* 証明部分はラムダ式で与える
+
+## 証明の概要
+* 今回は singleLinkedStack の実装を抽象的に表す Interface を通し、 **任意の数** を push し pop したとき、
+push した値と pop した値が等しくなることを証明する
+* このとき、どのような状態の Stack に push し、 pop をしても値が等しくなることを示したい
+* そのため、**状態の不定な** Stack を作成する関数を作成した
+
+## 不定な Stack の定義
+* 不定な Stack を作成する stackInSomeState という関数を作成した
+* stackInSomeState は stack を受け取り、状態の決まっていない stack を record を作成する
 
 ```AGDA
 stackInSomeState : {l m : Level } {D : Set l} {t : Set m } 
@@ -130,16 +143,22 @@
 stackInSomeState s =  record { stack = s ; stackMethods = singleLinkedStackSpec }
 ```
 
+## Agda での Interface を含めた部分的な証明
+*  push を２回行い、直後に pop を2回した値が push した値がpopした後の値と等しいことを示している
+* Agda 中では不明な部分を **?** と書くことができ、**?**部分には証明が入る
+* 証明部分はラムダ式で与える
+* 型部分に注目する
+
 ```AGDA
 push->push->pop2 : {l : Level } {D : Set l} (x y : D ) (s : SingleLinkedStack D ) ->
     pushStack ( stackInSomeState s )  x ( \s1 -> pushStack s1 y ( \s2 ->
-    pop2Stack s2 ( \s3 y1 x1 -> (Just x ≡ x1 ) ∧ (Just y ≡ y1 ) ) ))
+    pop2Stack s2 ( \s3 y1 x1 -> (Just x ≡ x1 ) ∧ (Just y ≡ y1 ) ) ))    
 push->push->pop2 {l} {D} x y s = ?
 ```
 
 ## ラムダ式
 * ラムダ式は関数内で無名の関数を定義することができる
-* **\s1 ->** はラムダ式で pushStack の次の CodeGear 部分にラムダ式を使いStackを継続している
+* **\s1 ->** はラムダ式で push->push->pop2 の型では次の CodeGear 部分にラムダ式を使いStackを渡している
 
 ```AGDA
 push->push->pop2 : {l : Level } {D : Set l} (x y : D ) (s : SingleLinkedStack D ) ->
@@ -149,15 +168,16 @@
 
 
 ## Agda での Interface を含めた部分的な証明
-*  証明部分に書いた ? はコンパイル後に **{ }0** に変わり、中に入る型が表示される
-* x、y はMaybe なので Justで返ってくる
-* push した x、 y と x1、 y1 が共に等しいことを証明したい
-* そこで **∧** の部分をrecordで定義した
+
+* ? 部分はコンパイル時に Agda から内部に入る型を示してもらえる
+
+* ここでは最終的に **(Just x ≡ x1) ∧ (Just y ≡ y1)** が返ってくる事がわかる
+
+* (Just x ≡ x1)と(Just y ≡ y1)の２つが同時成り立ってほしい
+
+* そこで **∧** の部分を record で定義した
 
 ```AGDA
-push->push->pop2 : {l : Level } {D : Set l} (x y : D ) (s : SingleLinkedStack D ) ->
-    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 = { }0
 ```
 
@@ -170,7 +190,7 @@
 ```
 
 ## Agda での Interface を含めた部分的な証明(∧)
-* a と b の証明から aかつb を作るコンストラクタ
+* a と b の証明から a かつ b を作るために
 * 直積を表す型を定義する
 
 ```AGDA
@@ -189,11 +209,13 @@
 push->push->pop2 {l} {D} x y s = record { pi1 = refl ; pi2 = refl }
 ```
 
-## 今後の課題
-* 本研究では Agda での Interface の記述及び Interface を含めた一部の証明を行った。
-* これにより、 Interface を経由しても一部の性質は実装と同様の働きをすることが証明できた。
-* また、これにより CbC での Interface 記述では考えられていなかった細かな記述が明らかになった。
-* 今後の課題としては Hoare Logic を継続を用いた Agda で表現し、その Hoare Logic をベースとして証明を行えるかを確認する。また RedBlackTree の挿入、削除の性質に関する証明も行おうと考えている。
+## まとめと今後の課題
+* 本研究では CodeGear、DataGear を Agda に定義できた
+* また Agda で Interface の記述及び Interface を含めた一部の証明を行えた
+* これにより、 Interface を経由しても一部の性質は実装と同様の働きをすることが証明できた
+<!-- * また、これにより CbC での Interface 記述では考えられていなかった細かな記述が明らかになった -->
+* 今後の課題としては  継続を用いた Agda で Hoare Logic を表現し、その Hoare Logic をベースとして証明を行えるかを確認する
+* また RedBlackTree の挿入、削除の性質に関する証明も行おうと考えている
 
 
 ## Hoare Logic